Formal Proofs and Deductive Systems

Mort Yao

1 Formal Proofs

Formal proof. A formal proof (or a derivation) is a finite sequence of well-formed formulas (in the scope of formal languages), each of which is an axiom, an assumption, or follows from the preceding sentences in the sequence by a rule of inference. Formal proofs are a form of logical argumentation using deductive reasoning.

Several commonly used deduction styles (also called proof calculi) for expressing logical arguments exist:

  • Structural proof theory (prefers the use of rules of inferences)
    • Natural deduction. Every line is a conditional tautology with zero or more conditions on the left, and exactly one asserted proposition on the right.
    • Sequent calculus. Every line is a conditional tautology with zero or more conditions on the left, and zero or more asserted propositions on the right.
  • Hilbert-style systems (prefers the use of axioms). Every line is an unconditional tautology.

A proof calculus is merely a style of formal inferences, which may be applied to different logics (e.g., classical logic, intuitionistic logic) in different formal systems.

A semi-formal proof is a proof written in a natural language, which is intended to be read by human. A semi-formal proof should be easily translatable into a formal proof that can be verified by a machine.

Term. A well-formed term is either a parameter variable, or a function applied to some other terms. In formal grammar: \[t ::= x\ |\ f(t_1, \dots, t_n)\]

A function symbol builds up a term from other terms, which can be defined as \[f(x_1, \dots, x_n) \equiv t\] (Note that \(t\) may not use \(f\) recursively.)

A relation symbol (or a predicate) builds up an atomic formula from terms, which can be defined as \[p(x_1, \dots, x_n) \equiv P\] (Note that \(P\) may not use \(p\) recursively.)

Formula. A well-formed formula is either an atomic formula, or a compound formula built up from atomic formulas using connectives or quantifiers. In formal grammar: \[P ::= p(t_1, \dots, t_n)\ |\ P_1 \land P_2\ |\ P_1 \lor P_2\ |\ P_1 \Rightarrow P_2\ |\ \top\ |\ \bot\ |\ \lnot P_1\ |\ \forall x : S . P_1\ |\ \exists x : S . P_1\]

(Note that a formula may contain free variables that are not bound by any quantifier.)

Proposition. A proposition is a statement such that

For all \(x_1\) in \(S_1\), , and \(x_n\) in \(S_n\), if \(P_1, \dots, P_m\) all hold, then \(Q\) holds.

or (as a well-formed formula) \[\models \forall x_1 : S_1 . \cdots \forall x_n : S_n . P_1 \land \cdots \land P_m \Rightarrow Q\] where \(x_1, \dots, x_n\) are the parameters, \(P_1, \dots, P_m\) are the assumptions (or the hypotheses), and \(Q\) is the conclusion (or the consequence). The assumptions and the conclusion may not contain free variables other than the given parameters. Thus, a proposition always has a definite truth value.

A proposition is valid (semantically true in all interpretations), if and only if there is a truth judgment \[P_1, \dots, P_m \models Q\]

A proposition is provable, if and only there is a sequent judgment \[P_1, \dots, P_m \vdash Q\] that follows from a formal proof, where \(P_1, \dots, P_m\) (also written collectively as \(\Gamma\)) are the antecedents, and \(Q\) is the consequent.

Theorem. A provably true proposition is a theorem.

Soundness. A formal system is said to be sound, if and only if given all axioms and rules of inference, \(\Gamma \vdash Q\) implies \(\Gamma \models Q\). (Provability implies validity)

Completeness. A formal system is said to be complete, if and only if given all axioms and rules of inference, \(\Gamma \models Q\) implies \(\Gamma \vdash Q\). (Validity implies provability)

While verifying a proof is often mechanized efficiently, finding the proof of a theorem can be computationally intractable or only semi-decidable.

2 Rules of Inference

In the tree-like presentation of a proof (proof tree), a derivation is constructed from proof rules such as \[\frac{\Gamma_1 \vdash Q_1 \quad \cdots \quad \Gamma_n \vdash Q_n}{\Gamma \vdash Q}\] The sequents above the line are the premises of the rule; the sequent below the line is the conclusion of the rule.

2.1 Assumption

\[\textsc{Ass}_i : \frac{}{P_1, \dots, P_n \vdash P_i} \quad (i \in \{1, \dots, n\})\]

2.2 Domain-Specific Axiom

\[\textsc{Axiom}_P : \frac{}{\Gamma \vdash P} \quad (P \textrm{ is an axiom})\]

2.3 Internal Lemma

\[\textsc{Lemma} : \frac{\Gamma \vdash P \quad \Gamma, P \vdash Q}{\Gamma \vdash Q}\]

2.4 Conjunction Introduction

Also called adjunction.

\[\land\textsc{I} : \frac{\Gamma \vdash P_1 \quad \Gamma \vdash P_2}{\Gamma \vdash P_1 \land P_2}\]

