= Propositional logic
{wiki}
<Propositional logic> studies reasoning with whole <propositions> represented by letters such as $p$ and $q$, and <propositional formulas> built from them using <logical connectives>. The classical two-valued, truth-functional presentation below assigns each primitive <proposition> either true or false: each compound value depends only on its component values. This is <classical propositional logic>; other systems, including <Intuitionistic propositional logic>, have different semantics and rules.
Starting with $p$ and $q$, one can build $\neg p$ by <logical negation>, $p\land q$ by <logical conjunction>, $p\lor q$ by <logical disjunction>, and $p\to q$ by <logical implication>, then combine these into larger <propositional formulas>. Parentheses specify the construction: $(p\to q)\land p$ has <logical conjunction> as its outermost <logical connective>. Primitive <propositions> have no internal structure in this language; a <first-order formula> can additionally describe objects and quantify over them. The formation rules are given in https://forallx.openlogicproject.org/html/Ch6.html[forall x: Calgary, chapter 6].
The following <truth table> shows the four basic <logical connectives>. <Logical disjunction> is inclusive: $p\lor q$ is true when either or both inputs are true. Classical <logical implication> has exactly the same values as $\neg p\lor q$; its only false row has $p$ true and $q$ false. These truth conditions are specified in https://forallx.openlogicproject.org/html/Ch9.html[forall x: Calgary, chapter 9].
\Image[/propositional-connective-truth-table.png]
{title=Classical <logical connectives> on all four <Boolean valuations>, with matching columns for $p\to q$ and $\neg p\lor q$}
Evaluate $(p\to q)\land p$ from the inside out: first the <logical implication>, then the outer <logical conjunction>. The final column also tests the <logical implication> expressing the <modus ponens rule>:
$$
\begin{array}{cc|c|c|c}
p&q&p\to q&(p\to q)\land p&((p\to q)\land p)\to q\\\hline
\mathrm T&\mathrm T&\mathrm T&\mathrm T&\mathrm T\\
\mathrm T&\mathrm F&\mathrm F&\mathrm F&\mathrm T\\
\mathrm F&\mathrm T&\mathrm T&\mathrm F&\mathrm T\\
\mathrm F&\mathrm F&\mathrm T&\mathrm F&\mathrm T
\end{array}
$$
At $p=\mathrm T,q=\mathrm F$, the <logical implication> is false, so the <logical conjunction> is false. The <abstract syntax tree> below separates the construction of the <propositional formula> from the values propagated through it. Both occurrences of $p$ receive the same value from the <Boolean valuation>. With the opposite assignment $p=\mathrm F,q=\mathrm T$, the <logical implication> is true but the <logical conjunction> is still false because its second input $p$ is false. Recursive evaluation and exhaustive <truth tables> are explained in https://forallx.openlogicproject.org/html/Ch11.html[forall x: Calgary, chapter 11].
\Image[/propositional-formula-evaluation-tree.png]
{title=An <abstract syntax tree> evaluating $(p\to q)\land p$ to false at the <Boolean valuation> $p=\mathrm T,q=\mathrm F$}
The last column is always true: $((p\to q)\land p)\to q$ is a <tautology>. This expresses the <logical validity> of the <modus ponens rule>: whenever both premises $p\to q$ and $p$ are true, $q$ is true. It does not say the premises are true under every <Boolean valuation>; their <logical conjunction> is true only on the first row. For a short <natural deduction> proof outline, assume $(p\to q)\land p$, extract both conjuncts, apply the <implication elimination rule> to obtain $q$, then discharge the assumption by the <implication introduction rule>. See https://forallx.openlogicproject.org/html/Ch17.html[forall x: Calgary, sections 17.3–17.5].
Three tests answer different questions: <Boolean satisfiability> requires at least one true row, a <tautology> requires every row true, and a <contradiction> has every row false. Thus $p\lor\neg p$ is a <tautology>, $p\land\neg p$ is a <contradiction>, and $p\land q$ is satisfiable but not a <tautology>: it is true only at $p=q=\mathrm T$. See https://forallx.openlogicproject.org/html/Ch12.html[forall x: Calgary, sections 12.1–12.4].
<Propositional logic> is useful because an inference pattern can be checked once and reused for many choices of <propositions>. Its beauty is that a finite <truth table> completely settles classical truth-functional questions about a fixed <propositional formula>. But <logical validity> does not verify real atomic claims. If $p$ means “the switch is closed” and $q$ means “the lamp is lit”, a valid use of the <modus ponens rule> still requires establishing its premises about the apparatus; the <truth table> supplies neither an observation nor a causal explanation. See https://forallx.openlogicproject.org/html/Ch2.html[forall x: Calgary, chapter 2] and https://forallx.openlogicproject.org/html/Ch10.html[chapter 10].
Back to article page
