# Can one use the Hilbert-Ackermann Consistency Theorem to prove the consistency of $PRA$?

In his textbook Mathematical Logic, Shoenfield states the Hilbert-Ackermann Consistency Theorem as follows:

"Consistency Theorem (Hilbert-Ackermann): An open theory $T$ is inconsistent iff there is a quasi-tautology [i.e. a tautological consequence of instances of identity axioms and equality axioms--this from the first sentence of the paragraph (my comment)] which is a disjunction of negations of instances of nonlogical axioms of $T$."

He defines the term "open theory" as follows:

"[Pg. 48] A theory is open if all of its nonlogical axioms are open."

"[Pg. 36] A formula is open if it contains no quantifiers."

Since the usual formulation of $PRA$ (Primitive Recursive Arithmetic) is quantifier-free, it is, from a naive point of view, an 'open theory'.

Question: Does the Hilbert-Ackermann Consistency theorem hold for $PRA$? If so, can one (from the literature or otherwise) produce a theorem of the consistency of $PRA$ using the Hilbert-Ackermann Consistency Theorem? If not, could someone please explain to me why the theorem does not apply to $PRA$?

• It seems to me (due to my lack of knowledge of German) that the consistency of $\mathsf {PRA}$ is proved into David Hilbert & Paul Bernays, Grundlagen der Mathematik. Vol 1 (2nd ed.1968), page 376 : "folgt insbesondere die Widerspruchsfreiheit des Systems (D)." For System D, see page 366. Feb 1 '16 at 10:41
• @MauroALLEGRANZA: Do you know if the Hilbert-Bernays Project translation (English translation) of the Grundlagen, vol I has the proof translated? Feb 1 '16 at 12:00
• It hase been published; see David Hilbert & Paul Bernays, Foundations of Mathematics I Part A. See also here. Feb 1 '16 at 12:27
• @MauroALLEGRANZA: Yes, I am aware--I have downloaded the first two sections of the book from the Hilbert-Bernays project. You may or may not be aware that the editors used an essay by Wilfrid Seig titled "Hilbert's Proof Theory" as an introduction. In it, Seig quotes Hilbert and Bernays (from Vol. 1, I believe) as saying, regarding Primitive Recursive Arithmetic : "This recursive number theory is closely related to intuitive number theory, as we have considered it in [section] 2, befcause all of its formulas have a finitist contentual conent. This contentual interpretability follows Feb 2 '16 at 17:30
• (cont.) from the verifiability of all derivable formulas of recursive number theory, as we have established it already. Indeed, in this area verifiability has the character of a direct contentual interpretation, and thus the proof of consistency could be obtained here so easily." Does this describe the gist of their consistency proof for $PRA$? If so, would such a consistency proof be acceptable to the moderm mathematical community? Feb 2 '16 at 17:39