Let H be a proof system for quantified propositional calculus (QPC). We define the Σqj-witnessing problem for H to be: given a prenex Σqj-formula A, an H-proof of A, and a truth assignment to the free variables in A, find a witness for the outermost existential quantifiers in A. We point out that the Σq1-witnessing problems for the systems G*1and G1 are complete for polynomial time and PLS (polynomial local search), respectively. We introduce and study the systems G*0 (...) and G0, in which cuts are restricted to quantifier-free formulas, and prove that the Σqj-witnessing problem for each is complete for NC1. Our proof involves proving a polynomial time version of Gentzen’s midsequent theorem for G*0 and proving that G0-proofs are TC0-recognizable. We also introduce QPC systems for TC0 and prove witnessing theorems for them. We introduce a finitely axiomatizable second-order system VNC1 of bounded arithmetic which we prove isomorphic to Arai’s first order theory AID + Σb0-CA for uniform NC1. We describe simple translations of VNC1 proofs of all bounded theorems to polynomial size families of G*0 proofs. From this and the above theorem we get alternative proofs of the NC1 witnessing theorems for VNC1 and AID. (shrink)

Let ℒ and ? be propositional languages over Basic Propositional Calculus, and ℳ = ℒ∩?. Weprove two different but interrelated interpolation theorems. First, suppose that Π is a sequent theory over ℒ, and Σ∪ {C⇒C′} is a set of sequents over ?, such that Π,Σ⊢C⇒C′. Then there is a sequent theory Φ over ℳ such that Π⊢Φ and Φ, Σ⊢C⇒C′. Second, let A be a formula over ℒ, and C 1, C 2 be formulas over ?, such (...) that A∧C 1⊢C 2. Then there exists a formula B over ℳ such that A⊢B and B∧C 1⊢C 2. (shrink)

We present an axiomatization for Basic Propositional Calculus BPC and give a completeness theorem for the class of transitive Kripke structures. We present several refinements, including a completeness theorem for irreflexive trees. The class of intermediate logics includes two maximal nodes, one being Classical Propositional Calculus CPC, the other being E1, a theory axiomatized by T → ⊥. The intersection CPC ∩ E1 is axiomatizable by the Principle of the Excluded Middle A V ∨ ⌝A. If (...) B is a formula such that → B is not derivable, then the lattice of formulas built from one propositional variable p using only the binary connectives, is isomorphically preserved if B is substituted for p. A formula → B is derivable exactly when B is provably equivalent to a formula of the form → A) →. (shrink)

The propositional calculus AoC, “Algebra of Classes”,and the extended propositional calculus EAC, “Extended Algebra ofClasses” are introduced in this paper. They are extensions, by additionalpropositional functions which are not invariant under the biconditional,of the corresponding classical propositional systems. Theirorigin lies in an analysis, motivated by Cantor’s concept of the cardinalnumbers, of A. P. Morse’s impredicative, polysynthetic set theory.

This paper is a conceptual study in the philosophy of logic. The question considered is 'How may formulae of the propositional calculus be brought into a representational relation to the world?'. Four approaches are distinguished: (1) the denotational approach, (2) the abbreviational approach, (3) the truth-conditional approach, and (4) the modelling approach. (2) and (3) are very familiar, so I do not discuss them. (1), which is now largely obsolete, led to some interesting twists and turns in early (...) analytic philosophy which will come as news to many contemporary readers, so I discuss it in some detail. The modelling approach is, to the best of my knowledge, newly introduced here. I am not presenting it as a rival to the other approaches, but as a philosophically interesting possibility. (shrink)

The purpose of the paper is to show that by cleaning Classical Logic (CL) from redundancies (irrelevances) and uninformative complexities in the consequence class and from too strong assumptions (of CL) one can avoid most of the paradoxes coming up when CL is applied to empirical sciences including physics. This kind of cleaning of CL has been done successfully by distinguishing two types of theorems of CL by two criteria. One criterion (RC) forbids such theorems in which parts of the (...) consequent (conclusion) can be replaced by arbitrary parts salva validitate of the theorem. The other (RD) reduces the consequences to simplest conjunctive consequence elements. Since the application of RC and RD to CL leads to a logic without the usual closure conditions, an approximation to RC and RD has been constructed by a basic logic with the help of finite (6-valued) matrices. This basic logic called RMQ (relevance, matrix, Quantum Physics) is consistent and decidable. It distinguishes two types of validity (strict validity) and classical or material validity. All theorems of CL (here: classical propositional calculus CPC) are classically or materially valid in RMQ. But those theorems of CPC which obey RC and RD and avoid the difficulties in the application to empirical sciences and to Quantum Physics are separated as strictly valid in RMQ. In the application to empirical sciences in general the proposed logic avoids the well known paradoxes in the area of explanation, confirmation, versimilitude and Deontic Logic. Concerning the application to physics it avoids also the difficulties with distributivity, commensurability and with Bell's inequalities. (shrink)

In recent research, some of the present authors introduced the concept of an $n$-dimensional Boolean algebra and its corresponding propositional logic $n\textrm{CL}$, generalizing the Boolean propositional calculus to $n\geq 2$ perfectly symmetric truth values. This paper presents a sound and complete sequent calculus for $n\textrm{CL}$, named $n\textrm{LK}$. We provide two proofs of completeness: one syntactic and one semantic. The former implies as a corollary that $n\textrm{LK}$ enjoys the cut admissibility property. The latter relies on the generalization (...) to the $n$-ary case of the classical proof based on the Lindenbaum algebra of formulas and Boolean ultrafilters. (shrink)

