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 is full and
The theories PAT for T being PA+ “S is a full
Consider the following sequence of formulas of the language L(PA) (one uses here arithmetization):
Γn+1(φ) = “there exists a proof of the formula φ
based on
Observe that in this system of ω-logic only the application of the ω-rule increases the degree of complexity of a proof.
Theorem 5 (Kotlarski 1986)
It can also be proved (cf. Kotlarski 1986) that the theory
The last sentence can be read as: “S makes all theorems of PA true”. It is equivalent to the
The system of ω-logic described above can be iterated in the transfinite and one can axiomatize theories
Define for an ordinal α a sequence
←34 | 35→
Theorem 6 (Kotlarski and Ratajczyk 1990b) Let m be a natural number. Then
The above theorems show how strong is Peano arithmetic augmented with an appropriate notion of satisfaction (and truth). One can see that only by assuming that the added notion of satisfaction (truth) is full and at least