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,^[4][1] or sometimes zeroth-order logic.^[b][6][7][8] Sometimes, it is called first-order propositional logic^[9] to contrast it with System F, but it should not be confused with first-order logic. It deals with propositions^[1] (which can be true or false)^[10] and relations between propositions,^[11] including the construction of arguments based on them.^[12] Compound propositions are formed by connecting propositions by logical connectives representing the truth functions of conjunction, disjunction, implication, biconditional, and negation.^{[13][14][15][16]} 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,^[c] in which propositions are represented by letters, which are called propositional variables. These are then used, together with symbols for connectives, to make propositional formula. Because of this, the propositional variables are called atomic formulas of a formal propositional language.^[14][2] While the atomic propositions are typically represented by letters of the alphabet,^[d][14] 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.

Notational variants of the connectives^[e][17][18]

Connective	Symbol
AND	${\displaystyle A\land B}$, ${\displaystyle A\cdot B}$, ${\displaystyle AB}$, ${\displaystyle A\&B}$, ${\displaystyle A\&\&B}$
equivalent	${\displaystyle A\equiv B}$, ${\displaystyle A\Leftrightarrow B}$, ${\displaystyle A\leftrightharpoons B}$
implies	${\displaystyle A\Rightarrow B}$, ${\displaystyle A\supset B}$, ${\displaystyle A\rightarrow B}$
NAND	${\displaystyle A{\overline {\land }}B}$, ${\displaystyle A\mid B}$, ${\displaystyle {\overline {A\cdot B}}}$
nonequivalent	${\displaystyle A\not \equiv B}$, ${\displaystyle A\not \Leftrightarrow B}$, ${\displaystyle A\nleftrightarrow B}$
NOR	${\displaystyle A{\overline {\lor }}B}$, ${\displaystyle A\downarrow B}$, ${\displaystyle {\overline {A+B}}}$
NOT	${\displaystyle \neg A}$, ${\displaystyle -A}$, ${\displaystyle {\overline {A}}}$, ${\displaystyle \sim A}$
OR	${\displaystyle A\lor B}$, ${\displaystyle A+B}$, ${\displaystyle A\mid B}$, ${\displaystyle A\parallel B}$
XNOR	${\displaystyle A\odot B}$
XOR	${\displaystyle A{\underline {\lor }}B}$, ${\displaystyle A\oplus B}$

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.^[19] 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.^[7][8]

Cite error: There are <ref group=lower-alpha> tags or {{efn}} templates on this page, but the references will not show without a {{reflist|group=lower-alpha}} template or {{notelist}} template (see the help page).