No label defined (Q4699334)

This paper has to do with the set of well-formed formulas of propositional logic, based on a given set of atomic formulas and the connectives \(\neg,\vee,\wedge\), and \(\to\). The characterization of this structure as an absolutely free algebra is attributed to Tarski. The author constructs a second-order theory for such a structure, with a monadic predicate \(P\) (where \(Px\) is interpreted as `\(x\) is an atomic formula') and the connectives as function letters. The one second-order axiom of this theory is of the form \(\forall\varphi F\varphi\), where \(F\varphi\) is first-order. If we replace this axiom in the usual way by a corresponding first-order axiom schema, then the resulting theory is complete and decidable, but has non-standard models that are not structures corresponding to the well-formed formulas of a propositional logic. (The author actually discusses these results in the simplified case where negation is the only connective.) The author's conclusion is that it is not possible to find a first-order axiomatization of the set of well-formed formulas of propositional logic. He then claims that this negative result (namely, that the understanding of such a simple concept as that of a well-formed formula of propositional logic requires us to go beyond first-order logic) has `fundamental philosophical import' as an argument against formalism. The reviewer does not understand why this is so remarkable, since we already are familiar with many essentially higher-order concepts. For the entire collection see [Zbl 0919.00038].