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.


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

  • $\begingroup$ 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! $\endgroup$
    – doze
    Sep 24 '16 at 23:22

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.