Proof rules for Predicate Logic

With an understanding of scope and substitution, we can now look at the proof rules for Predicate Logic. The videos below introduce the rules and show how to use them in the interactive proof editor. There are exercises throughout the page to help you understand how the rules work, and so how the quantifiers work.

Slides for the videos below (PDF)

Proof rules for “for all”

Enter any notes to yourself here

Using the Proof Editor

Enter any notes to yourself here

Exercises

These exercises use the new rules for “for all”, as well as the rules for the propositional connectives:

Proof commands...

The blue boxes represent parts of the proof that are unfinished. The comments (in green) tells you what the current goal is. Either the goal is unfocused:

{ goal: <some formula> }

or there is a formula is focus:

{ focus: <formula1>; goal: <formula2> }

The commands that you can use differ according to which mode youare in. The commands correspond directly to the proof rules given in the videos.

Unfocused mode

These rules can be used when there is no formula in the focus. These rules either act on the conclusion directly to break it down into simpler sub-goals, or switch to focused mode (the use command).

introduce H can be used when the goal is an implication ‘P → Q’. The name H is used to give a name to the new assumption P. The proof then continues proving Q with this new assumption. A green comment is inserted to say what the new named assumption is.
NEW introduce y can be used when the goal is a for all quantification ‘∀x. Q’. The name y is used for the assumption of an arbitrary individual that we have to prove ‘Q’ for. The proof then continues proving ‘Q’. A green comment is inserted to say that the rest of this branch of the proof is under the assumption that there is a named entity.
split can be used when the goal is a conjunction “P ∧ Q”. The proof will split into two sub-proofs, one to prove the first half of the conjunction “P”, and one to prove the other half “Q”.
true can be used when the goal to prove is ‘T’ (true). This will finish this branch of the proof.
left can be used when the goal to prove is a disjunction ‘P ∨ Q’. A new sub goal will be created to prove ‘P’.
right can be used when the goal to prove is a disjunction ‘P ∨ Q’. A new sub goal will be created to prove ‘Q’.
not-intro H can be used when the goal is a negation ‘¬P’. The name H is used to give a name to the new assumption P. The proof then continues proving F (i.e. False) with this new assumption. A green comment is inserted to say what the new named assumption is.
use H can be used whenever there is no current focus. H is the name of some assumption that is available on this branch of the proof. Named assumptions come from the original statement to be proved, and uses of introduce H, cases H1 H2, not-intro H, and unpack y H.

Focused mode

These rules apply when there is a formula in focus. These rules either act upon the formula in focus, or finish the proof when the focused formula is the same as the goal.

done can be used when the formula in focus is exactly the same as the goal formula. This will finish this branch of the proof.
apply can be used when the formula in focus is an implication ‘P → Q’. A new subgoal to prove ‘P’ is generated, and the focus becomes ‘Q’ to continue the proof.
first can be used when the formula in focus is a conjunction P ∧ Q. The focus then becomes ‘P’, the first part of the conjunction, and the proof continues.
second can be used when the formula in focus is a conjunction P ∧ Q. The focus then becomes ‘Q’, the second part of the conjunction, and the proof continues.
cases H1 H2 can be used then the formula in focus is a disjunction ‘P ∨ Q’. The proof splits into two branches, one for ‘P’ and one for ‘Q’. The two names H1 and H2 are used to name the new assumption on the two branches. Green comments are inserted to say what the new named assumptions are.
false can be used when the formula in focus is ‘F’ (false). The proof finishes at this point, no matter what the conclusion is.
not-elim can be used when the formula in focus is a negation ‘¬P’. A new subgoal is generated to prove ‘P’ in order to generate a contradiction.
NEW inst "t" can be used when the formula in focus is of the form ‘∀x. P’. The term t (which must be in quotes) is substituted in the place of x in the formula after the quantifier and the substituted formula ‘P[x:=t]’ remains in focus.

