2
$\begingroup$

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$?

$\endgroup$
6
  • $\begingroup$ 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. $\endgroup$ Feb 1 '16 at 10:41
  • $\begingroup$ @MauroALLEGRANZA: Do you know if the Hilbert-Bernays Project translation (English translation) of the Grundlagen, vol I has the proof translated? $\endgroup$ Feb 1 '16 at 12:00
  • $\begingroup$ It hase been published; see David Hilbert & Paul Bernays, Foundations of Mathematics I Part A. See also here. $\endgroup$ Feb 1 '16 at 12:27
  • $\begingroup$ @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 $\endgroup$ Feb 2 '16 at 17:30
  • $\begingroup$ (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? $\endgroup$ Feb 2 '16 at 17:39
3
$\begingroup$

The theorem holds for PRA.

However, in order to use it to prove that PRA is consistent, you would first need to know that none of the infinitely many disjunctions of negations of instances of PRA's axioms are quasi-tautologies. At least at first glance, that doesn't look particularly easy.

$\endgroup$
1
$\begingroup$

Iirc, Shoenfield proves the theorem in PA. It is, however, a theorem of PRA. If one could use it to prove the consistency of PRA in PRA, that would prove the consistency of PRA in PRA, which is impossible by Gődel's second incompleteness theorem. One can prove the consistency of PRA in, e.g., PA quite independently of the Hilbet–Ackermann consistency theorem: if PA is consistent, so is PRA; if PA is inconsistent, then it can prove anything, hence that PRA is consistent.

$\endgroup$
2
  • 1
    $\begingroup$ Can you cite references for your answer ? $\endgroup$
    – Shailesh
    Mar 21 '16 at 16:10
  • $\begingroup$ @zillion: Nelson's revenge, if correct? $\endgroup$ Mar 21 '16 at 22:46

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.