The simplest formal (logical) language is the propositional calculus. This considers the logical relationships that hold between complete propositions. The language of the propositional calculus consists of an infinite number of atomic propositional variables P, Q, R, … and a set of logical connectives ¬ (“not”), & (“and”), ∨ (“or”), ⊃ (the material conditional “if … then …”), and ≡ (the bi-conditional “… if and only if …”). The set of logical connectives {¬, &, ∨, ⊃, ≡} is expressively complete for the propositional calculus, although some of the connectives are inter-definable, and smaller sets of logical connectives can also be shown to be expressively complete. A well-formed formula (wff) of the propositional calculus is any atomic propositional variable or a molecular formula built up recursively via the following formation rules:
If P is a wff, then ¬P is a wff;
If P is a wff and Q is a wff, then (P & Q) is a wff;
If P is a wff and Q is a wff, then (P ∨ Q) is a wff;
If P is a wff and Q is a wff, then (P ⊃ Q) is a wff;
If P is a wff and Q is a wff, then (P ≡ Q) is a wff;
Nothing else is a wff.
Semantics
An interpretation for the propositional calculus is a function that assigns to every propositional variable a truth value (either true or false). The truth values for complex, molecular formulas can then be built up compositionally via the truth tables for the logical connectives:
P Q ¬P P & Q P ∨∨ Q P ⊃⊃ Q P ≡ Q
T T F T T T T
T F F F T F F
F T T F T T F
F F T F F T T
By inspection of the truth tables, it can be seen how many of the logical connectives are inter-definable; for example, (P ⊃ Q) is equivalent to (¬P ∨ Q).
Proof Theory
In simple terms, a proof for a formula φ is nothing more than a list of well-formed formulas (in the relevant formal language) containing φ as the last step. To be convincing, however, each step in the proof must either consist of an initial premise whose truth is taken for granted or derived from a previous step by a transformation rule shown to be truth-preserving. The most straightforward proof theory for the propositional calculus, therefore, proceeds via the truth tables. It can be established by inspection whether there is any possible interpretation (that is, assignment of truth values) whereby one step of the proof is true but the next step is false, and thus whether the proposed transformation is necessarily truth-preserving. This method is purely mechanical and can be performed by a machine (the propositional calculus is therefore said to be decidable) but is unwieldy for longer proofs and provides little philosophical insight into the derivation.
A natural deduction system is a set of inference rules intended to produce a more
intuitive proof sequence. Any proposition φ can be introduced as an assumption at any stage of the proof and will remain an assumption of the proof unless it is later discharged. The other rules of the natural deduction system essentially provide the conditions for introducing or eliminating the logical connectives; in each case, any new formula will depend upon the same assumptions as the premises from which it is derived. Here is a concise set of natural deduction rules for the propositional calculus:
Rule of Assumption: Any proposition φ can be introduced at any stage of the proof.
Modus Ponens/Modus Tollens: Given φ and (φ ⊃ ψ), we can derive ψ; given (φ ⊃ ψ) and ¬ψ, we can derive ¬φ.
Conditional Proof: Given a proof of ψ from φ, we can derive (φ ⊃ ψ).
Double Negation Introduction and Elimination: Given φ, we can derive ¬¬φ; given ¬¬φ, we can derive φ.
&-Introduction and &-Elimination: Given φ and ψ, we can derive (φ & ψ); given (φ & ψ), we can derive both φ or ψ individually.
∨-Introduction and ∨-Elimination: Given either φ or ψ separately, we can derive (φ ∨ ψ); given (φ ∨ ψ), along with a proof of θ from φ, and a proof of θ from ψ, we can derive θ.
Reductio ad Absurdum: Given a proof of (ψ & ¬ψ) from φ, we can derive ¬φ.
In addition to capturing the intuitive meaning of the logical connectives, these rules can also be shown via the truth tables to be necessarily truth-preserving. In addition, any tautology (a logically true wff that, therefore, does not depend upon any assumptions) can also be introduced at any time, usually as a way to shorten the proof.
Meta-Logical Results
The propositional calculus is both sound and complete. Informally, a logical language is said to be sound if it is only possible to prove a formula that is true; that is to say, if a set of wellformed formulas X syntactically entails a formula φ, then X semantically entails φ (if X ⊢ φ, then X ⊨ φ). Similarly, a logical language is said to be complete only if every true formula also has a proof; that is to say, if a set of well formed formulas X semantically entails a formula φ, then X syntactically entails φ (if X ⊨ φ, then X ⊢ φ). Formal proofs can be provided for both results, but the idea should be intuitive: informally, given that an interpretation of the propositional calculus assigns truth values to complex formulas compositionally via the truth tables for the logical connectives, and given that the steps for any proof theory for the propositional calculus involves (truth-preserving) introduction and elimination rules for the logical connectives, it is easy to see why the propositional calculus should be both sound and complete.