For all things, if p and q are true, then p is true:
(config (solution (Rule(Introduce x)((Rule(Introduce x-is-p-and-q)((Rule(Use x-is-p-and-q)((Rule Conj_elim1((Rule Close())))))))))) (goal "all x. (p(x) /\ q(x)) -> p(x)"))
If p is true for all things, then it is true for the specific individual a().
(config (solution (Rule(Introduce everything-is-p)((Rule(Use everything-is-p)((Rule(Instantiate(Fun a()))((Rule Close())))))))) (goal "(all x. p(x)) -> p(a())"))
If p and q are true for all things, then p is true for all things.
(config (solution (Rule(Introduce all-p-and-q)((Rule(Introduce y)((Rule(Use all-p-and-q)((Rule(Instantiate(Var y))((Rule Conj_elim1((Rule Close())))))))))))) (goal "(all x. p(x) /\ q(x)) -> (all y. p(y))"))

Proof rules for “exists”

Enter any notes to yourself here

Using the Proof Editor

Enter any notes to yourself here

Exercises

These exercises use the new rules for “exists”, as well as the rules for the propositional connectives:

Proof commands...

The blue boxes represent parts of the proof that are unfinished. The comments (in green) tells you what the current goal is. Either the goal is unfocused:

{ goal: <some formula> }

or there is a formula is focus:

{ focus: <formula1>; goal: <formula2> }

The commands that you can use differ according to which mode youare in. The commands correspond directly to the proof rules given in the videos.

Unfocused mode

introduce H can be used when the goal is an implication ‘P → Q’. The name H is used to give a name to the new assumption P. The proof then continues proving Q with this new assumption. A green comment is inserted to say what the new named assumption is.
introduce y can be used when the goal is a for all quantification ‘∀x. Q’. The name y is used for the assumption of an arbitrary individual that we have to prove ‘Q’ for. The proof then continues proving ‘Q’. A green comment is inserted to say that the rest of this branch of the proof is under the assumption that there is a named entity.
split can be used when the goal is a conjunction “P ∧ Q”. The proof will split into two sub-proofs, one to prove the first half of the conjunction “P”, and one to prove the other half “Q”.
true can be used when the goal to prove is ‘T’ (true). This will finish this branch of the proof.
left can be used when the goal to prove is a disjunction ‘P ∨ Q’. A new sub goal will be created to prove ‘P’.
right can be used when the goal to prove is a disjunction ‘P ∨ Q’. A new sub goal will be created to prove ‘Q’.
not-intro H can be used when the goal is a negation ‘¬P’. The name H is used to give a name to the new assumption P. The proof then continues proving F (i.e. False) with this new assumption. A green comment is inserted to say what the new named assumption is.
NEW exists "t" can be used when the goal is an exists quantification ‘∃x. Q’. The term t which must be in quotes, is used as the existential witness and is substituted for x in Q. The proof then continues proving ‘Q[x:=t]’,
use H can be used whenever there is no current focus. H is the name of some assumption that is available on this branch of the proof. Named assumptions come from the original statement to be proved, and uses of introduce H, cases H1 H2, not-intro H, and unpack y H.

Focused mode

These rules apply when there is a formula in focus. These rules either act upon the formula in focus, or finish the proof when the focused formula is the same as the goal.

done can be used when the formula in focus is exactly the same as the goal formula. This will finish this branch of the proof.
apply can be used when the formula in focus is an implication ‘P → Q’. A new subgoal to prove ‘P’ is generated, and the focus becomes ‘Q’ to continue the proof.
first can be used when the formula in focus is a conjunction P ∧ Q. The focus then becomes ‘P’, the first part of the conjunction, and the proof continues.
second can be used when the formula in focus is a conjunction P ∧ Q. The focus then becomes ‘Q’, the second part of the conjunction, and the proof continues.
cases H1 H2 can be used then the formula in focus is a disjunction ‘P ∨ Q’. The proof splits into two branches, one for ‘P’ and one for ‘Q’. The two names H1 and H2 are used to name the new assumption on the two branches. Green comments are inserted to say what the new named assumptions are.
false can be used when the formula in focus is ‘F’ (false). The proof finishes at this point, no matter what the conclusion is.
not-elim can be used when the formula in focus is a negation ‘¬P’. A new subgoal is generated to prove ‘P’ in order to generate a contradiction.
inst "t" can be used when the formula in focus is of the form ‘∀x. P’. The term t (which must be in quotes) is substituted in the place of x in the formula after the quantifier and the substituted formula ‘P[x:=t]’ remains in focus.
NEW unpack y H can be used when the formula in focus is of the form ‘∃x. P’. The existential is “unpacked” into the assumption of an entity y and its property ‘P[x:=y]’, which is named H. Green comments are inserted to say what the assumption ‘H’ is.

If p is true for a(), then there exists a thing for which p is true:
(config (solution (Rule(Introduce a-is-p)((Rule(Exists(Fun a()))((Rule(Use a-is-p)((Rule Close())))))))) (goal "p(a()) -> (ex x. p(x))"))
If something exists that has two properties, then something exists that has one of those properties:
(config (solution (Rule(Introduce exists-a-p-and-q)((Rule(Use exists-a-p-and-q)((Rule(ExElim x x-is-p-and-q)((Rule(Exists(Var x))((Rule(Use x-is-p-and-q)((Rule Conj_elim1((Rule Close())))))))))))))) (goal "(ex x. p(x) /\ q(x)) -> (ex z. p(z))"))
If something exists that has one of two properties, then either there exists something that has the first property, or one that has the second:
(config (solution (Rule(Introduce exists-a-p-or-q)((Rule(Use exists-a-p-or-q)((Rule(ExElim x x-is-p-or-q)((Rule(Use x-is-p-or-q)((Rule(Cases x-is-p x-is-q)((Rule Left((Rule(Exists(Var x))((Rule(Use x-is-p)((Rule Close())))))))(Rule Right((Rule(Exists(Var x))((Rule(Use x-is-q)((Rule Close())))))))))))))))))) (goal "(ex x. p(x) \/ q(x)) -> ((ex z. p(z)) \/ (ex z. q(z)))"))

Exercises combining ∀ and ∃

These exercises combine “for all” and “exists”:

Proof commands...

The blue boxes represent parts of the proof that are unfinished. The comments (in green) tells you what the current goal is. Either the goal is unfocused:

{ goal: <some formula> }

or there is a formula is focus:

{ focus: <formula1>; goal: <formula2> }

The commands that you can use differ according to which mode youare in. The commands correspond directly to the proof rules given in the videos.

Unfocused mode

introduce H can be used when the goal is an implication ‘P → Q’. The name H is used to give a name to the new assumption P. The proof then continues proving Q with this new assumption. A green comment is inserted to say what the new named assumption is.
introduce y can be used when the goal is a for all quantification ‘∀x. Q’. The name y is used for the assumption of an arbitrary individual that we have to prove ‘Q’ for. The proof then continues proving ‘Q’. A green comment is inserted to say that the rest of this branch of the proof is under the assumption that there is a named entity.
split can be used when the goal is a conjunction “P ∧ Q”. The proof will split into two sub-proofs, one to prove the first half of the conjunction “P”, and one to prove the other half “Q”.
true can be used when the goal to prove is ‘T’ (true). This will finish this branch of the proof.
left can be used when the goal to prove is a disjunction ‘P ∨ Q’. A new sub goal will be created to prove ‘P’.
right can be used when the goal to prove is a disjunction ‘P ∨ Q’. A new sub goal will be created to prove ‘Q’.
not-intro H can be used when the goal is a negation ‘¬P’. The name H is used to give a name to the new assumption P. The proof then continues proving F (i.e. False) with this new assumption. A green comment is inserted to say what the new named assumption is.
exists "t" can be used when the goal is an exists quantification ‘∃x. Q’. The term t which must be in quotes, is used as the existential witness and is substituted for x in Q. The proof then continues proving ‘Q[x:=t]’,
use H can be used whenever there is no current focus. H is the name of some assumption that is available on this branch of the proof. Named assumptions come from the original statement to be proved, and uses of introduce H, cases H1 H2, not-intro H, and unpack y H.

