A logical calculus is a formal, axiomatic system for recursively generating well-formed formulas (wffs). Essentially, it's a definition of a vocabulary, rules for the formation of well-formed formulas (wffs), and rules of inference permitting the generation of all valid argument forms expressible in the calculus.
The propositional calculus is the foundation of symbolic logic; more complex logical calculi are usually defined by adding new operators and rules of transformation to it. It is generally defined as follows:
The vocabulary is composed of:
; Double Negative Elimination: From the wff ¬ ¬ φ, we may infer φ
; Conjunction Introduction: From any wff φ and any wff ψ, we may infer ( φ ∧ ψ ).
; Conjunction Elimination: From any wff ( φ ∧ ψ ), we may infer φ or ψ
; Disjunction Introduction: From any wff φ, we may infer the disjunction of φ with any other wff.
; Disjunction Elimination: From wffs of the form ( φ ∨ ψ ), ( φ → χ ), and ( ψ → χ ), we may infer χ.
; Biconditional Introduction: From wffs of the form ( φ → ψ ) and ( ψ → φ ), we may infer ( φ ↔ ψ ).
; Biconditional Elimination: From the wff ( φ ↔ ψ ), we may infer ( φ → ψ ) or ( ψ → φ ).
; Modus Ponens: From wffs of the form φ and ( φ → ψ ), we may infer ψ.
; Conditional Proof: If ψ can be derived from the hypothesis φ, we may infer ( φ → ψ ) and discharge the hypothesis.
; Reductio ad Absurdum: If we can derive both ψ and ¬ ψ from the introduction of the hypothesis φ, we may infer ¬ φ and discharge the hypothesis.
Introducing a hypothesis means adding a wff to a derivation not originally present as a premise; discharging the hypothesis means eliminating the wff justifiably--any wffs correctly derived from the hypothesis justify the introduction of the hypothesis after the fact.
With wffs and rules of inference, it's possible to derive wffs; the derivation is a valid argument form, while the derived wff is known as a lemma.
See also: