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.