Theories

In Chapters 11 and 12, we have asserted the important fact that decision machines cannot be constructed for PL and PL(=). This has an obvious consequence for axiomatic systems such as those discussed in Chapter 10. Let an axiomatic system be given by citing axioms involving certain non-logical constants, and by taking PL, PL(=), or PL(=) with symbols like “+” as the associated logic. We are now interested in discussing such axiomatic systems in general. It can be assumed that the only axiomatic systems of interest to us are (simply) consistent. We may then investigate the (simple) completeness of such axiomatic systems, and the question of whether or not decision machines can be constructed for them. Clearly, some (simply) consistent axiomatic systems are (simply) incomplete. We had some examples in Chapter 10. It is also clear that decision machines are not available for at least some axiomatic systems. To show this, we can imagine that each axiomatic system is re-abstracted to forms of the logical system with which it is associated. Then the question of whether a particular sentence is a theo?rem of the axiomatic system becomes equivalent to a question of whether a particular logical form is derivable from a set of other logical forms.