At the foundational roots of mathematical thought lies a profound dualism: the tension between syntactic deduction—the mechanical manipulation of uninterpreted typographical marks according to rigid inferential rules—and semantic truth—the assignment of meaning, reality, and truth-values in an interpretative universe. Classical propositional calculus represents the atomic crucible where this dualism is resolved through the twin theorems of Soundness and Semantic Completeness.
1. The Formal Syntax of Propositional Logic
To eliminate the ambiguities and semantic contaminations of natural human language, modern mathematical logic begins with a strictly defined formal language $mathcal{L}_0$. The alphabet of $mathcal{L}_0$ consists of three disjoint sets:
- A countably infinite set of propositional variables: $text{Var} = {P_1, P_2, P_3, dots, Q, R, dots}$.
- Logical connectives: Negation ($neg$), Conjunction ($land$), Disjunction ($lor$), Implication ($to$), and optionally Biconditional ($leftrightarrow$).
- Punctuation symbols: Left and right parentheses $(, )$.
The set of well-formed formulas (WFFs), denoted $text{Form}(mathcal{L}_0)$, is defined inductively as the smallest set satisfying:
- If $P in text{Var}$, then $P in text{Form}(mathcal{L}_0)$ (Atomic formulas).
- If $phi in text{Form}(mathcal{L}_0)$, then $(neg phi) in text{Form}(mathcal{L}_0)$.
- If $phi, psi in text{Form}(mathcal{L}_0)$ and $circ in {land, lor, to, leftrightarrow}$, then $(phi circ psi) in text{Form}(mathcal{L}_0)$.
By the Unique Readability Theorem, for every formula $phi in text{Form}(mathcal{L}_0)$, there exists a unique construction tree, guaranteeing that no formula can be parsed ambiguously.
2. Formal Semantics: Valuations & Truth Tables
Semantics endows the syntactic skeleton with values. A truth valuation is a set-theoretic function $v: text{Var} to {0, 1}$, assigning to each propositional variable either False ($0$) or True ($1$).
By the principle of truth-functionality, any valuation $v$ extends uniquely to a homomorphism $bar{v}: text{Form}(mathcal{L}_0) to {0, 1}$ defined recursively:
[
bar{v}(neg phi) = 1 – bar{v}(phi)
]
[
bar{v}(phi land psi) = min(bar{v}(phi), bar{v}(psi)) = bar{v}(phi) cdot bar{v}(psi)
]
[
bar{v}(phi lor psi) = max(bar{v}(phi), bar{v}(psi)) = bar{v}(phi) + bar{v}(psi) – bar{v}(phi)bar{v}(psi)
]
[
bar{v}(phi to psi) = max(1 – bar{v}(phi), bar{v}(psi))
]
A formula $phi$ is a tautology (written $vDash phi$) if $bar{v}(phi) = 1$ for every valuation $v$. Given a set of premises $Gamma subseteq text{Form}(mathcal{L}_0)$, we write $Gamma vDash phi$ (semantic consequence) if every valuation that satisfies all formulas in $Gamma$ also satisfies $phi$:
[
Gamma vDash phi iff forall v ; left( left( forall gamma in Gamma, bar{v}(gamma) = 1 right) implies bar{v}(phi) = 1 right)
]
3. Hilbert-Style & Natural Deduction Proof Systems
In stark contrast to semantic truth, a deductive system operates entirely syntactically without invoking truth-values. In a Hilbert-style deductive system $mathcal{H}$, derivations are sequences of formulas where each line is either an axiom or derived from previous lines via inference rules.
The Classic Łukasiewicz Axiom System
Taking $neg$ and $to$ as primitive connectives:
- A1 (Affirmation of the Consequent): $phi to (psi to phi)$
- A2 (Distribution of Implication): $(phi to (psi to chi)) to ((phi to psi) to (phi to chi))$
- A3 (Contraposition): $(neg psi to neg phi) to (phi to psi)$
Inference Rule — Modus Ponens (MP):
[
frac{phi quad phi to psi}{psi}
]
A formal proof of $phi$ from $Gamma$ (written $Gamma vdash phi$) is a finite sequence of formulas $langle phi_1, phi_2, dots, phi_n rangle$ such that $phi_n = phi$, and for every $1 le i le n$, either $phi_i in Gamma$, $phi_i$ is an instance of an axiom, or $phi_i$ follows from earlier formulas via Modus Ponens.
4. The Deduction Theorem
One of the central metatheorems of syntactic logic is the Deduction Theorem (Herbrand, 1930):
[
Gamma cup {phi} vdash psi iff Gamma vdash phi to psi
]
The proof proceeds by induction on the length $n$ of the deduction of $psi$ from $Gamma cup {phi}$. If $psi = phi$, then $vdash phi to phi$ is a provable theorem using A1 and A2. If $psi$ was derived via Modus Ponens from $chi$ and $chi to psi$, induction hypotheses $Gamma vdash phi to chi$ and $Gamma vdash phi to (chi to psi)$ combine with axiom A2 to yield $Gamma vdash phi to psi$.
5. Soundness & Completeness: The Bridge of Reason
The philosophical triumph of formal logic is the exact equivalence between syntactic proof and semantic reality:
Theorem 1: Soundness ($Gamma vdash phi implies Gamma vDash phi$)
Every formally derivable formula is a semantic consequence. The proof proceeds by structural induction on the derivation length: all axioms are easily verified to be tautologies under truth tables, and Modus Ponens preserves semantic truth.
Theorem 2: Semantic Completeness ($Gamma vDash phi implies Gamma vdash phi$)
Every semantic consequence is formally derivable. First proved by Emil Post (1921), completeness guarantees that our purely mechanical inference rules are strong enough to capture every mathematical truth in the propositional realm.
Equivalently, Completeness states that every syntactically consistent set of formulas is satisfiable ($text{Consistent} iff text{Satisfiable}$). This establishes that in propositional logic, the mechanical engine of symbol manipulation matches semantic truth with total precision.
