This is an old revision of the document!
Informal Proofs and Mathematical Induction
Proof Rules
We next summarize proof rules that we can use to establish validity of formulas of first-order logic. We will keep these rules in mind for informal reasoning, but they can also be mechanized and we illustrate this fact in the Isabelle theorem prover. (Later we look at resolution procedure as an alternative to these proof rules.)
When proving a formula, we typically have a set of current assumptions and a goal. Moreover, we will consider the possibility of having multiple alternative goals, to explore multiple possible proofs at the same time. A state of our proof attempt is therefore given by a sequent of the form \[
A_1,\ldots,A_n \vdash G_1,\ldots,G_m
\]
where are assumptions and
are goals. The meaning of a sequent is the implication formula
\[
A_1 \land \ldots \land A_n \rightarrow G_1 \lor \ldots \lor G_m
\]
We admit the case of no assumptions () in which the left hand side is true and the case of no goals (
) in which case the right-hand side is considered to be false. (You can think of one of the assumptions always being the trivial assumption true, and one of the goals always being the trivially unprovable goal false.)
The rules below will have the form \[
\frac{S_1\ ;\ ... \ ;\ S_K}{S_0}
\]
where are sequents. The meaning of each rule is that if we establish sequents
then we can derive sequent
. In other words, if we wish to prove sequent
, it suffices to prove sequents
. The rules below allow us to eliminate propositional connectives in valid formulas until we obtain sequents of the form
, which is a trivially valid sequent because one of its goals appears as an assumption.
To make rules concise we avoid writing common assumptions and conclusions. We assume that we can apply each rule in a context: we can introduce any set of assumptions simultaneously to all left-hand sides of a rule. Similarly, we can introduce another set of assumptions to all right-hand sides of the sequents in the rule. We ignore the ordering of assumptions and goals, because they are connected by associative and commutative logical operations.
Below we present one rule for each logical connective (,
,
,
) and quantifier (
,
). For each of these construct we show how to prove the sequent when the formula with the connective is on the left-hand side and when the formula with the connective is on the right hand side. The English comment is just to aide some intuition and is by necessity imprecise.
Conjunction-Left
If we can prove something from two assumptions, we can also prove it from their conjunction. \[ \frac{P,Q \vdash}
{P\land Q \vdash}
\]
Conjunction-Right
To prove a conjunction, prove each conjunct. \[ \frac{\vdash P\ ;\ \vdash Q}
{\vdash P \land Q}
\]
Disjunction-Left
To prove something from a disjunctive assumption, prove it by case analysis, one case for each disjunct. \[ \frac{P \vdash \ ; \ Q \vdash}
{P\lor Q \vdash}
\]
Disjunction-Right
To prove a disjunction try to prove one of the disjuncts. \[ \frac{\vdash P,Q}
{\vdash P \lor Q}
\]
Implication-Left
To prove something from an implication, prove it from its conclusion and also prove the premise. \[ \frac{\vdash P\ ;\ Q \vdash}
{P \rightarrow Q \vdash}
\]
Implication-Right
To prove an implication, assume its premise and prove its goal. \[ \frac{P \vdash Q}
{\vdash P \rightarrow Q}
\]
Negation-Left
Instead of proving a goal, you can assume its negation and prove any remaining goals (this generalizes proof by contradiction). \[ \frac{\lnot P \vdash\}
{\vdash P}
\]
Negation-Right
If you prove one of the goals, you can assume its negation and prove remaining goals. \[ \frac{\vdash P}
{\lnot P \vdash}
\]
Forall-Left
If you have a universally quantified assumption, you can instantiate universal quantifier with any value, denoted by term t (this is what “for all” means). You keep the original quantified assumption in case you need to instantiate it multiple times. \[ \frac{P(t), \forall x.P(x)}
{\forall x.P(x) \vdash}
\]
Forall-Right
To prove a universally quantified goal, prove the goal for an arbitrary element, denoted by fresh variable . Informally we would say “let
be arbitrary…”.
\[
\frac{\vdash P(x_0)}
{\vdash \forall x.P(x)}
\]
Exists-Left
When you have an existentially quantified assumption, you can pick a witness for existential statement and denote it by fresh variable “x_0”. Informally we would say “let be such
”.
\[
\frac{P(x_0)}
{\exists x. P(x) \vdash}
\]
Exists-Right
To prove an existentially quntified statement, supply a witness for the existential quantifier, given by value of some term t. Keep the original existential quantifier in case this was not the right instantiation. \[ \frac{\vdash P(t), \exists x.P(x)}
{\vdash \exists x. P(x)}
\]
Example
Let us prove the following formula: \[
\exists x. \forall y. F(x,y) \vdash \forall u. \exists v. F(v,u)
\]
Using Proof Rules in Isabelle
Completeness for First-Order Logic
Completeness theorem: If a first-order logic formula without equality is valid, it can be shown valid using the above rules.
- Gallier Logic Book, Section 5.4 page 187+23, Section 5.5
We will later introduce a different proof system (resolution), for which we will prove completeness.
Proving Universally Quantified Statements by Mathematical Induction
Stepwise Induction
\[ \frac{P(0)\ \ \land\ \ (\forall n\in \mathbb{N}. (P(n) \rightarrow P(n+1))}
{\forall n \in \mathbb{N}. P(n)}
\]
Total Induction
\[ \frac{\forall n \in \mathbb{N}. 1) \rightarrow P(n))}
{\forall n \in \mathbb{N}. P(n)}
\]
Deriving one induction from another.
Structural Induction
- Calculus of Computation Textbook, Chapter 4 (some example refer to previous chapters, if you do not understand them, ignore them for now)