Arithmetic translations of axiom systems
Hao Henry Wang · Transactions of the American Mathematical Society · 1951
By applying the method of arithmetization to some proof of the well known Löwenheim-Skolem-Gödel theorem, we can prove that for each ordinary axiom system S (for example, the original Zermelo set theory as refined by Skolem) there are arithmetic predicates expressible in the notation of ordinary number theory such that when they are substituted for the predicates (for example, the membership predicate) in the axioms of S, the resulting assertions are all provable in the system obtained from ordinary number theory by adding the arithmetic statement Con(S) (expressing the consistency of S) as a new axiom.With the adoption of a suitable definition for the notion of translatability, the theorem can be rephrased as saying that every system S is translatable into the system obtained from number theory by adding Con(S) as an axiom.As the theorem reveals the strength of the assertion Con(S) for each given system S, it can be applied in considerations regarding problems of relative consistency.For two special systems N and N', it is shown that N' is translatable into N# (namely, the system obtained from N by adding Con(N) as an axiom) and that therefore the relative consistency of N' to N# can be proved in number theory.It is also observed that if N is co-consistent, then iV# is consistent.The same method can be applied, for similarly related systems S and S', to prove the relative consistency of S' to S#, although in certain cases S' is demonstrably not translatable into S. Using the same notion of translation, we have also, from Gödel's theorem on the impossibility of proving Con(S) in S, the conclusion that if Con(S) is provable in S', then S' is not translatable into S. Since, as it is known, the consistency of any given system can in a certain sense be proved in a stronger system, it follows that there exists an infinite sequence of systems Lo (being the ordinary number theory), Li, L2, • • • which are all of the same notation as the ordinary number theory and of which each is translatable into all its successors but none is translatable into any of its predecessors.There are also predicates Pi, P2, • ■ • such that Pm is definable in L" when and only when m is not greater than n.The question whether the arithmetic translations of the predicates such as Pi, P2, ■ ■ ■ could be recursive predicates seems to be an open question.To help us in the studies reported in this paper, Professors Paul Bernays, W. V. Quine, and J. Barkley Rosser have given generously their time and made very valuable criticisms as well as suggestions.