2.5 Conjunction Elimination

Also called simplification.

\[\land\textsc{E}_1 : \frac{\Gamma \vdash P_1 \land P_2}{\Gamma \vdash P_1}\]

\[\land\textsc{E}_2 : \frac{\Gamma \vdash P_1 \land P_2}{\Gamma \vdash P_2}\]

2.6 Disjunction Introduction

Also called addition.

\[\lor\textsc{I}_1 : \frac{\Gamma \vdash P_1}{\Gamma \vdash P_1 \lor P_2}\]

\[\lor\textsc{I}_2 : \frac{\Gamma \vdash P_2}{\Gamma \vdash P_1 \lor P_2}\]

2.7 Disjunction Elimination

Also called proof by cases.

\[\lor\textsc{E} : \frac{\Gamma \vdash P_1 \lor P_2 \quad \Gamma, P_1 \vdash Q \quad \Gamma,P_2 \vdash Q}{\Gamma \vdash Q} \]

2.8 Implication Introduction

Also called the deduction theorem.

\[\Rightarrow\textsc{I} : \frac{\Gamma, P \vdash Q}{\Gamma \vdash P \Rightarrow Q}\]

2.9 Implication Elimination

Also called modus ponens.

\[\Rightarrow\textsc{E} : \frac{\Gamma \vdash P \Rightarrow Q \quad \Gamma \vdash P}{\Gamma \vdash Q}\]

2.10 Truth Introduction

\[\top\textsc{I} : \frac{}{\Gamma \vdash \top}\]

2.11 Falsehood Elimination

Also called the principle of explosion (ex falso quodlibet). This rule is rejected by minimal logic.

\[\bot\textsc{E} : \frac{\Gamma \vdash \bot}{\Gamma \vdash Q}\]

An alternative rule of the ex falso axiom is

\[\Rightarrow\textsc{EFQ} = \frac{\Gamma \vdash \lnot P}{\Gamma \vdash P \Rightarrow Q}\]

2.12 Negation Introduction

\[\lnot\textsc{I} : \frac{\Gamma, P \vdash \bot}{\Gamma \vdash \lnot P}\]

A related rule is modus tollens:

\[\lnot\textsc{MT} : \frac{\Gamma \vdash P \Rightarrow Q, \lnot Q}{\Gamma \vdash \lnot P}\]

2.13 Negation Elimination

\[\lnot\textsc{E} : \frac{\Gamma \vdash \lnot P \quad \Gamma \vdash P}{\Gamma \vdash \bot}\]

2.14 Universal Introduction

\[\forall\textsc{I} : \frac{\Gamma \vdash P[x'/x]}{\Gamma \vdash \forall x : S . P} \quad (x' \textrm{ does not occur in } \Gamma \textrm{ or } P.)\]

2.15 Universal Elimination

\[\forall\textsc{E}_t : \frac{\Gamma \vdash \forall x : S . P}{\Gamma \vdash P[t/x]} \quad (t \textrm{ is a term of sort } S.)\]

2.16 Existential Introduction

\[\exists\textsc{I}_t : \frac{\Gamma \vdash P[t/x]}{\Gamma \vdash \exists x : S . P} \quad (t \textrm{ is a term of sort } S.)\]

2.17 Existential Elimination

\[\exists\textsc{E} : \frac{\Gamma \vdash \exists x : S . P \quad \Gamma, P[x'/x] \vdash Q}{\Gamma \vdash Q} \quad (x' \textrm{ does not occur in } \Gamma, P \textrm{ or } Q.)\]

2.18 Equality

2.18.1 Equality Introduction

Also call reflexivity.

\[=\textsc{I} : \frac{}{\Gamma \vdash t = t}\]

2.18.2 Equality Elimination

\[=\textsc{E} : \frac{\Gamma \vdash t_1 = t_2 \quad \Gamma \vdash P[t_1/x]}{\Gamma \vdash P[t_2/x]}\]

2.19 Indirect Proofs

These rules are rejected by intuitionistic logic.

2.19.1 Proof by Contradiction

\[\textsc{PBC} : \frac{\Gamma, \lnot P \vdash \bot}{\Gamma \vdash P}\]

2.19.2 Double Negation Elimination

\[\textsc{DNE} : \frac{\Gamma \vdash \lnot\lnot P}{\Gamma \vdash P}\]

2.19.3 Law of Excluded Middle

\[\textsc{LEM} : \frac{}{\Gamma \vdash P \lor \lnot P}\]

2.20 Induction

2.20.1 Mathematical Induction

\[\textsc{Ind}_\mathbb{N} : \frac{\Gamma \vdash P[0/x] \quad \Gamma, P[x'/x] \vdash P[(x' + 1)/x]}{\Gamma \vdash \forall x : \mathbb{N} . P} \quad (x' \textrm{ does not occur in } \Gamma \textrm{ or } P.)\]