CS208 Logic & Algorithms

Semester 1: Logic

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”

Using the Proof Editor

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).

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.

  1. For all things, if p and q are true, then p is true:

    Theorem: 
     ⊢ ∀x.  (p(x) ∧ q(x)) → p(x)
    Proof
    goal: ∀x.  (p(x) ∧ q(x)) → p(x)
    Proof incomplete (1 subgoal open).

  2. If p is true for all things, then it is true for the specific individual a().

    Theorem: 
     ⊢ (∀x.  p(x)) → p(a())
    Proof
    goal: (∀x.  p(x)) → p(a())
    Proof incomplete (1 subgoal open).

  3. If p and q are true for all things, then p is true for all things.

    Theorem: 
     ⊢ (∀x.  p(x) ∧ q(x)) → (∀y.  p(y))
    Proof
    goal: (∀x.  p(x) ∧ q(x)) → (∀y.  p(y))
    Proof incomplete (1 subgoal open).

Proof rules for “exists”

Using the Proof Editor

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

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).

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.

  1. If p is true for a(), then there exists a thing for which p is true:

    Theorem: 
     ⊢ p(a()) → (∃x.  p(x))
    Proof
    goal: p(a()) → (∃x.  p(x))
    Proof incomplete (1 subgoal open).

  2. If something exists that has two properties, then something exists that has one of those properties:

    Theorem: 
     ⊢ (∃x.  p(x) ∧ q(x)) → (∃z.  p(z))
    Proof
    goal: (∃x.  p(x) ∧ q(x)) → (∃z.  p(z))
    Proof incomplete (1 subgoal open).

  3. 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:

    Theorem: 
     ⊢ (∃x.  p(x) ∨ q(x)) → ((∃z.  p(z)) ∨ (∃z.  q(z)))
    Proof
    goal: (∃x.  p(x) ∨ q(x)) → ((∃z.  p(z)) ∨ (∃z.  q(z)))
    Proof incomplete (1 subgoal open).

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

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).

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.

  1. If every p has something that is r-related to it, and a() is a p, then there is something r-related to a().

    Theorem: 
     ⊢ (∀x.  p(x) → (∃y.  r(x, y))) → p(a()) → (∃z.  r(a(), z))
    Proof
    goal:
    (∀x.  p(x) → (∃y.  r(x, y))) → p(a()) → (∃z.  r(a(), z))
    Proof incomplete (1 subgoal open).

  2. If everything is not p, then there does not exist a p:

    Theorem: 
     ⊢ (∀x.  ¬p(x)) → ¬(∃y.  p(y))
    Proof
    goal: (∀x.  ¬p(x)) → ¬(∃y.  p(y))
    Proof incomplete (1 subgoal open).

  3. If there exists a non-p, then not everything is a p:

    Theorem: 
     ⊢ (∃x.  ¬p(x)) → ¬(∀y.  p(y))
    Proof
    goal: (∃x.  ¬p(x)) → ¬(∀y.  p(y))
    Proof incomplete (1 subgoal open).

  4. Quantifier order can be swapped, when they are the same quantifier:

    Theorem: 
     ⊢ (∀x. ∀y.  R(x, y)) → (∀x. ∀y.  R(y, x))
    Proof
    goal: (∀x. ∀y.  R(x, y)) → (∀x. ∀y.  R(y, x))
    Proof incomplete (1 subgoal open).