Propositional calculus

The propositional calculus^[a] is a branch of logic.^[1] It is also called propositional logic,^[2] statement logic,^[1] sentential calculus,^[3] sentential logic,^[1] or sometimes zeroth-order logic.^[4]^[5] It deals with propositions^[1] (which can be true or false)^[6] and relations between propositions,^[7] including the construction of arguments based on them.^[8] Compound propositions are formed by connecting propositions by logical connectives representing the truth functions of conjunction, disjunction, implication, biconditional, and negation.^[9]^[10]^[11]^[12] Some sources include other connectives, as in the table below.

Not to be confused with Propositional analysis.

Unlike first-order logic, propositional logic does not deal with non-logical objects, predicates about them, or quantifiers. However, all the machinery of propositional logic is included in first-order logic and higher-order logics. In this sense, propositional logic is the foundation of first-order logic and higher-order logic.

Propositional logic is typically studied with a formal language, in which propositions are represented by letters, which are called propositional variables. These are then used, together with symbols for connectives, to make compound propositions. Because of this, the propositional variables are called atomic formulas of a formal zeroth-order language.^[10]^[2] While the atomic propositions are typically represented by letters of the alphabet,^[10] there is a variety of notations to represent the logical connectives. The following table shows the main notational variants for each of the connectives in propositional logic.

The most thoroughly researched branch of propositional logic is classical truth-functional propositional logic,^[1] in which formulas are interpreted as having precisely one of two possible truth values, the truth value of true or the truth value of false.^[15] The principle of bivalence and the law of excluded middle are upheld. By comparison with first-order logic, truth-functional propositional logic is considered to be zeroth-order logic.^[4]^[5]

is a free online encyclopedia that anyone can edit.

Wikipedia

is the capital of England.

London

All speak at least three languages.

Wikipedia editors

$p_{5}$

$c_{3}^{2}(p_{2},p_{9})$

$c_{3}^{2}(p_{1},c_{2}^{1}(p_{3}))$

$c_{1}^{3}(p_{4},p_{6},c_{2}^{2}(p_{1},p_{2}))$

$c_{4}^{2}(c_{1}^{1}(p_{7}),c_{3}^{1}(p_{8}))$

$c_{2}^{3}(c_{1}^{2}(p_{3},p_{4}),c_{2}^{1}(p_{5}),c_{3}^{2}(p_{6},p_{7}))$

$c_{3}^{1}(c_{1}^{3}(p_{2},p_{3},c_{2}^{2}(p_{4},p_{5})))$

${\mathcal {I}}(\neg P)={\mathsf {T}}$ if, and only if, ${\mathcal {I}}(P)={\mathsf {F}}$

${\mathcal {I}}(P\land Q)={\mathsf {T}}$ if, and only if, ${\mathcal {I}}(P)={\mathsf {T}}$ and ${\mathcal {I}}(Q)={\mathsf {T}}$

${\mathcal {I}}(P\lor Q)={\mathsf {T}}$ if, and only if, ${\mathcal {I}}(P)={\mathsf {T}}$ or ${\mathcal {I}}(Q)={\mathsf {T}}$

${\mathcal {I}}(P\to Q)={\mathsf {T}}$ if, and only if, it is true that, if ${\mathcal {I}}(P)={\mathsf {T}}$ , then ${\mathcal {I}}(Q)={\mathsf {T}}$

${\mathcal {I}}(P\leftrightarrow Q)={\mathsf {T}}$ if, and only if, it is true that ${\mathcal {I}}(P)={\mathsf {T}}$ if, and only if, ${\mathcal {I}}(Q)={\mathsf {T}}$

The alpha set $\mathrm {A}$ is a countably infinite set of ${\mathcal {L}}$ 's or propositional variables. In the examples to follow, the elements of $\mathrm {A}$ are typically the letters $p$ , $q$ , $r$ , and so on.

atomic formulas

The omega set $Ω$ is a finite set of elements called or logical connectives. The set $Ω$ is partitioned into disjoint subsets as $\Omega =\Omega _{0}\cup \Omega _{1}\cup \cdots \cup \Omega _{j}\cup \cdots \cup \Omega _{m}.$ , where, $\Omega _{j}$ is the set of operator symbols of arity $j$ . For instance, a partition of $Ω$ for the typical five connectives would have $\Omega _{1}=\{\lnot \},$ and $\Omega _{2}\subseteq \{\land ,\lor ,\to ,\leftrightarrow \}.$ Also, the constant logical values are treated as operators of arity zero, so that $\Omega _{0}=\{\bot ,\top \}.$

operator symbols

Solvers[edit]

One notable difference between propositional calculus and predicate calculus is that satisfiability of a propositional formula is decidable.^[109] Deciding satisfiability of propositional logic formulas is an NP-complete problem. However, practical methods exist (e.g., DPLL algorithm, 1962; Chaff algorithm, 2001) that are very fast for many useful cases. Recent work has extended the SAT solver algorithms to work with propositions containing arithmetic expressions; these are the SMT solvers.

First-order logic

Second-order propositional logic

Second-order logic

Higher-order logic

Brown, Frank Markham (2003), Boolean Reasoning: The Logic of Boolean Equations, 1st edition, Kluwer Academic Publishers, Norwell, MA. 2nd edition, Dover Publications, Mineola, NY.

and Keisler, H.J. (1973), Model Theory, North-Holland, Amsterdam, Netherlands.

Chang, C.C.

Kohavi, Zvi (1978), Switching and Finite Automata Theory, 1st edition, McGraw–Hill, 1970. 2nd edition, McGraw–Hill, 1978.

(1974), Discrete Computational Structures, Academic Press, New York, NY.

Korfhage, Robert R.

and Scott, P.J. (1986), Introduction to Higher Order Categorical Logic, Cambridge University Press, Cambridge, UK.

Lambek, J.

Mendelson, Elliot (1964), Introduction to Mathematical Logic, D. Van Nostrand Company.

(2006), "Propositional Logic", in James Fieser and Bradley Dowden (eds.), Internet Encyclopedia of Philosophy, Eprint.

Klement, Kevin C.

contains a systematic formal development with axiomatic proof

Formal Predicate Calculus

, by P.D. Magnus, covers formal semantics and proof theory for sentential logic.

forall x: an introduction to formal logic

from Logic In Action

Chapter 2 / Propositional Logic

on Project Nayuki. (note: implication can be input in the form !X|Y, and a sequent can be a single formula prefixed with > and having no commas)