In this short note we relate some known properties of propositional calculus to purely algebraic considerations of a Boolean algebra. Classes of formulas of propositional calculus are considered as elements of a Boolean algebra. As such they can be represented by uniquely defined elements of this algebra which we call "logical primes". The algebraic notations appear useful because they make it possible to derive well known properties of propositional calculus by simple calculations or to substitute lengthy logical considerations by schematic algebraic manipulations.
For formulas of the Implicational Propositional Calculus (IPC) that are theorems of the classical Propositional Calculus (PC) we show that PC proofs yield IPC proofs. As a consequence, completeness of PC yields completeness of IPC.
In this paper, we consider iterative propositional calculi, which are finite sets of propositional formulas together with the rules of modus ponens and weak substitution (when formula being substituted must be already inferred). We construct an undecidable iterative propositional calculus using axioms in 3 variables. Particulary, we show that the general problem of derivability for these calculi is undecidable.
We introduce a multi-type display calculus for Propositional Dynamic Logic (PDL). This calculus is complete w.r.t. PDL, and enjoys Belnap-style cut-elimination and subformula property.
We give a normal five-valued truth-table proving independence of one of the axioms in Robinson's set of axioms for propositional calculus from 1968, answering a question raised in his article, where he uses a non-normal truth-table. We also give a normal four-valued truth-table proving independence of one of the other axioms, where he uses a normal five-valued truth-table.
In this paper, we construct an undecidable 3-variable superintuitionistic propositional calculus, i.e., a finitely axiomatizable extension of the intuitionistic propositional calculus with axioms containing only 3 variables. Since there are no 2-variable superintuitionistic propositional calculi, this is the minimal possible number of variables.
I formalize important theorems about classical propositional logic in the proof assistant Coq. The main theorems I prove are (1) the soundness and completeness of natural deduction calculus, (2) the equivalence between natural deduction calculus, Hilbert systems and sequent calculus and (3) cut elimination for sequent calculus.
The thesis of this paper is that truth-relevant logic is a better foundation for mathematics than classical logic. It is a system proposed by Richard Diaz in 1981. In a certain sense t-relevant logic is based on Kleene strong tables. These define a system with three values: true, false, unknown. It turns out that there exist tautologies with the following property: there exists a proper subset of propositional variables (t-relevant variables) such that for all combinations true/false the tautology will be true, that is, the rest of the variables (redundant variables) occurring in the tautology…
In this paper we consider propositional calculi, which are finitely axiomatizable extensions of intuitionistic implicational propositional calculus together with the rules of modus ponens and substitution. We give a proof of undecidability of the following problem for these calculi: whether a given finite set of propositional formulas constitutes an adequate axiom system for a fixed propositional calculus. Moreover, we prove the same for the following restriction of this problem: whether a given finite set of theorems of a fixed propositional calculus derives all theorems of this calculus. The…
Propositional logics in general, considered as a set of sentences, can be undecidable even if they have "nice" representations, e.g., are given by a calculus. Even decidable propositional logics can be computationally complex (e.g., already intuitionistic logic is PSPACE-complete). On the other hand, finite-valued logics are computationally relatively simple - at worst NP. Moreover, finite-valued semantics are simple, and general methods for theorem proving exist. This raises the question to what extent and under what circumstances propositional logics represented in various ways can be approx…
In this paper, we present a propositional sequent calculus containing disjoint copies of classical and intuitionistic logics. We prove a cut-elimination theorem and we establish a relation between this system and linear logic.
We present a rooted hypersequent calculus for modal propositional logic S5. We show that all rules of this calculus are invertible and that the rules of weakening, contraction, and cut are admissible. Soundness and completeness are established as well.
A contraction-free and cut-free sequent calculus $\msf{G3SDM}$ for semi-De Morgan algebras, and a structural-rule-free and single-succedent sequent calculus $\msf{G3DM}$ for De Morgan algebras are developed. The cut rule is admissible in both sequent calculi. Both calculi enjoy the decidability and Craig interpolation. The sequent calculi are applied to prove some embedding theorems: $\msf{G3DM}$ is embedded into $\msf{G3SDM}$ via Gödel-Gentzen translation. $\msf{G3DM}$ is embedded into a sequent calculus for classical propositional logic. $\msf{G3SDM}$ is embedded into the sequent calculus $\…
It is a consequence of existing literature that least and greatest fixed-points of monotone polynomials on Heyting algebras-that is, the alge- braic models of the Intuitionistic Propositional Calculus-always exist, even when these algebras are not complete as lattices. The reason is that these extremal fixed-points are definable by formulas of the IPC. Consequently, the $μ$-calculus based on intuitionistic logic is trivial, every $μ$-formula being equiv- alent to a fixed-point free formula. We give in this paper an axiomatization of least and greatest fixed-points of formulas, and an algorithm…
We show that the modalized Heyting calculus~\cite{esa06} admits a normal axiomatization. Then we prove that in this calculus the inference rule $\squareα/α$ is admissible (Proposition 5.6), but the rule $\squareα\rightarrowα/α$ is not (Proposition 6.1). Finally, we show that this calculus and intuitionistic propositional calculus are assertorically equipollent, which leads to a variant of limited separation property for the modalized Heyting calculus.
Cirquent calculus is a new proof-theoretic and semantic approach introduced for the needs of computability logic by G.Japaridze, who also showed that, through cirquent calculus, one can capture, refine and generalize independence-friendly (IF) logic. Specifically, the approach allows us to account for independence from propositional connectives in the same spirit as the traditional IF logic accounts for independence from quantifiers. Japaridze's treatment of IF logic, however, was purely semantical, and no deductive system was proposed. The present paper constructs a formal system sound and co…
It is a consequence of existing literature that least and greatest fixed-points of monotone polynomials on Heyting algebras-that is, the algebraic models of the Intuitionistic Propositional Calculus-always exist, even when these algebras are not complete as lattices. The reason is that these extremal fixed-points are definable by formulas of the IPC. Consequently, the $μ$-calculus based on intuitionistic logic is trivial, every $μ$-formula being equivalent to a fixed-point free formula. We give in this paper an axiomatization of least and greatest fixed-points of formulas, and an algorithm to …
Intuitionistic logic extended with decidable propositional atoms combines classical properties in its propositional part and intuitionistic properties for derivable formulas not containing propositional symbols. Sequent calculus is used as a framework for investigating this extension. Admissibility of cut is retained. Constrained Kripke structures are introduced for modeling intuitionistic logic with decidable propositional atoms. The extent of the disjunction and existence properties is investigated. The latest information about this research can be found at http://sakharov.net/median.html
Intuitionism and computing with partial information
Sofia University（索非亚大学）；University of Leeds（利兹大学）；University of California, Berkeley（加州大学伯克利分校）；Università Degli Studi di Siena（锡耶纳大学）；University of Wisconsin Madison（威斯康星大学麦迪逊分校）
We present a propositional modal logic $\sf WC$, which includes a logical $verum$ constant $\top$ but does not have any propositional variables. Furthermore, the only connectives in the language of $\sf WC$ are consistency-operators $\langle α\rangle$ for each ordinal $α$. As such, we end up with a class-size logic. However, for all practical purposes, we can consider restrictions of $\sf WC$ up to a given ordinal. Given the restrictive signature of the language, the only formulas are iterated consistency statements, which are called worms. The theorems of $\sf WC$ are all of the form $A \vdas…
Presented, in this monograph, are the results of the U. S. Naval Academy Mathematical Logic Course Project. The propositional and predicate calculus is presented in a unique manner. All aspects are rigorously established using the the fewest mathematical techniques. The propositional calculus is expanded considerably and many of the proof methods are used to establish the predicate calculus results. Consequnce operators are also introduced. Further, the material is considered to be a terminal experience and is directed towards applications such as logic-networks, procedures to determine the va…
A presentation is provided of the basic notions and operations of a) the propositional calculus of a variant of fuzzy logic -- canonical fuzzy logic, CFL -- and in a more succinct and introductory way, of b) the theory of fuzzy sets according to that same logic. The propositional calculus of bivalent classical logic and classical set theory can be considered as particular cases of the corresponding theories of CFL if the numerical value of a specific parameter $w$ is restricted to only two possibilities, 0 and 1.
This paper studies the transfinite propositional provability logics $\glp_Λ$ and their corresponding algebras. These logics have for each ordinal $ξ< Λ$ a modality $\la α\ra$. We will focus on the closed fragment of $\glp_Λ$ (i.e., where no propositional variables occur) and \emph{worms} therein. Worms are iterated consistency expressions of the form $\la ξ_n\ra \ldots \la ξ_1 \ra \top$. Beklemishev has defined well-orderings $<_ξ$ on worms whose modalities are all at least $ξ$ and presented a calculus to compute the respective order-types. In the current paper we present a generalization of t…
Intuitionistic belief has been axiomatized by Artemov and Protopopescu as an extension of intuitionistic propositional logic by means of the distributivity scheme K, and of co-reflection $A\rightarrow\Box A$. This way, belief is interpreted as a result of verification, and it fits an extended Brouwer-Heyting-Kolmogorov interpretation for intuitionistic propositional logic with an epistemic modality. In the present paper, structural properties of a natural deduction system $\mathsf{IEL}^{-}$ for intuitionistic belief are investigated. The focus is on the analyticity of the calculus, so that the…
In this article, we continue the study of tense symmetric Heyting algebras (or TSH-algebras). These algebras constitute a generalization of tense algebras. In particular, we describe a discrete duality for TSHalgebras bearing in mind the results indicated by E. Or lowska and I. Rewitzky in [E. Or lowska and I. Rewitzky, Discrete Dualities for Heyting Algebras with Operators, Fund. Inform. 81 (2007), no.1-3, 275-295.] for Heyting algebras. In addition, we introduce a propositional calculus and prove this calculus has TSH-algebras as algebraic counterpart. Finally, the duality mentioned above al…
The Kripke semantics of classical propositional normal modal logic is made algebraic via an embedding of Kripke structures into the larger class of pointed stably supported quantales. This algebraic semantics subsumes the traditional algebraic semantics based on lattices with unary operators, and it suggests natural interpretations of modal logic, of possible interest in the applications, in structures that arise in geometry and analysis, such as foliated manifolds and operator algebras, via topological groupoids and inverse semigroups. We study completeness properties of the quantale based se…
