Lesson 13

In general, however, our favorite model may have an axiomatization that consists of an infinite set of expressions. So, our proof system must be generalized to allow for proofs from infinitely many premises. Let \(\Delta\) be a set of expressions, and \(\phi\) another expression. We say that \(\phi\) is a valid consequence of \(\Delta\), written \(\Delta \models \phi\), if any model that satisfies each expression in \(\Delta\) must also satisfy \(\phi\). In our intended application to axiomatization, presumably the valid consequences of \(\Delta\) will be all properties of \(M_{0}\), and just these. So, we are very much interested in systematically generating all valid consequences of \(\Delta\).

We introduce next a proof system, which is a natural extension of the one above for validity, and is helpful in identifying valid consequences. Let \(\Delta\) be a set of expressions. Let \(S\) be a finite sequence of first-order expressions \(S = (\phi_{1}, \phi_{2}, …, \phi_{n})\), such that, for each expression \(\phi_{i}\) in the sequence, \(1 \leq i \leq n\), either (a) \(\phi \in \Lambda\), or (b) \(\phi \in \Delta\), or (c) there are two expressions of the form \(\psi\), \(\psi \Rightarrow \phi\) among the expressions \(\phi_{1}, …, \phi_{i-1}\). Then we say that \(S\) is a proof of \(\phi = \phi_{n}\) from \(\Delta\). The expression \(\phi\) is then called a \(\Delta\)-first-order theorem, and we write \(\Delta \vdash \phi\) (compare with \(\Delta \models \phi\)).

In other words, a \(\Delta\)-first-order theorem would be an ordinary first-order theorem if we allowed all expressions in \(\Delta\) to be added to our logical axioms. In this context, the expressions in \(\Delta\) are called the nonlogical axioms of our system.