Related papers: Classical theorems in the Implicational Propositio…
We discuss tableaux for the Implicational Propositional Calculus and show how they may be used to establish its completeness.
We study $Q$-tableaux and axiom systems that they engender, producing a new proof that the Implicational Propositional Calculus is complete.
We prove a version of the Gr\"atzer-Schmidt theorem for the Lindenbaum-Tarski algebra associated to the Implicational Propositional Calculus.
We present a proof of completeness for the implicational propositional calculus, based on a variant of the Lindenbaum procedure.
Isomorphism between formulae is defined with respect to categories formalizing equality of deductions in classical propositional logic and in the multiplicative fragment of classical linear propositional logic caught by proof nets. This…
Craig interpolation is a fundamental property of classical and non-classic logics with a plethora of applications from philosophical logic to computer-aided verification. The question of which interpolants can be obtained from an…
Teaching proofs is a crucial component of any undergraduate-level program that covers formal reasoning. We have developed a calculational reasoning format and refined it over several years of teaching a freshman-level course, "Logic and…
Computability logic is a formal theory of computational tasks and resources. Its formulas represent interactive computational problems, logical operators stand for operations on computational problems, and validity of a formula is…
We shall settle the completeness of some classical positive propositional calculi (positive propositional calculi in which the so-called Peirce's law holds) by resorting to a close adaptation of Kalmar's completeness proof procedure. First…
Proof systems for the Relativized Propositional Calculus are defined and compared.
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…
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…
One advantage of paraconsistent logic is that it can deal with inconsistencies without making the system trivial. However, unlike classical propositional calculus, its deductive system is limited, and the meaning of paraconsistent negation…
The classical satisfiability problem (SAT) is used as a natural and general tool to express and solve combinatorial problems that are in NP. We postulate that provability for implicational intuitionistic propositional logic (IIPC) can serve…
The paper presents probabilistic extensions of interval temporal logic (ITL) and duration calculus (DC) with infinite intervals and complete Hilbert-style proof systems for them. The completeness results are a strong completeness theorem…
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…
We offer the proofs that complete our article introducing the propositional calculus called semi-intuitionistic logic with strong negation.
We study the notion of conservative translation between logics introduced by Feitosa and D'Ottaviano. We show that classical propositional logic (CPC) is universal in the sense that every finitary consequence relation over a countable set…
We give a calculus for reasoning about the first-order fragment of classical logic that is adequate for giving the truth conditions of intuitionistic Kripke frames, and outline a proof-theoretic soundness and completeness proof, which we…
"[M]athematicians care no more for logic than logicians for mathematics." Augustus de Morgan, 1868. Proofs are traditionally syntactic, inductively generated objects. This paper presents an abstract mathematical formulation of propositional…