In this paper, we present valuation semantics for the Propositional Intuitionistic Calculus (also called Heyting Calculus) and three important subcalculi: the Implicative, the Positive and the Minimal Calculus (also known as Kolmogoroff or Johansson Calculus). Algorithms based in our definitions yields decision methods for these calculi. DOI:10.5007/1808-1711.2010v14n1p125.

Discusses alternative interpretations of the modal operators, for the modal propositional logic S5.

According to the standard definition, a first-order theory is categorical if all its models are isomorphic. The idea behind this definition obviously is that of capturing semantic notions in axiomatic terms: to be categorical is to be, in this respect, successful. Thus, for example, we may want to axiomatically delimit the concept of natural number, as it is given by the pre-theoretic semantic intuitions and reconstructed by the standard model. The well-known results state that this cannot be done within first-order (...) logic, but it can be done within second-order one. Now let us consider the following question: can we axiomatically capture the semantic concept of conjunction? Such question, to be sure, does not make sense within the standard framework: we cannot construe it as asking whether we can form a first-order (or, for that matter, whatever-order) theory with an extralogical binary propositional operator so that its only model (up to isomorphism) maps the operator on the intended binary truth-function. The obvious reason is that the framework of standard logic does not allow for extralogical constants of this type. But of course there is also a deeper reason: an existence of a constant with this semantics is presupposed by the very definition of the framework1. Hence the question about the axiomatic capturability of concunction, if we can make sense of it at all, cannot be asked within the framework of standard logic, we would have to go to a more abstract level. To be able to make sense of the question we would have to think about a propositional ‘proto-language’, with uninterpreted logical constants, and to try to search out axioms which would fix the denotations of the constants as the intended truth-functions. Can we do this? It might seem that the answer to this question is yielded by the completeness theorem for the standard propositional calculus: this theorem states that the axiomatic delimitation of the calculus and the semantic delimitation converge to the same result.. (shrink)

The propositional μ -calculus is an extension of the modal system K with a least fixpoint operator. Kozen posed a question about completeness of the axiomatisation of the logic which is a small extension of the axiomatisation of the modal system K. It is shown that this axiomatisation is complete.

Explicit description of maps definable by formulæ of the second order intuitionistic propositional calculus is given on two classes of linear Heyting algebras—the dense ones and the ones which possess successors. As a consequence, it is shown that over these classes every formula is equivalent to a quantifier free formula in the dense case, and to a formula with quantifiers confined to the applications of the successor in the second case.

With each superintuitionistic propositional logic L with a disjunction property we associate a set of modal logics the assertoric fragment of which is L . Each formula of these modal logics is interdeducible with a formula representing a set of rules admissible in L . The smallest of these logics contains only formulas representing derivable in L rules while the greatest one contains formulas corresponding to all admissible in L rules. The algebraic semantic for these logics is described.

Questions connected with the admissibility of rules of inference and the solvability of the substitution problem for modal and intuitionistic logic are considered in an algebraic framework. The main result is the decidability of the universal theory of the free modal algebra imageω extended in signature by adding constants for free generators. As corollaries we obtain: there exists an algorithm for the recognition of admissibility of rules with parameters in the modal system Grz, the substitution problem for Grz and for (...) the intuitionistic calculus H is decidable, intuitionistic propositional calculus H is decidable with respect to admissibility . A semantical criterion for the admissibility of rules of inference in Grz is given. (shrink)

We prove a finite model theorem and infinitary completeness result for the propositional -calculus. The construction establishes a link between finite model theorems for propositional program logics and the theory of well-quasi-orders.

An assignment is a function f that assigns subsets of N to some atoms. Then f is extended to f* which sends every formula A of HPC to a subset of S(A).

The present paper deals with a systemS of propositional calculus, conjunction, equivalence and falsum being its primitive terms.The only primitive rule inS is the rule of extensionality defined by the scheme: $\frac{{E\alpha \beta ,\Phi (\alpha )}}{{\Phi (\beta )}}$.

In this paper we obtain a finite Hilbert-style axiomatization of the implicationless fragment of the intuitionistic propositional calculus. As a consequence we obtain finite axiomatizations of all structural closure operators on the algebra of {–}-formulas containing this fragment.

LetL 3 c be the smallest set of propositional formulas, which containsCpCqpCCCpqCrqCCqpCrpCCCpqCCqrqCCCpqppand is closed with respect to substitution and detachment. Let $\mathfrak{M}_3^c $ be Łukasiewicz’s three-valued implicational matrix defined as follows:cxy=min (1,1−x+y), where $x,y \in \{ 0,\tfrac{1}{2},1\}$ . In this paper the following theorem is proved: $$L_3^c = E( \mathfrak{M}_3^c )$$ The idea used in the proof is derived from Asser’s proof of completeness of the two-valued propositional calculus. The proof given here is based on the Pogorzelski’s (...) deduction theorem fork-valued propositional calculi and on Lindenbaum’s theorem. (shrink)

We show that the quantified propositional proof systems Gi are polynomially equivalent to their restricted versions that require all cut formulas to be prenex Σqi . Previously this was known only for the treelike systems G*i. © 2011 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim.