theory PAn is complete with respect to In PA one can define partial notions of truth, i.e., one can define satisfaction and truth for formulas of a given class of the arithmetical hierarchy. Denote by
The previous theorem can now be formulated as:
In the definition of the hierarchy Tα no restriction was put on formulas to which the ω-rule was applied. Consider now a hierarchy in which such a restriction is put. So let T be any theory in the language L(PA). Define the following hierarchy of theories (cf. Niebergall 1996):
| T(o) | = | T, |
|
|
= |
|
|
|
||
| T(α+1) | = |
the smallest set of formulas containing |
| under the rules of inference of PA, | ||
| T(λ) | = |
|
Hence the ω-rule is now applied at stage n to
One has the following
Theorem 3 (Niebergall 1996) For any n ∈N,
The above theorems19 indicate interconnections between Peano arithmetic augmented with the ω-rule and the partial truths. Other connections between them can be formulated in the language of interpretability. So let S ≼ T denote that a theory S is relatively interpretable in the theory T (in the sense of Tarski 1953). We have now the following facts (cf. Niebergall 1996):
←32 | 33→
Theorem 4 Let ConS (for an appropriate theory S) denote a statement of L(PA) stating that S is consistent. Then
The above theorems indicate that the arithmetical truth, i.e., the set Th(No) of all arithmetical sentences true in the standard model No, can be approximated by syntactical methods, i.e. by demonstrability – though not by finitary means (one uses here the ω-rule).
So far, we have considered Peano arithmetic and partial truths. Ask now: What about PA and the full truth? Gödel’s and Tarski’s theoremshows that the truth predicate for L(PA) cannot be defined in PA. But one can extend the language L(PA) by adding a new binary predicate S called satisfaction class and characterizing it axiomatically by adding to Peano arithmetic PA axioms being an appropriate modification of Tarski’s definition of satisfaction (cf. Krajewski 1976, where this notion was introduced, or Murawski, 1997). Note that since those axioms form a finite set of axioms, one can write them as a single formula of the language L(PA) ∪ S. Denote this theory as PA + “S is a satisfaction class”. One can extend this theory by adding new axioms stating special properties of S. In particular, one can demand that S is full, i.e., S decides any formula of L(PA) on any valuation or that S is Γinductive for Γ being a given class of formulas of the language L(PA) ∪ S, i.e., that the induction axiom holds for all formulas of the class Γ (if Γ is the class of all formulas of L(PA) ∪ S then one says that the satisfaction class S is inductive).
Since theories T of the indicated type are extensions of PA one can ask what about natural numbers can be proved in T, i.e., one can consider theories of the type
Theorems of PAT are those sentences of the language L(PA) of Peano arithmetic (hence sentences about natural numbers) which can be proved in the stronger theory T. A natural problem of finding an axiomatization of the theory PAT arises.
One can easily see that the following theories are conservative extensions of PA:
| (a) | PA + “S is a satisfaction class”, |
| (b) | PA + “S is a full satisfaction class” and |
| (c) | PA + “S is an inductive satisfaction class”. |
←33 | 34→
This means that one can prove in those theories exactly the same theorems about natural numbers (i.e., formulas of the language L(PA)) as in Peano arithmetic PA. Hence the addition of a new notion, i.e., of a notion of a satisfaction class (and consequently a notion of truth), with properties indicated in (a)–(c) does not increase the proof-theoretical power of a theory with respect to sentences of the language L(PA). On the other hand, the assumption that a satisfaction class
