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)

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)

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)

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)

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 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.

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 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.

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)

We introduce a Gentzen style formulation of Basic Propositional Calculus(BPC), the logic that is interpreted in Kripke models similarly tointuitionistic logic except that the accessibility relation of eachmodel is not necessarily reflexive. The formulation is presented as adual-context style system, in which the left hand side of a sequent isdivided into two parts. Giving an interpretation of the sequents inKripke models, we show the soundness and completeness of the system withrespect to the class of Kripke models. The cut-elimination (...) theorem isproved in a syntactic way by modifying Gentzen's method. Thisdual-context style system exemplifies the effectiveness of dual-contextformulation in formalizing various non-classical logics. (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.

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 most difficult problem that Leniewski came across in constructing his system of the foundations of mathematics was the problem of defining definitions, as he used to put it. He solved it to his satisfaction only when he had completed the formalization of his protothetic and ontology. By formalization of a deductive system one ought to understand in this context the statement, as precise and unambiguous as possible, of the conditions an expression has to satisfy if it is added to (...) the system as a new thesis. Now, some protothetical theses, and some ontological ones, included in the respective systems, happen to be definitions. In the present essay I employ Leniewski's method of terminological explanations for the purpose of formalizing ukasiewicz's system of implicational calculus of propositions, which system, without having recourse to quantification, I first extended some time ago into a functionally complete system. This I achieved by allowing for a rule of implicational definitions, which enabled me to define any propositionforming functor for any finite number of propositional arguments. (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.

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

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)

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.

In classical propositional calculus for each proposition A(p) the following holds: $\vdash A(p) \leftrightarrow A^3(p)$ . In this paper we consider what remains of this in the intuitionistic case. It turns out that for each proposition A(p) the following holds: there is an n ∈ N such that $\vdash A^n(p) \leftrightarrow A^{n + 2}(p)$ . As a byproduct of the proof we give some theorems which may be useful elsewhere in propositional calculus.