Eliminating definitions and Skolem functions in first-order logic

ABSTRACT

From proofs in any classical first-order theory that proves the existence of at least two elements, one can eliminate definitions in polynomial time. From proofs in any classical first-order theory strong enough to code finite functions, including sequential theories, one can also eliminate Skolem functions in polynomial time.

REFERENCES

• 1: Ajtai, M. 1988. The complexity of the pigeonhole principle. In Proceedings of the IEEE 29th Annual Symposium on Foundations of Computer Science. IEEE Computer Society Press, Los Almitos, Calif., 346--355.
• 2: Avigad, J. 1996. Formalizing forcing arguments in subsystems of second-order arithmetic. Ann. Pure Appl. Logic 82, 2, 165--191.
• 3: Avigad, J. 2000. A realizability interpretation for classical arithmetic. In Logic Colloquium '98 (Prague), Czech Republic Lecture Notes in Logic, vol. 13. Association of Symbolic Logic, Urbana, Ill. 57--90.
• 4: Avigad, J. 2001a. Algebraic proofs of cut elimination. J. Log. Algebr. Program. 49, 1-2, 15--30.
• 5: Jeremy Avigad, Eliminating Definitions and Skolem Functions in First-Order Logic, Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science, p.139, June 16-19, 2001
• 6: Avigad, J. 2001c. Weak theories of nonstandard arithmetic and analysis. In Reverse Mathematics 2001, Stephen Simpson, Ed. To appear.
• 7: Clote, P. and Krajíček, J. 1993. Arithmetic, Proof Theory, and Computational Complexity. Oxford University Press, Oxford, England.
• 8: Hájek, P. and Pudlák, P. 1993. Metamathematics of first-order arithmetic. Springer, Berlin, Germany.
• 9: Hilbert, D. and Bernays, P. 1939. Grundlagen der Mathematik. Vol. II. Springer, Berlin, Germany.
• 10: Jan Krajíček, Bounded arithmetic, propositional logic, and complexity theory, Cambridge University Press, New York, NY, 1996
• 11: Paris, J. and Wilkie, A. 1985. Counting problems in bounded arithmetic. In Methods in Mathematical Logic (Caracas, Venezuela), Lecture Notes in Mathematics, vol. 1130. Springer, Berlin, Germany, 317--340.
• 12: Pudlák, P. 1998. The lengths of proofs. In Handbook of Proof Theory. Stud. Logic Found. Math., vol. 137. North-Holland, Amsterdam, The Netherlands, 547--637.
• 13: Schwichtenberg, H. 1979. Logic and the axiom of choice. In Logic Colloquium '78, Maurice Boffa, Dirk van Dalen, and Kenneth McAloon, Eds., North-Holland, Amsterdam, The Netherlands, 351--356.
• 14: Shoenfield, J. R. 2001. Mathematical logic. Association for Symbolic Logic, Urbana, IL. Reprint of the 1973 second printing.
• 15: Takeuti, G. 1987. Proof Theory, 2nd ed. North-Holland, Amsterdam, The Netherlands.
• 16: A. S. Troelstra , H. Schwichtenberg, Basic proof theory (2nd ed.), Cambridge University Press, New York, NY, 2000

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Proof theory

Additional Classification:
  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
      I.2.3 Deduction and Theorem Proving

General Terms:
Algorithms, Theory

Keywords:
Definitions, Skolem functions, lengths of proofs, proof complexity