Online research in philosophy

The aim of this paper is to present the method of Socratic proofs for seven modal propositional logics: K5, S4.2, S4.3, S4M, S4F, S4R and G. This work is an extension of [10] where the method was presented for the most common modal propositional logics: K, D, T, KB, K4, S4 and S5.

We give a direct proof of admissibility of cut and contraction for the contraction-free sequent calculus G4ip for intuitionistic propositional logic and for a corresponding multi-succedent calculus: this proof extends easily in the presence of quantifiers, in contrast to other, indirect, proofs. i.e., those which use induction on sequent weight or appeal to admissibility of rules in other calculi.

We propose a new sequent calculus for bi intuitionistic logic which sits somewhere between display calculi and traditional sequent calculi by using nested sequents. Our calculus enjoys a simple (purely syntactic) cut elimination proof as do display calculi. But it has an easily derivable variant calculus which is amenable to automated proof search as are (some) traditional sequent calculi. We first present the initial calculus and its cut elimination proof. We then present the derived calculus, and then present a proof search strategy which allows it to be used for automated proof search. We prove that this search strategy is terminating and complete by showing how it can be used to mimic derivations obtained from an existing calculus GBiInt for bi intuitionistic logic. As far as we know, our new calculus is the first sequent calculus for bi intuitionistic logic which uses no semantic additions like labels, which has a purely syntactic cut elimination proof, and which can be used naturally for backwards proof search. Keywords: Bi-intuitionistic logic, display calculi, proof search.

We prove that the problem of determining the minimum propositional proof length is NP- hard to approximate within a factor of 2 log 1 - o(1) n . These results are very robust in that they hold for almost all natural proof systems, including: Frege systems, extended Frege systems, resolution, Horn resolution, the polynomial calculus, the sequent calculus, the cut-free sequent calculus, as well as the polynomial calculus. Our hardness of approximation results usually apply to proof length measured either by number of symbols or by number of inferences, for tree-like or dag-like proofs. We introduce the Monotone Minimum (Circuit) Satisfying Assignment problem and reduce it to the problems of approximation of the length of proofs.

We introduce new proof systems for propositional logic, simple deduction Frege systems, general deduction Frege systems, and nested deduction Frege systems, which augment Frege systems with variants of the deduction rule. We give upper bounds on the lengths of proofs in Frege proof systems compared to lengths in these new systems. As applications we give near-linear simulations of the propositional Gentzen sequent calculus and the natural deduction calculus by Frege proofs. The length of a proof is the number of lines (or formulas) in the proof. A general deduction Frege proof system provides at most quadratic speedup over Frege proof systems. A nested deduction Frege proof system provides at most a nearly linear speedup over Frege system where by "nearly linear" is meant the ratio of proof lengths is O(α(n)) where α is the inverse Ackermann function. A nested deduction Frege system can linearly simulate the propositional sequent calculus, the tree-like general deduction Frege calculus, and the natural deduction calculus. Hence a Frege proof system can simulate all those proof systems with proof lengths bounded by O(n · α(n)). Also we show that a Frege proof of n lines can be transformed into a tree-like Frege proof of O(n log n) lines and of height O(log n). As a corollary of this fact we can prove that natural deduction and sequent calculus tree-like systems simulate Frege systems with proof lengths bounded by O(n log n).

This paper develops a new proof method for two propositional paraconsistent logics: the propositional part of Batens' weak paraconsistent logic CLuN and Schütte's maximally paraconsistent logic Φv. Proofs are de.ned as certain sequences of questions. The method is grounded in Inferential Erotetic Logic.

First-order logic is formalized by means of tools taken from the logic of questions. A calculus of questions which is a counterpart of the Pure Calculus of Quantifiers is presented. A direct proof of completeness of the calculus is given.

We introduce a Gentzen-style modal predicate logic and prove the cut-elimination theorem for it. This sequent calculus of cut-free proofs is chosen as a proxy to develop the proof-theory of the logics introduced in [14, 15, 4]. We present syntactic proofs for all the metatheoretical results that were proved model-theoretically in loc. cit. and moreover prove that the form of weak reflection proved in these papers is as strong as possible.