Are the structure of logical expression based on formative constructions like sequences or trees ?

Question

Recently, I get confused when reading the book Principles of Mathematical Logic written by D. Hilbert. How to define the term 'logical expression'?

I just envisage that it might be defined as anyone who occur in a sequence , for whose element, one of the following conditions is satisfied.

A. it is an elementary expression, denoted $X, Y, Z$, ...

B. Constructed by two preceding elements with function notation & (and) $\lor$ (or).

C. constructed by one preceding element with function notation $一$ (negation).

This definition is similar to that of formative construction given by Bourbaki in his Theory of Sets, Chapter 1 : Description of formal mathematics.

Another idea is the tree model, the source of leaves just can be elementary expressions, and the tree constructed by &, $\lor$, $一$.

The point is that the two methods can't tell me the precise procedure even when we solve the simple question like : How a general logical expression cab be brought into a certain normal form (conjunction of disjunction ...).

I beg someone could tell me how I find the precise and constructive proof method with manipulation , like computer procedure. I may bewitched by my intelligence, like Wittgenstein said. Could I find some safe proof methods, please recommend some books, I get confused for so long a time.

Answer 1

I think that you must take into account that David Hilbert's Principles of Mathematical Logic is an old book (the first edition was : David Hilbert and Wilhelm Ackermann, Grundzüge der theoretischen Logik (1928)).

I think also that Bourbaki's text is not a good point to start with math log.

So said, your idea that the definition of well-formed logical expression can be best presented as a formation tree is perfectly sound; see Herbert Enderton, A Mathematical Introduction to Logic (2n ed - 2001) : page 17.

About "the precise procedure : how a general logical expression cab be brought into a certain normal form (conjunction of disjunction)", in propositional logic you can use truth-tables :

each line of the table which comes out $T$ will yield one of the basic conjunctions of the disjunctive normal form, where a basic conjunction is a conjunction with no repetition of a propositional letter (if that letter has $T$ in that line) or of the negation of propositional letters (if that letter has $F$ in that line).

This is an effective procedure (of course, with formulae with more than few propositional letters, the number of rows in the truth-table becomes practically intractable).