Focused mode

These rules apply when there is a formula in focus. These rules either act upon the formula in focus, or finish the proof when the focused formula is the same as the goal.

done can be used when the formula in focus is exactly the same as the goal formula. This will finish this branch of the proof.
apply can be used when the formula in focus is an implication ‘P → Q’. A new subgoal to prove ‘P’ is generated, and the focus becomes ‘Q’ to continue the proof.
first can be used when the formula in focus is a conjunction P ∧ Q. The focus then becomes ‘P’, the first part of the conjunction, and the proof continues.
second can be used when the formula in focus is a conjunction P ∧ Q. The focus then becomes ‘Q’, the second part of the conjunction, and the proof continues.
cases H1 H2 can be used then the formula in focus is a disjunction ‘P ∨ Q’. The proof splits into two branches, one for ‘P’ and one for ‘Q’. The two names H1 and H2 are used to name the new assumption on the two branches. Green comments are inserted to say what the new named assumptions are.
false can be used when the formula in focus is ‘F’ (false). The proof finishes at this point, no matter what the conclusion is.
not-elim can be used when the formula in focus is a negation ‘¬P’. A new subgoal is generated to prove ‘P’ in order to generate a contradiction.
inst "t" can be used when the formula in focus is of the form ‘∀x. P’. The term t (which must be in quotes) is substituted in the place of x in the formula after the quantifier and the substituted formula ‘P[x:=t]’ remains in focus.
unpack y H can be used when the formula in focus is of the form ‘∃x. P’. The existential is “unpacked” into the assumption of an entity y and its property ‘P[x:=y]’, which is named H. Green comments are inserted to say what the assumption ‘H’ is.

If every p has something that is r-related to it, and a() is a p, then there is something r-related to a().
(config (solution (Rule(Introduce H)((Rule(Introduce a-is-p)((Rule(Use H)((Rule(Instantiate(Fun a()))((Rule Implies_elim((Rule(Use a-is-p)((Rule Close())))(Rule Close())))))))))))) (goal "(all x. p(x) -> (ex y. r(x,y))) -> p(a()) -> (ex z. r(a(),z))"))
If everything is not p, then there does not exist a p:
(config (solution (Rule(Introduce H)((Rule(NotIntro exists-p)((Rule(Use exists-p)((Rule(ExElim y y-is-p)((Rule(Use H)((Rule(Instantiate(Var y))((Rule NotElim((Rule(Use y-is-p)((Rule Close())))))))))))))))))) (goal "(all x. ¬p(x)) -> ¬(ex y. p(y))"))
If there exists a non-p, then not everything is a p:
(config (solution (Rule(Introduce H)((Rule(NotIntro all-are-p)((Rule(Use H)((Rule(ExElim x x-is-not-p)((Rule(Use x-is-not-p)((Rule NotElim((Rule(Use all-are-p)((Rule(Instantiate(Var x))((Rule Close())))))))))))))))))) (goal "(ex x. ¬p(x)) -> ¬(all y. p(y))"))
Quantifier order can be swapped, when they are the same quantifier:
(config (solution (Rule(Introduce H)((Rule(Introduce x)((Rule(Introduce y)((Rule(Use H)((Rule(Instantiate(Var y))((Rule(Instantiate(Var x))((Rule Close())))))))))))))) (goal "(all x. all y. R(x,y)) -> (all x. all y. R(y,x))"))