4

I have trouble understanding the first lemma proof of the Herbrand's theorem section of the book. The proof of the lemma starts with a closed existential formula A and proves that A is a theorem iff T[$\neg$ B] is inconsistent, where B is the matrix of A. Then it invokes the consistency theorem (which states that 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 ) as a chain to prove the lemma. But to use that, shouldn't $\neg$ B be a non-logical axiom of T ? and this can't even be a case, since the lemma states that T is a theory with no nonlogical axioms.

Here's where i take a look at to help me understand the argument. In this proof the same technique is adopted.

user1868607
  • 5,791
doze
  • 45

1 Answers1

2

Apply the consistency theorem to the theory $\mathbf{T[not B]}$ rather than to $\mathbf{T}$.

Stephen A. Meigs
  • 433
  • Yes i eventually figured it out, i think i got some confusion about terminology by the book. Since T has no nonlogical axioms, T[notB] has only notB as nonlogical axiom and then the consistency theorem holds there for instances of notnotB. Thank you very much! – doze Sep 24 '16 at 23:22