A **logical calculus** is a formal, axiomatic system for recursively generating well-formed formulas (*wff*s). Essentially, it's a definition of a vocabulary, rules for the formation of well-formed formulas (*wff*s), 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:

- The letters of the alphabet (usually capitalized).
- Symbols denoted logical operators: ¬, &and, &or, &rarr, &harr
- Parenthesis for grouping a
*wff*as a sub-*wff*of a compound*wff*s: (, )

- Letters of the alphabet (usually capitalized) are
*wff*s. - If φ is a
*wff*, then ¬ φ is a*wff*. - If φ and ψ are
*wff*s, then (φ ∧ ψ), (φ ∨ ψ), (φ → ψ), and (φ ↔ ψ) are*wff*s.

- By rule 1, A is a
*wff*. - By rule 2, ¬ A is a
*wff*. - By rule 1, B is a
*wff*. - By rule 3, ( ¬ A ∨ B ) is a
*wff*.

; 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 *wff*s of the form ( φ ∨ ψ ), ( φ → χ ), and ( ψ → χ ), we may infer χ.

; Biconditional Introduction: From *wff*s of the form ( φ → ψ ) and ( ψ → φ ), we may infer ( φ ↔ ψ ).

; Biconditional Elimination: From the *wff* ( φ ↔ ψ ), we may infer ( φ → ψ ) or ( ψ → φ ).

; Modus Ponens: From *wff*s 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 *wff*s 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:

- Metamath: a project to construct mathematics using an axiomatic system based on propositional calculus, predicate calculus, and set theory