How to use Proof Checker Pro

Quick start

1. Enter any predicate definitions.
2. Enter one axiom per line. The checker supplies Roman numerals.
3. Enter the goal.
4. Write one proof command per line.
5. Watch the current goal, pretend worlds, checkmarks, and compiler output as you type.

Enter the problem

Predicate definitions

Definitions give a short name to a longer statement. Formal parameters begin with lowercase letters.

FAS(c) = (∀ d in Creatures)(S(d) → F(c, d))
FAM(c) = (∀ d in Creatures)(M(d) → F(c, d))

The goal display shows both the short name and its expansion when that information is useful.

Axioms

Enter one axiom per line. Do not type the Roman numerals unless you want to supply a particular label yourself.

(∀ c in Creatures)(S(c) → M(c))
(∀ c in Creatures)(M(c) → V(c))

These become Axioms I and II. You may cite an axiom by writing its Roman numeral after a rule name.

Goal

(∀ c in Creatures)(S(c) → V(c))

The current-goal display changes whenever you enter or leave a pretend world.

Define inductive types and recursive functions

An inductive declaration lists every way an object of a type can be constructed. Constructor names begin uppercase; constructor-field names begin lowercase.

inductive BinaryTree
    Leaf
    InternalNode(left: BinaryTree, right: BinaryTree)
end

A recursive function gives exactly one equation for each constructor. Recursive calls may use only the direct recursive parts named by that constructor.

recursive count(tree: BinaryTree): Natural
    count(Leaf) = 1
    count(InternalNode(left, right))
        = count(left) + count(right) + 1
end

Recursive properties use the same pattern:

recursive predicate Perfect(tree: BinaryTree)
    Perfect(Leaf) = True
    Perfect(InternalNode(left, right))
        = Perfect(left) ∧ Perfect(right)
          ∧ height(left) = height(right)
end

Use a definition explicitly in a proof:

count(InternalNode(Left, Right))
    = count(Left) + count(Right) + 1
    by definition of count

Structural induction

Induct on t
  BaseCase Leaf
    ...
  therefore P(Leaf) by induction case

  InductiveCase InternalNode(Left, Right)
    For induction assume:
      P(Left)
      P(Right)
    ...
  therefore P(InternalNode(Left, Right)) by induction case

therefore (∀ t in BinaryTrees)P(t) by induction

Use BaseCase for a constructor with no recursive parts and InductiveCase for a constructor with one or more recursive parts. The first line of every inductive case must be For induction assume:. Then state the original theorem once for each immediate recursive part. The checker verifies each hypothesis instead of supplying it, and each correct hypothesis becomes a numbered proof line that can be cited later.

Follow the shape of the goal

The outermost part of the goal usually determines the first move.

The Hint button follows this same strategy. It first simplifies universal and implication goals, then searches for useful instantiations and detachments.

Pretend worlds and scope

Universal generalization, make-believe, existential instantiation, proof by cases, and proof by contradiction create temporary worlds. The editor draws vertical rails to show their nesting.

Pretend Bob is a Creature.
  Make believe S(Bob).
    S(Bob) → M(Bob) by UI I
    M(Bob) by detachment 2, 3
  therefore S(Bob) → M(Bob) by MB 4
therefore (∀ c in Creatures)(S(c) → M(c)) by UG 5

• A line may use facts from its current world and any enclosing world.
• A fact created in a world cannot be used after that world has closed.
• Write introduced individuals with an uppercase first letter: Bob, X, or F.
• Indentation is added automatically. Spaces you type are accepted, but the scope comes from the proof commands.

When the current goal has been established inside a world, the checker offers a button that inserts the appropriate pop-out line.

Proof-rule recipes

S(Bob) → M(Bob) by UI I

M(Bob) by detachment 2, 3

Pretend Bob is a Creature.
...
therefore (∀ c in Creatures)P(c) by UG

Make believe P.
...
therefore P → Q by MB

Let Ari be a witness such that P(Ari) by EI I
...
therefore R by EI

(∃ k) 2k = N by EG 6

P ∧ Q by and introduction 2, 3
P by and elimination 4

P ∨ Q by or introduction 2
Case 1: Make believe P by cases III
...
therefore R by case
Case 2: Make believe Q by cases III
...
therefore R by case
therefore R by cases III

For contradiction assume ¬P.
...
Contradiction from lines 4, 7
therefore P by contradiction

¬P ∨ ¬Q by De Morgan 3
P by double negation 5

P ↔ Q by iff introduction 4, 8
P → Q by iff elimination 9

N^2 = 4J^2 + 4J + 1 by algebra

P by axiom II

A complete example

Axioms

(∀ c in Creatures)(S(c) → M(c))
(∀ c in Creatures)(M(c) → V(c))

Goal

(∀ c in Creatures)(S(c) → V(c))

Proof

Pretend Bob is a Creature.
  Make believe S(Bob).
    S(Bob) → M(Bob) by UI I
    M(Bob) by detachment 2, 3
    M(Bob) → V(Bob) by UI II
    V(Bob) by detachment 4, 5
  therefore S(Bob) → V(Bob) by MB 6
therefore (∀ c in Creatures)(S(c) → V(c)) by UG 7

The first line reduces the universal goal to a statement about arbitrary Bob. The second line reduces the implication goal to V(Bob). The two UI–detachment pairs establish that goal. MB and UG then close the worlds in reverse order.

Use the compiler feedback

• A green checkmark means that line compiles in its current world.
• A red × means the compiler cannot justify that line. Select it to jump to the corresponding diagnostic.
• The compiler stops trusting later lines after the first error, because their scopes or sources may depend on the broken line.
• The gray column beside the proof shows expanded predicate definitions.
• The current-goal panel tells you what remains to be established in the innermost world.

Frequent errors

• No available line matches: check the formula and cite the intended source.
• Line belongs to a closed world: that temporary fact is no longer available.
• Individual must begin uppercase: use Bob, not bob.
• Cannot infer references: add the axiom or line numbers after the rule name.
• Goal is not complete: establish the displayed goal and then close the current world.

Notation and typing shortcuts

Periods at the ends of proof commands are optional. Pressing Space after a completed shortcut performs the conversion while you type.