I understand that Turing reduced the halting problem to the satisfiability problem of first-order logic thus proving first-order logic undecidable. However, when thinking about the sequent calculus for first-order logic (a la Gentzen), the only problematic rules appear to be the forall-left and exists-right rules when trying to prove decidability via proof-search. When these rules are applied bottom-up with a formula of the form QxA(x) (with Q a universal or existential quantifier), they force one to instantiate the x in A(x) with some term t. Nevertheless, it seems to me that the only terms one needs to consider when performing such an instantiation are those which occur in the end sequent, or the eigenvariables that arise from forall-right or exists-left rules. All other terms appear to me to be irrelevant. Notice that if we restrict the terms t that we instantiate A(x) with to those that are eigenvariables or those that are in the end sequent, then the forall-left and exists-right rules need only be applied a finite number of times in proof-search. Thus, my question is about why this proof-search strategy does not work, and where the "non-termination" of performing proof-search enters?

I assume that my misconception has something to do with my assumption that "All other terms appear to me to be irrelevant." If this is indeed the case, then why is this assumption wrong?

  • 1
    $\begingroup$ See Negri & von Plato, Structural Proof Theory, page 77 for an example of loop in the proof-search procedure. $\endgroup$ – Mauro ALLEGRANZA Feb 27 at 7:18
  • $\begingroup$ Thanks Mauro! This answers the question for G3i and first-order intuitionistic logic (which I was also wondering about). However, the counter-example provided on page 77 would terminate in G3c (for first-order logic) since universal and existential quantification are dual (hence, the formula provided in the non-termination example is classically valid). Do you perhaps know of a non-termination example in G3c as well? $\endgroup$ – Joe Smith Feb 27 at 10:52
  • 1
    $\begingroup$ Another classical counterexample is in S.C. Kleene, Mathematical Logic (1967), page 293 : the procedure "grows up" without end also if (with insight) we can find a counterexample. This corresponds to the fact (Lowenheim) that there are FOL formulas which are valid (not falsifiable) in every non-empty finite domain, but are not valid (are falsifiable) in an infinite domain. $\endgroup$ – Mauro ALLEGRANZA Feb 28 at 15:29

Your Answer

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

Browse other questions tagged or ask your own question.