4

I read in another question about the Hilbert-Ackermann Consistency Theorem:

Hilbert-Ackermann: An open theory $T$ is inconsistent iff there is a quasi-tautology which is a disjunction of negations of instances of nonlogical axioms of $T$.

In the other question it is also said that a quasi-tautology is a tautological consequence of instances of identity axioms and equality axioms.

Several questions:

  1. What are "tautological consequences of instances of identity axioms and equality axioms"?

  2. What is the use of this consistency theorem? Are there any noteworthy applications? If not, why was it formulated?

Jori
  • 1,698

1 Answers1

1

About 1., I have provided the necessary definitions in my answer to this question. The identity and equality axioms are the axioms which describe the behavior of the equality symbol. In Shoenfield's book, Mathematical Logic, they are of the form:

Identity Axiom: for any variable $x$, $x=x$ is an instance of the identity axiom;

and, for each $n$-ary function symbol $f$ and $m$-ary predicate symbol $P$ in the language, the following are instances of the equality axioms:

$(x_1 = y_1 \wedge \dots \wedge x_n = y_n) \rightarrow f(x_1, \dots, x_n) = f(y_1, \dots, y_n)$

$(x_1 = y_1 \wedge \dots \wedge x_m = y_m) \wedge P(x_1, \dots x_m) \rightarrow P(y_1, \dots, y_m)$.

As for your second question, the consistency theorem can be used, unsurprisingly, to prove consistency results. Shoenfield himself, on p. 51, uses it to sketch a consistency proof for a theory similar to Robinson arithmetic.

Nagase
  • 5,467
  • I've finally come around to reading Shoenfield's proof. But his explanation of finitism is confusing me in that section you reference where he finitarily "proves" the consistency of some system of arithmetic like $Q$. Now that I think more about it, I'm not sure how to think about finitism at all. Shoenfield mentions "concrete" and "visualizable". But in that section he also talks about validity in $\mathbb{N}$, which I'm not sure is finitary (I don't want to believe in completed infinities). Also how do we visualize things like $\forall x,y , (x+y=y+x)$. (cont.) – Jori Sep 23 '20 at 21:57
  • It's an abstract claim of many concrete instances. I can agree that you can give finitary justification to $1+2=2+1$, etc., but how can I finitarily make the jump from that to the recognition that I can finitarily recognize that it works in every concrete case where $x,y$ have been replaced by numerals. In such an abstract case the talk about visualization becomes shaky as well. – Jori Sep 23 '20 at 22:09