The propositional calculus is a branch of logic.[1] It is also called propositional logic, statement logic, sentential calculus,[2] sentential logic, or sometimes zeroth-order logic.[3] [4] It deals with propositions (which can be true or false) and relations between propositions,[5] including the construction of arguments based on them.[6] Compound propositions are formed by connecting propositions by logical connectives representing the truth functions of conjunction, disjunction, implication, biconditional, and negation.[7] [8] [9] [10] Some sources include other connectives, as in the table below.
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. While the atomic propositions are typically represented by letters of the alphabet, 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.
| Connective | Symbol | |
|---|---|---|
| AND | A\landB A ⋅ B AB A\&B A\&\&B | |
| equivalent | A\equivB A\LeftrightarrowB A\leftrightharpoonsB | |
| implies | A ⇒ B A\supsetB A → B | |
| NAND | A\overline{\land}B A\midB \overline{A ⋅ B} | |
| nonequivalent | A\not\equivB A\not\LeftrightarrowB A\nleftrightarrowB | |
| NOR | A\overline{\lor}B A\downarrowB \overline{A+B} | |
| NOT | \negA -A \overline{A} \simA | |
| OR | A\lorB A+B A\midB A\parallelB | |
| XNOR | A\odotB | |
| XOR | A\underline{\lor}B A ⊕ B |
The most thoroughly researched branch of propositional logic is classical truth-functional propositional logic, 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.[13] 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.
See main article: History of logic. Although propositional logic (also called propositional calculus) had been hinted by earlier philosophers, it was developed into a formal logic (Stoic logic) by Chrysippus in the 3rd century BC[14] and expanded by his successor Stoics. The logic was focused on propositions. This was different from the traditional syllogistic logic, which focused on terms. However, most of the original writings were lost[15] and, at some time between the 3rd and 6th century CE, Stoic logic faded into oblivion, to be resurrected only in the 20th century, in the wake of the (re)-discovery of propositional logic.
Symbolic logic, which would come to be important to refine propositional logic, was first developed by the 17th/18th-century mathematician Gottfried Leibniz, whose calculus ratiocinator was, however, unknown to the larger logical community. Consequently, many of the advances achieved by Leibniz were recreated by logicians like George Boole and Augustus De Morgan, completely independent of Leibniz.[16]
Gottlob Frege's predicate logic builds upon propositional logic, and has been described as combining "the distinctive features of syllogistic logic and propositional logic."[17] Consequently, predicate logic ushered in a new era in logic's history; however, advances in propositional logic were still made after Frege, including natural deduction, truth trees and truth tables. Natural deduction was invented by Gerhard Gentzen and Stanisław Jaśkowski. Truth trees were invented by Evert Willem Beth.[18] The invention of truth tables, however, is of uncertain attribution.
Within works by Frege[19] and Bertrand Russell,[20] are ideas influential to the invention of truth tables. The actual tabular structure (being formatted as a table), itself, is generally credited to either Ludwig Wittgenstein or Emil Post (or both, independently). Besides Frege and Russell, others credited with having ideas preceding truth tables include Philo, Boole, Charles Sanders Peirce,[21] and Ernst Schröder. Others credited with the tabular structure include Jan Łukasiewicz, Alfred North Whitehead, William Stanley Jevons, John Venn, and Clarence Irving Lewis. Ultimately, some have concluded, like John Shosky, that "It is far from clear that any one person should be given the title of 'inventor' of truth-tables.".
See main article: article and Proposition. Propositional logic, as currently studied in universities, is a specification of a standard of logical consequence in which only the meanings of propositional connectives are considered in evaluating the conditions for the truth of a sentence, or whether a sentence logically follows from some other sentence or group of sentences.
Propositional logic deals with statements, which are defined as declarative sentences having truth value.[22] Examples of statements might include:
Declarative sentences are contrasted with questions, such as "What is Wikipedia?", and imperative statements, such as "Please add citations to support the claims in this article.".[23] [24] Such non-declarative sentences have no truth value,[25] and are only dealt with in nonclassical logics, called erotetic and imperative logics.
See also: Atomic formula and Atomic sentence. In propositional logic, a statement can contain one or more other statements as parts. Compound sentences are formed from simpler sentences and express relationships among the constituent sentences.[26] This is done by combining them with logical connectives:[27] the main types of compound sentences are negations, conjunctions, disjunctions, implications, and biconditionals, which are formed by using the corresponding connectives to connect propositions.[28] [29] In English, these connectives are expressed by the words "and" (conjunction), "or" (disjunction), "not" (negation), "if" (material conditional), and "if and only if" (biconditional). Examples of such compound sentences might include:
If sentences lack any logical connectives, they are called simple sentences, or atomic sentences; if they contain one or more logical connectives, they are called compound sentences, or molecular sentences.
Sentential connectives are a broader category that includes logical connectives. Sentential connectives are any linguistic particles that bind sentences to create a new compound sentence, or that inflect a single sentence to create a new sentence. A logical connective, or propositional connective, is a kind of sentential connective with the characteristic feature that, when the original sentences it operates on are (or express) propositions, the new sentence that results from its application also is (or expresses) a proposition. Philosophers disagree about what exactly a proposition is, as well as about which sentential connectives in natural languages should be counted as logical connectives. Sentential connectives are also called sentence-functors, and logical connectives are also called truth-functors.
See main article: article and Argument. An argument is defined as a pair of things, namely a set of sentences, called the premises, and a sentence, called the conclusion.[30] The conclusion is claimed to follow from the premises, and the premises are claimed to support the conclusion.
The following is an example of an argument within the scope of propositional logic:
Premise 1: If it's raining, then it's cloudy.
Premise 2: It's raining.
Conclusion: It's cloudy.
The logical form of this argument is known as modus ponens, which is a classically valid form.[31] So, in classical logic, the argument is valid, although it may or may not be sound, depending on the meteorological facts in a given context. This example argument will be reused when explaining .
See main article: article, Validity (logic) and Soundness. An argument is valid if, and only if, it is necessary that, if all its premises are true, its conclusion is true.[32] Alternatively, an argument is valid if, and only if, it is impossible for all the premises to be true while the conclusion is false.
Validity is contrasted with soundness. An argument is sound if, and only if, it is valid and all its premises are true. Otherwise, it is unsound.
Logic, in general, aims to precisely specify valid arguments. This is done by defining a valid argument as one in which its conclusion is a logical consequence of its premises, which, when this is understood as semantic consequence, means that there is no case in which the premises are true but the conclusion is not true – see below.
Propositional logic is typically studied through a formal system in which formulas of a formal language are interpreted to represent propositions. This formal language is the basis for proof systems, which allow a conclusion to be derived from premises if, and only if, it is a logical consequence of them. This section will show how this works by formalizing the . The formal language for a propositional calculus will be fully specified in, and an overview of proof systems will be given in .
See main article: article and Propositional variable. Since propositional logic is not concerned with the structure of propositions beyond the point where they cannot be decomposed any more by logical connectives, it is typically studied by replacing such atomic (indivisible) statements with letters of the alphabet, which are interpreted as variables representing statements (propositional variables). With propositional variables, the would then be symbolized as follows:
Premise 1:
P\toQ
Premise 2:
P
Conclusion:
Q
When is interpreted as "It's raining" and as "it's cloudy" these symbolic expressions correspond exactly with the original expression in natural language. Not only that, but they will also correspond with any other inference with the same logical form.
When a formal system is used to represent formal logic, only statement letters (usually capital roman letters such as
P
Q
R
If we assume that the validity of modus ponens has been accepted as an axiom, then the same can also be depicted like this:
| P\toQ,P | |
| Q |
This method of displaying it is Gentzen's notation for natural deduction and sequent calculus. The premises are shown above a line, called the inference line, separated by a comma, which indicates combination of premises. The conclusion is written below the inference line. The inference line represents syntactic consequence, sometimes called deductive consequence,[33] which is also symbolized with ⊢.[34] So the above can also be written in one line as
P\toQ,P\vdashQ
Syntactic consequence is contrasted with semantic consequence, which is symbolized with ⊧. In this case, the conclusion follows syntactically because the natural deduction inference rule of modus ponens has been assumed. For more on inference rules, see the sections on proof systems below.
The language (commonly called
l{L}
A well-formed formula is any atomic formula, or any formula that can be built up from atomic formulas by means of operator symbols according to the rules of the grammar. The language
l{L}
Usually the syntax of
l{L}
Given a set of atomic propositional variables
p1
p2
p3
| 1 | |
| c | |
| 1 |
| 1 | |
| c | |
| 2 |
| 1 | |
| c | |
| 3 |
| 2 | |
| c | |
| 1 |
| 2 | |
| c | |
| 2 |
| 2 | |
| c | |
| 3 |
| 3 | |
| c | |
| 1 |
| 3 | |
| c | |
| 2 |
| 3 | |
| c | |
| 3 |
Definition 1: Atomic propositional variables are formulas.
Definition 2: If
| m | |
| c | |
| n |
\langle
\rangle
| m | |
| c | |
| n |
\langle
\rangle
Definition 3: Nothing else is a formula.
Writing the result of applying
| m | |
| c | |
| n |
\langle
\rangle
| m | |
| c | |
| n |
p5
| 2(p | |
| c | |
| 2, |
p9)
| 2(p | |
| c | |
| 1, |
| 1(p | |
| c | |
| 3)) |
| 3(p | |
| c | |
| 4, |
p6,
| 2(p | |
| c | |
| 1, |
p2))
| 1(p | |
| c | |
| 7), |
| 1(p | |
| c | |
| 8)) |
| 2(p | |
| c | |
| 3, |
p4),
| 1(p | |
| c | |
| 5), |
| 2(p | |
| c | |
| 6, |
p7))
| 3(p | |
| c | |
| 2, |
p3,
| 2(p | |
| c | |
| 4, |
p5)))
What was given as Definition 2 above, which is responsible for the composition of formulas, is referred to by Colin Howson as the principle of composition. It is this recursion in the definition of a language's syntax which justifies the use of the word "atomic" to refer to propositional variables, since all formulas in the language
l{L}
The definition that "nothing else is a formula", given above as Definition 3, excludes any formula from the language which is not specifically required by the other definitions in the syntax. In particular, it excludes infinitely long formulas from being well-formed.
An alternative to the syntax definitions given above is to write a context-free (CF) grammar for the language
l{L}
\phi::=a1,a2,\ldots~|~\neg\phi~|~\phi~\&~\psi~|~\phi\vee\psi~|~\phi → \psi~|~\phi\leftrightarrow\psi
\phi
\phi
|~\Box\phi~|~\Diamond\phi
Mathematicians sometimes distinguish between propositional constants, propositional variables, and schemata. Propositional constants represent some particular proposition,[42] while propositional variables range over the set of all atomic propositions. Schemata, or schematic letters, however, range over all formulas.[43] (Schematic letters are also called metavariables.) It is common to represent propositional constants by,, and, propositional variables by,, and, and schematic letters are often Greek letters, most often,, and .
However, some authors recognize only two "propositional constants" in their formal system: the special symbol
\top
\bot
See main article: article, Semantics of logic and Model theory. To serve as a model of the logic of a given natural language, a formal language must be semantically interpreted. In classical logic, all propositions evaluate to exactly one of two truth-values: True or False. For example, "Wikipedia is a free online encyclopedia that anyone can edit" evaluates to True,[47] while "Wikipedia is a paper encyclopedia" evaluates to False.[48]
In other respects, the following formal semantics can apply to the language of any propositional logic, but the assumptions that there are only two semantic values (bivalence), that only one of the two is assigned to each formula in the language (noncontradiction), and that every formula gets assigned a value (excluded middle), are distinctive features of classical logic. To learn about nonclassical logics with more than two truth-values, and their unique semantics, one may consult the articles on "Many-valued logic", "Three-valued logic", "Finite-valued logic", and "Infinite-valued logic".
See main article: Interpretation (logic). For a given language
l{L}
l{L}
l{L}
l{L}
l{V}=\{T,F\}
l{V}=\{1,0\}
For
n
2n
a
21=2
a
a
a
b
22=4
a
b
a
b
l{L}
\aleph0
| \aleph0 | |
| 2 |
=akc
l{L}
Where
l{I}
\varphi
\psi
\langle\{\varphi1,\varphi2,\varphi3,...,\varphin\},\psi\rangle
\{\varphi1,\varphi2,\varphi3,...,\varphin\}
\psi
\{\varphi1,\varphi2,\varphi3,...,\varphin\}\models\psi
l{I}
\{\varphi1,\varphi2,\varphi3,...,\varphin\}
\psi
See main article: article, Logical connective and Truth function. An interpretation assigns semantic values to atomic formulas directly. Molecular formulas are assigned a function of the value of their constituent atoms, according to the connective used; the connectives are defined in such a way that the truth-value of a sentence formed from atoms with connectives depends on the truth-values of the atoms that they're applied to, and only on those. This assumption is referred to by Colin Howson as the assumption of the truth-functionality of the connectives.
Since logical connectives are defined semantically only in terms of the truth values that they take when the propositional variables that they're applied to take either of the two possible truth values, the semantic definition of the connectives is usually represented as a truth table for each of the connectives, as seen below:
| p | q | p ∧ q | p ∨ q | p → q | p ↔ q | ¬p | ¬q | |
|---|---|---|---|---|---|---|---|---|
| T | T | T | T | T | T | F | F | |
| T | F | F | T | F | F | F | T | |
| F | T | F | T | T | F | T | F | |
| F | F | F | F | T | T | T | T |
This table covers each of the main five logical connectives: conjunction (here notated p ∧ q), disjunction (p ∨ q), implication (p → q), biconditional (p ↔ q) and negation, (¬p, or ¬q, as the case may be). It is sufficient for determining the semantics of each of these operators. For more truth tables for more different kinds of connectives, see the article "Truth table".
Some authors (viz., all the authors cited in this subsection) write out the connective semantics using a list of statements instead of a table. In this format, where
l{I}(\varphi)
\varphi
l{I}(\negP)=T
l{I}(P)=F
l{I}(P\landQ)=T
l{I}(P)=T
l{I}(Q)=T
l{I}(P\lorQ)=T
l{I}(P)=T
l{I}(Q)=T
l{I}(P\toQ)=T
l{I}(P)=T
l{I}(Q)=T
l{I}(P\leftrightarrowQ)=T
l{I}(P)=T
l{I}(Q)=T
l{I}(\varphi)
\varphi
|\varphi|
l{I}(\varphi)=T
\varphi
T
ak{M}
ak{M}\models\varphi
l{I}(\varphi)=T
l{I}
ak{M}
Some of these connectives may be defined in terms of others: for instance, implication, p → q, may be defined in terms of disjunction and negation, as ¬p ∨ q;[57] and disjunction may be defined in terms of negation and conjunction, as ¬(¬p ∧ ¬q). In fact, a truth-functionally complete system, in the sense that all and only the classical propositional tautologies are theorems, may be derived using only disjunction and negation (as Russell, Whitehead, and Hilbert did), or using only implication and negation (as Frege did), or using only conjunction and negation, or even using only a single connective for "not and" (the Sheffer stroke), as Jean Nicod did. A joint denial connective (logical NOR) will also suffice, by itself, to define all other connectives, but no other connectives have this property.
Some authors, namely Howson and Cunningham,[58] distinguish equivalence from the biconditional. (As to equivalence, Howson calls it "truth-functional equivalence", while Cunningham calls it "logical equivalence".) Equivalence is symbolized with ⇔ and is a metalanguage symbol, while a biconditional is symbolized with ↔ and is a logical connective in the object language
l{L}
Given
\varphi
\psi
l{L}
l{I}
l{L}
\varphi
l{L}
l{I}
l{I}
\varphi
\varphi
l{I}
l{I}
\varphi
\varphi
l{I}
\neg\varphi
l{I}
\varphi
l{I}
\varphi
l{I}
\psi
l{L}
\varphi\models\psi
\varphi
\varphi
\psi
\varphi
l{L}
\models\varphi
l{L}
(p\land\negp)
For interpretations (cases)
l{I}
l{L}
l{I}
\varphi
l{I}
\neg\varphi
l{I}
\varphi
l{L}
l{I}
\varphi
l{L}
\varphi
\neg\varphi
l{I}
For classical logic, which assumes that all cases are complete and consistent, the following theorems apply:
\varphi
l{I}
\neg\varphi
l{I}
\neg\varphi
l{I}
\varphi
l{I}
\varphi
(\varphi\to\psi)
l{I}
\psi
l{I}
\models\varphi
\models(\varphi\to\psi)
\models\psi
(\varphi\to\psi)
l{I}
\varphi
l{I}
\psi
l{I}
\varphi\models\psi
(\varphi\to\psi)
\varphi\models\psi
\models(\varphi\to\psi)
See also: Proof theory and Proof calculus. Proof systems in propositional logic can be broadly classified into semantic proof systems and syntactic proof systems,[65] [66] [67] according to the kind of logical consequence that they rely on: semantic proof systems rely on semantic consequence (
\varphi\models\psi
\varphi\vdash\psi
Semantic proof systems rely on the concept of semantic consequence, symbolized as
\varphi\models\psi
\varphi
\psi
See main article: article and Truth table. A truth table is a semantic proof method used to determine the truth value of a propositional logic expression in every possible scenario.[69] By exhaustively listing the truth values of its constituent atoms, a truth table can show whether a proposition is true, false, tautological, or contradictory.[70] See .
See main article: article and Method of analytic tableaux. A semantic tableau is another semantic proof technique that systematically explores the truth of a proposition.[71] It constructs a tree where each branch represents a possible interpretation of the propositions involved.[72] If every branch leads to a contradiction, the original proposition is considered to be a contradiction, and its negation is considered a tautology.[73] See .
Syntactic proof systems, in contrast, focus on the formal manipulation of symbols according to specific rules. The notion of syntactic consequence,
\varphi\vdash\psi
\psi
\varphi
See main article: article and Axiomatic system (logic). An axiomatic system is a set of axioms or assumptions from which other statements (theorems) are logically derived.[74] In propositional logic, axiomatic systems define a base set of propositions considered to be self-evidently true, and theorems are proved by applying deduction rules to these axioms.[75] See .
See main article: article and Natural deduction. Natural deduction is a syntactic method of proof that emphasizes the derivation of conclusions from premises through the use of intuitive rules reflecting ordinary reasoning.[76] Each rule reflects a particular logical connective and shows how it can be introduced or eliminated. See .
See main article: article and Sequent calculus. The sequent calculus is a formal system that represents logical deductions as sequences or "sequents" of formulas.[77] Developed by Gerhard Gentzen, this approach focuses on the structural properties of logical deductions and provides a powerful framework for proving statements within propositional logic.[78]
See also: Truth table.
Taking advantage of the semantic concept of validity (truth in every interpretation), it is possible to prove a formula's validity by using a truth table, which gives every possible interpretation (assignment of truth values to variables) of a formula. If, and only if, all the lines of a truth table come out true, the formula is semantically valid (true in every interpretation). Further, if (and only if)
\neg\varphi
\varphi
For instance, this table shows that "p → (q ∨ r → (r → ¬p))" is not valid:
| p | q | r | q ∨ r | r → ¬p | q ∨ r → (r → ¬p) | p → (q ∨ r → (r → ¬p)) | |
|---|---|---|---|---|---|---|---|
| T | T | T | T | F | F | F | |
| T | T | F | T | T | T | T | |
| T | F | T | T | F | F | F | |
| T | F | F | F | T | T | T | |
| F | T | T | T | T | T | T | |
| F | T | F | T | T | T | T | |
| F | F | T | T | T | T | T | |
| F | F | F | F | T | T | T |
The computation of the last column of the third line may be displayed as follows:
| p | → | (q | ∨ | r | → | (r | → | ¬ | p)) | |
|---|---|---|---|---|---|---|---|---|---|---|
| T | → | (F | ∨ | T | → | (T | → | ¬ | T)) | |
| T | → | ( | T | → | (T | → | F | )) | ||
| T | → | ( | T | → | F | ) | ||||
| T | → | F | ||||||||
| F | ||||||||||
| T | F | F | T | T | F | T | F | F | T |
Further, using the theorem that
\varphi\models\psi
(\varphi\to\psi)
\{\varphi1,\varphi2,\varphi3,...,\varphin\}\models\psi
\left(\left(wedge
| n | |
| i=1 |
\varphii\right) → \psi\right)
\models\left(\left(wedge
| n | |
| i=1 |
\varphii\right) → \psi\right)
See main article: article and Method of analytic tableaux. Since truth tables have 2n lines for n variables, they can be tiresomely long for large values of n. Analytic tableaux are a more efficient, but nevertheless mechanical,[84] semantic proof method; they take advantage of the fact that "we learn nothing about the validity of the inference from examining the truth-value distributions which make either the premises false or the conclusion true: the only relevant distributions when considering deductive validity are clearly just those which make the premises true or the conclusion false."
Analytic tableaux for propositional logic are fully specified by the rules that are stated in schematic form below. These rules use "signed formulas", where a signed formula is an expression
TX
FX
X
l{L}
TX
X
FX
X
TX
X
X
FX
X
X
\begin{align} &1)
| T\simX | |
| FX |
&&
| F\simX | |
| TX |
\\ \phantom{spacer}\\ &2)
| T(X\landY) | |
| \begin{matrix |
TX\ TY\end{matrix}} &&
| F(X\landY) | |
| FX|FY |
\\ \phantom{spacer}\\ &3)
| T(X\lorY) | |
| TX|TY |
&&
| F(X\lorY) | |
| \begin{matrix |
FX\ FY\end{matrix}}\\ \phantom{spacer}\\ &4)
| T(X\supsetY) | |
| FX|TY |
&&
| F(X\supsetY) | |
| \begin{matrix |
TX\ FY\end{matrix}} \end{align}
In this notation, rule 2 means that
T(X\landY)
TX,TY
F(X\landY)
FX,FY
T\varphi
\varphi
F\varphi
\neg\varphi
One constructs a tableau for a set of formulas by applying the rules to produce more lines and tree branches until every line has been used, producing a complete tableau. In some cases, a branch can come to contain both
TX
FX
X
To construct a tableau for an argument
\langle\{\varphi1,\varphi2,\varphi3,...,\varphin\},\psi\rangle
\{\varphi1,\varphi2,\varphi3,...,\varphin\}
T
T\varphi
T\varphi
\psi
F
F\psi
\varphi\models\psi
\{\varphi,\sim\psi\}
\varphi,\sim\psi\models
Using semantic checking methods, such as truth tables or semantic tableaux, to check for tautologies and semantic consequences, it can be shown that, in classical logic, the following classical argument forms are semantically valid, i.e., these tautologies and semantic consequences hold. We use
\varphi
\psi
\varphi
\psi
\varphi\models\psi
\psi\models\varphi
| Name | Sequent | Description | |
|---|---|---|---|
| Modus Ponens | ((p\toq)\landp)\modelsq | If then ; ; therefore | |
| Modus Tollens | ((p\toq)\land\negq)\models\negp | If then ; not ; therefore not | |
| Hypothetical Syllogism | ((p\toq)\land(q\tor))\models(p\tor) | If then ; if then ; therefore, if then | |
| Disjunctive Syllogism | ((p\lorq)\land\negp)\modelsq | Either or, or both; not ; therefore, | |
| Constructive Dilemma | ((p\toq)\land(r\tos)\land(p\lorr))\models(q\lors) | If then ; and if then ; but or ; therefore or | |
| Destructive Dilemma | ((p\toq)\land(r\tos)\land(\negq\lor\negs))\models(\negp\lor\negr) | If then ; and if then ; but not or not ; therefore not or not | |
| Bidirectional Dilemma | ((p\toq)\land(r\tos)\land(p\lor\negs))\models(q\lor\negr) | If then ; and if then ; but or not ; therefore or not | |
| Simplification | (p\landq)\modelsp | and are true; therefore is true | |
| Conjunction | p,q\models(p\landq) | and are true separately; therefore they are true conjointly | |
| Addition | p\models(p\lorq) | is true; therefore the disjunction (or) is true | |
| Composition | ((p\toq)\land(p\tor))\models(p\to(q\landr)) | If then ; and if then ; therefore if is true then and are true | |
| De Morgan's Theorem (1) | \neg(p\landq) (\negp\lor\negq) | The negation of (and) is equiv. to (not or not) | |
| De Morgan's Theorem (2) | \neg(p\lorq) (\negp\land\negq) | The negation of (or) is equiv. to (not and not) | |
| Commutation (1) | (p\lorq) (q\lorp) | (or) is equiv. to (or) | |
| Commutation (2) | (p\landq) (q\landp) | (and) is equiv. to (and) | |
| Commutation (3) | (p\leftrightarrowq) (q\leftrightarrowp) | (iff) is equiv. to (iff) | |
| Association (1) | (p\lor(q\lorr)) ((p\lorq)\lorr) | or (or) is equiv. to (or) or | |
| Association (2) | (p\land(q\landr)) ((p\landq)\landr) | and (and) is equiv. to (and) and | |
| Distribution (1) | (p\land(q\lorr)) ((p\landq)\lor(p\landr)) | and (or) is equiv. to (and) or (and) | |
| Distribution (2) | (p\lor(q\landr)) ((p\lorq)\land(p\lorr)) | or (and) is equiv. to (or) and (or) | |
| Double Negation | p \neg\negp | is equivalent to the negation of not | |
| Transposition | (p\toq) (\negq\to\negp) | If then is equiv. to if not then not | |
| Material Implication | (p\toq) (\negp\lorq) | If then is equiv. to not or | |
| Material Equivalence (1) | (p\leftrightarrowq) ((p\toq)\land(q\top)) | is equiv. to (if is true then is true) and (if is true then is true) | |
| Material Equivalence (2) | (p\leftrightarrowq) ((p\landq)\lor(\negp\land\negq)) | is equiv. to either (and are true) or (both and are false) | |
| Material Equivalence (3) | (p\leftrightarrowq) ((p\lor\negq)\land(\negp\lorq)) | is equiv to., both (or not is true) and (not or is true) | |
| Exportation | ((p\landq)\tor)\models(p\to(q\tor)) | from (if and are true then is true) we can prove (if is true then is true, if is true) | |
| Importation | (p\to(q\tor)) ((p\landq)\tor) | If then (if then) is equivalent to if and then | |
| Tautology (1) | p (p\lorp) | is true is equiv. to is true or is true | |
| Tautology (2) | p (p\landp) | is true is equiv. to is true and is true | |
| Tertium non datur (Law of Excluded Middle) | \models(p\lor\negp) | or not is true | |
| Law of Non-Contradiction | \models\neg(p\land\negp) | and not is false, is a true statement | |
| Explosion | (p\land\negp)\modelsq | and not ; therefore |
See main article: article and Natural deduction. Natural deduction, since it is a method of syntactical proof, is specified by providing inference rules (also called rules of proof) for a language with the typical set of connectives
\{-,\&,\lor,\to,\leftrightarrow\}
Different authors vary to some extent regarding which inference rules they give, which will be noted. More striking to the look and feel of a proof, however, is the variation in notation styles. The, which was covered earlier for a short argument, can actually be stacked to produce large tree-shaped natural deduction proofs—not to be confused with "truth trees", which is another name for analytic tableaux. There is also a style due to Stanisław Jaśkowski, where the formulas in the proof are written inside various nested boxes, and there is a simplification of Jaśkowski's style due to Fredric Fitch (Fitch notation), where the boxes are simplified to simple horizontal lines beneath the introductions of suppositions, and vertical lines to the left of the lines that are under the supposition. Lastly, there is the only notation style which will actually be used in this article, which is due to Patrick Suppes, but was much popularized by E.J. Lemmon and Benson Mates.[91] This method has the advantage that, graphically, it is the least intensive to produce and display, which made it a natural choice for the editor who wrote this part of the article, who did not understand the complex LaTeX commands that would be required to produce proofs in the other methods.
A proof, then, laid out in accordance with the Suppes–Lemmon notation style, is a sequence of lines containing sentences, where each sentence is either an assumption, or the result of applying a rule of proof to earlier sentences in the sequence. Each line of proof is made up of a sentence of proof, together with its annotation, its assumption set, and the current line number. The assumption set lists the assumptions on which the given sentence of proof depends, which are referenced by the line numbers. The annotation specifies which rule of proof was applied, and to which earlier lines, to yield the current sentence. See the .
Natural deduction inference rules, due ultimately to Gentzen, are given below. There are ten primitive rules of proof, which are the rule assumption, plus four pairs of introduction and elimination rules for the binary connectives, and the rule reductio ad adbsurdum. Disjunctive Syllogism can be used as an easier alternative to the proper ∨-elimination, and MTT and DN are commonly given rules, although they are not primitive.
| Rule Name | Alternative names | Annotation | Assumption set | Statement | |
|---|---|---|---|---|---|
| Rule of Assumptions | Assumption | A | The current line number. | At any stage of the argument, introduce a proposition as an assumption of the argument. | |
| Conjunction introduction | Ampersand introduction, conjunction (CONJ)[92] | m, n &I<ref name=":35" /> | The union of the assumption sets at lines m and n. | From \varphi \psi \varphi~\&~\psi | |
| Conjunction elimination | Simplification (S), ampersand elimination | m &E<ref name=":35" /> | The same as at line m. | From \varphi~\&~\psi \varphi \psi | |
| Disjunction introduction | Addition (ADD) | m ∨I | The same as at line m. | From \varphi \varphi\lor\psi \psi | |
| Disjunction elimination | Wedge elimination, dilemma (DL) | j,k,l,m,n ∨E | The lines j,k,l,m,n. | From \varphi\lor\psi \varphi \chi \varphi \psi \chi \psi \chi | |
| Disjunctive Syllogism | Wedge elimination (∨E), modus tollendo ponens (MTP) | m,n DS | The union of the assumption sets at lines m and n. | From \varphi\lor\psi -\varphi \psi \varphi\lor\psi -\psi \varphi | |
| Arrow elimination | Modus ponendo ponens (MPP), modus ponens (MP), conditional elimination | m, n →E | The union of the assumption sets at lines m and n. | From \varphi\to\psi \varphi \psi | |
| Arrow introduction | Conditional proof (CP), conditional introduction | n, →I (m) | Everything in the assumption set at line n, excepting m, the line where the antecedent was assumed. | From \psi \varphi \varphi\to\psi | |
| Reductio ad absurdum | Indirect Proof (IP), negation introduction (−I), negation elimination (−E) | m, n RAA (k) | The union of the assumption sets at lines m and n, excluding k (the denied assumption). | From a sentence and its denial at lines m and n, infer the denial of any assumption appearing in the proof (at line k). | |
| Double arrow introduction | Biconditional definition (Df ↔), biconditional introduction | m, n ↔ I | The union of the assumption sets at lines m and n. | From \varphi\to\psi \psi\to\varphi \varphi\leftrightarrow\psi | |
| Double arrow elimination | Biconditional definition (Df ↔), biconditional elimination | m ↔ E | The same as at line m. | From \varphi\leftrightarrow\psi \varphi\to\psi \psi\to\varphi | |
| Double negation | Double negation elimination | m DN | The same as at line m. | From --\varphi \varphi | |
| Modus tollendo tollens | Modus tollens (MT) | m, n MTT | The union of the assumption sets at lines m and n. | From \varphi\to\psi -\psi -\varphi |
The proof below derives
-P
P\toQ
-Q
| Assumption set | Line number | Sentence of proof | Annotation | |
|---|---|---|---|---|
P\toQ | A | |||
-Q | A | |||
P | A | |||
| , | Q | , →E | ||
| , | -P | , RAA |
See main article: article and Axiomatic system (logic). It is possible to perform proofs axiomatically, which means that certain tautologies are taken as self-evident and various others are deduced from them using modus ponens as an inference rule, as well as a rule of substitution, which permits replacing any well-formed formula with any of it. Alternatively, one uses axiom schemas instead of axioms, and no rule of substitution is used.
This section gives the axioms of some historically notable axiomatic systems for propositional logic. For more examples, as well as metalogical theorems that are specific to such axiomatic systems (such as their completeness and consistency), see the article Axiomatic system (logic).
Although axiomatic proof has been used since the famous Ancient Greek textbook, Euclid's Elements of Geometry, in propositional logic it dates back to Gottlob Frege's 1879 Begriffsschrift.[93] Frege's system used only implication and negation as connectives, and it had six axioms, which were these ones:[94] [95]
a\supset(b\supseta)
(c\supset(b\supseta))\supset((c\supsetb)\supset(c\supseta))
(d\supset(b\supseta))\supset(b\supset(d\supseta))
(b\supseta)\supset(\nega\supset\negb)
\neg\nega\supseta
a\supset\neg\nega
These were used by Frege together with modus ponens and a rule of substitution (which was used but never precisely stated) to yield a complete and consistent axiomatization of classical truth-functional propositional logic.
Jan Łukasiewicz showed that, in Frege's system, "the third axiom is superfluous since it can be derived from the preceding two axioms, and that the last three axioms can be replaced by the single sentence
CCNpNqCpq
(\negp → \negq) → (p → q)
p\to(q\top)
(p\to(q\tor))\to((p\toq)\to(p\tor))
(\negp\to\negq)\to(q\top)
Just like Frege's system, this system uses a substitution rule and uses modus ponens as an inference rule. The exact same system was given (with an explicit substitution rule) by Alonzo Church,[96] who referred to it as the system P2,[97] and helped popularize it.
One may avoid using the rule of substitution by giving the axioms in schematic form, using them to generate an infinite set of axioms. Hence, using Greek letters to represent schemata (metalogical variables that may stand for any well-formed formulas), the axioms are given as:
\varphi\to(\psi\to\varphi)
(\varphi\to(\psi\to\chi))\to((\varphi\to\psi)\to(\varphi\to\chi))
(\neg\varphi\to\neg\psi)\to(\psi\to\varphi)
The schematic version of P2 is attributed to John von Neumann, and is used in the Metamath "set.mm" formal proof database. It has also been attributed to Hilbert,[98] and named
l{H}
As an example, a proof of
A\toA
(A1)
(p\to(q\top))
(A2)
((p\to(q\tor))\to((p\toq)\to(p\tor)))
(A3)
((\negp\to\negq)\to(q\top))
And the proof is as follows:
A\to((B\toA)\toA)
(A\to((B\toA)\toA))\to((A\to(B\toA))\to(A\toA))
(A\to(B\toA))\to(A\toA)
A\to(B\toA)
A\toA
One notable difference between propositional calculus and predicate calculus is that satisfiability of a propositional formula is decidable.[99] 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.
!X|Y, and a sequent can be a single formula prefixed with > and having no commas)