ON NON-MONOTONOUS PROPERTIES OF SOME CLASSICAL AND NONCLASSICAL PROPOSITIONAL PROOF SYSTEMS

We investigate the relations between the proof lines of non-minimal tautologies and its minimal tautologies for the Frege systems, the sequent systems with cut rule and the systems of natural deductions of classical and nonclassical logics. We show that for these systems there are sequences of tautologies ψn, every one of which has unique minimal tautologies φn such that for each n the minimal proof lines of φn are an order more than the minimal proof lines of ψn.

On Some Universal Propositional Proof Systems for Many-Valued Logic

Some uniform Hilbert-like propositional proof system is suggested for all versions of many-valued logic to apply them to 3 versions of 3-valued logic, two of which have only one designated value, and the last one has two designated values

CONSISTENCY OF CIRCUIT EVALUATION, EXTENDED RESOLUTION AND TOTAL NP SEARCH PROBLEMS

We consider sets ${\it\Gamma}(n,s,k)$ of narrow clauses expressing that no definition of a size $s$ circuit with $n$ inputs is refutable in resolution R in $k$ steps. We show that every CNF with a short refutation in extended R, ER, can be easily reduced to an instance of ${\it\Gamma}(0,s,k)$ (with $s,k$ depending on the size of the ER-refutation) and, in particular, that ${\it\Gamma}(0,s,k)$ when interpreted as a relativized NP search problem is complete among all such problems provably total in bounded arithmetic theory $V_{1}^{1}$. We use the ideas of implicit proofs from Krajíček [J. Symbolic Logic, 69 (2) (2004), 387–397; J. Symbolic Logic, 70 (2) (2005), 619–630] to define from ${\it\Gamma}(0,s,k)$ a nonrelativized NP search problem $i{\it\Gamma}$ and we show that it is complete among all such problems provably total in bounded arithmetic theory $V_{2}^{1}$. The reductions are definable in theory $S_{2}^{1}$. We indicate how similar results can be proved for some other propositional proof systems and bounded arithmetic theories and how the construction can be used to define specific random unsatisfiable formulas, and we formulate two open problems about them.