Abstract

In this work we study the calculi for first-order logic as propositional proof systems. It is easy to see (and discussed in this thesis formally) that predicate calculi can serve as propositional proof systems. The question is whether they can allow for some shorter proofs.
The motivation for this comes from a problem whether there exists a polynomially bounded proof system. We will shortly review this problem (first stated by S.A.Cook and R.A.Reckhow) in the introduction to this thesis. We interpret calculi for predicate logic and some first-order theories as propositional proof system in the sense of Cook-Reckhow and we study their efficiency in terms of polynomial simulations.
We prove that predicate calculus is polynomially equivalent to Frege systems while a theory saying that there are at least two different elements is polynomially equivalent to the Quantified propositional calculus. We prove analogous results also for some stronger theories.
Further we define the notion of a "weak theory" and show that weak theries can be polynomially simulated by the Quantified propositional logic too. We conclude with some negative examples and some open problems.

Table of Contents

1. Abstract
2. Introduction
3. Propositional proof systems
4. Examples of propositional proof systems
5. Predicate calculus as propositional proof system
6. Weak first order theories
7. Theories extending $T_{\infty}$
8. Theories with "fast growing models"
9. Open problems