A Brief NatDed Tutorial

Entering Theorems

When you execute natded.exe, you will get an Enter theorem: prompt. Enter the theorem which you would like to prove. Symbols are translated as follows:

Words beginning with uppercase letters are predicates. Words beginning with lowercase letters are functions and variables. You need a dot (.) after quantifiers.

Commands

Typing help brings up a list of commands with descriptions.

? help
Commands are:
    <->i  apply iff-intro
     ->i  apply arrow-intro
   ->e P  apply arrow-elim with assumption P
      &i  apply and-intro
   &el Q  apply and-elim-left with rhs Q
   &er P  apply and-elim-right with lhs P
     |il  apply or-intro-left
     |ir  apply or-intro-right
  |e P|Q  apply or-elim with disjunction P|Q
      ~i  apply not-intro
      ~e  apply not-elim
    Ei t  apply exists-intro with subst term t
    Ee P  apply exists-elim with premise P
      Ai  apply forall-intro
    Ae P  apply forall-elim with premise P
     efq  apply ex falso quodlibet
   magic  apply law of excluded middle
     raa  apply reductio ad absurdum
    unit  apply unit
   use x  use assumption x
   tasks  show list of tasks
    undo  undo last command
 latex f  write latex to file f
     enc  toggle ISO-8859-1/UTF-8 character encoding
   reset  begin proof from scratch
    init  start new theorem
    quit  quit
    help  show list of commands
    

Theorem Proving

NatDed assists you in proving the theorem you entered. All you need to do is complete all the tasks. The current task is completed when the Goal is obtained. To obtain the Goal, think of what application of inference rules (listed in the commands) would lead to the Goal. For example, a goal of 0 (false) can be achieved in a number of ways, including ⇒-elimination if we had premises A and A -> 0. Hence, typing ->e A at the prompt completes the current task, but introduces two new tasks: to prove A and to prove A -> 0.

The inference rules are described in the notes for Lecture 13 (propositional logic) and Lecture 14 (predicate logic). The rules magic and raa (reductio ad absurdum) are part of classical logic but not intuitionistic logic. The rule magic is the axiom (rule without any premises) P ∨ ¬P.

Examples

Example 1: A ∧ ¬A ⇒ ⊥

Enter theorem:
P & ~P -> 0
Theorem: P & ~P -> 0  (* the theorem to be proved is displayed *)
Proof: T0             (* this is the extracted computational content of the proof *)
1 task(s)             (* initially, just a free proof variable T0 *)
Current task T0:      (* there is one task for each free proof variable *)
  Premises:
    no premises
  Goal: P & ~P -> 0
? enc                 (* toggle character encoding to see the symbols *)
================================================
Theorem: P ∧ ¬P ⇒ ⊥  (* if you see garbage here, just toggle back *)
Proof: T0
1 task(s)
Current task T0:
  Premises:
    no premises
  Goal: P ∧ ¬P ⇒ ⊥
? ->i                (* we wish to apply -> introduction *)
================================================
Theorem: P ∧ ¬P ⇒ ⊥
Proof: (fun x0 -> T0)
1 task(s)
Current task T0:
  Premises:
    x0: P ∧ ¬P       (* -> intro introduces the lhs as a premise *)
  Goal: ⊥            (* the goal is the rhs *)
? ->e P              (* now apply -> elim with lhs P *)
================================================
Theorem: P ∧ ¬P ⇒ ⊥
Proof: (fun x0 -> (T1 T0))
2 task(s)            (* this creates 2 new tasks, to prove P and to *)
Current task T0:     (* prove P -> 0 from the premise P & ~P *)
  Premises:
    x0: P ∧ ¬P
  Goal: P
? tasks              (* type 'tasks' to see the remaining tasks *)
T0:
  Premises:
    x0: P ∧ ¬P
  Goal: P
T1:
  Premises:
    x0: P ∧ ¬P
  Goal: P ⇒ ⊥
================================================
Theorem: P ∧ ¬P ⇒ ⊥
Proof: (fun x0 -> (T1 T0))
2 task(s)
Current task T0:
  Premises:
    x0: P ∧ ¬P
  Goal: P
? &el ~P            (* apply &-elim-left to use P from the premise *)
================================================
Theorem: P ∧ ¬P ⇒ ⊥
Proof: (fun x0 -> (T1 (fst T0)))
2 task(s)
Current task T0:
  Premises:
    x0: P ∧ ¬P
  Goal: P ∧ ¬P
? use x0             (* now we can use the premise, completing task T0 *)
================================================
Theorem: P ∧ ¬P ⇒ ⊥
Proof: (fun x0 -> (T1 (fst x0))) (* note that T0 disappeared in the extract term *)
1 task(s)
Current task T1:
  Premises:
    x0: P ∧ ¬P
  Goal: P ⇒ ⊥
? ~e                 (* apply ~ elim to change P -> 0 to ~P *)
================================================
Theorem: P ∧ ¬P ⇒ ⊥
Proof: (fun x0 -> (T1 (fst x0)))
1 task(s)
Current task T1:
  Premises:
    x0: P ∧ ¬P
  Goal: ¬P
? &er P             (* apply &-elim-right to use ~P from the premise *)
================================================
Theorem: P ∧ ¬P ⇒ ⊥
Proof: (fun x0 -> ((snd T1) (fst x0)))
1 task(s)
Current task T1:
  Premises:
    x0: P ∧ ¬P
  Goal: P ∧ ¬P
? use x0           (* just use the premise *)
================================================
Theorem: P ∧ ¬P ⇒ ⊥
Proof: (fun x0 -> ((snd x0) (fst x0))) (* no free proof variables remaining *)
No tasks           (* the proof is complete *)
? latex ex1.tex    (* write it out to a LaTeX file *)

This is an intuitionistic proof, so the extract term is executable. Here are the LaTeX source of the proof and the PDF file produced from it.

Example 2: ¬∃x.(P(x) ∧ ¬P(x))

Enter theorem:
~#x.(P(x) & ~P(x)) 
Theorem: ¬∃x.(P(x) ∧ ¬P(x))
Proof: T0
1 task(s)
Current task T0:
  Premises:
    no premises
  Goal: ¬∃x.(P(x) ∧ ¬P(x))
? ~i
================================================
Theorem: ¬∃x.(P(x) ∧ ¬P(x))
Proof: T0
1 task(s)
Current task T0:
  Premises:
    no premises
  Goal: ∃x.(P(x) ∧ ¬P(x)) ⇒ ⊥
? ->i
================================================
Theorem: ¬∃x.(P(x) ∧ ¬P(x))
Proof: (fun x0 -> T0)
1 task(s)
Current task T0:
  Premises:
    x0: ∃x.(P(x) ∧ ¬P(x))
  Goal: ⊥
? Ee x0       (* if a required argument of a rule is a premise, just type the name *)
================================================
Theorem: ¬∃x.(P(x) ∧ ¬P(x))
Proof: (fun x0 -> (Out a T0 T1))
2 task(s)
Current task T0:
  Premises:
    x0: ∃x.(P(x) ∧ ¬P(x))
  Goal: ∃x.(P(x) ∧ ¬P(x))
? use x0
================================================
Theorem: ¬∃x.(P(x) ∧ ¬P(x))
Proof: (fun x0 -> (Out a x0 T1))
1 task(s)
Current task T1:
  Premises:
    x0: ∃x.(P(x) ∧ ¬P(x))
  Goal: P(a) ∧ ¬P(a) ⇒ ⊥
? ...         (* the remainder of the proof is just like Ex. 1 *)
================================================
Theorem: ¬∃x.(P(x) ∧ ¬P(x))
Proof: (fun x0 -> (Out a x0 (fun x1 -> ((snd x1) (fst x1)))))
No tasks
? latex ex2.tex

Example 3: ¬¬P ⇒ P

This example requires the use of magic or raa, because it is not intuitionistically valid.

Enter theorem:
~~P -> P
Theorem: ¬¬P ⇒ P
Proof: T0
1 task(s)
Current task T0:
  Premises:
    no premises
  Goal: ¬¬P ⇒ P
? ->i
================================================
Theorem: ¬¬P ⇒ P
Proof: (fun x0 -> T0)
1 task(s)
Current task T0:
  Premises:
    x0: ¬¬P
  Goal: P
? raa
================================================
Theorem: ¬¬P ⇒ P
Proof: (fun x0 -> (fun x1 -> T0))
1 task(s)
Current task T0:
  Premises:
    x1: ¬P
    x0: ¬¬P
  Goal: ⊥
? ->e ~P
================================================
Theorem: ¬¬P ⇒ P
Proof: (fun x0 -> (fun x1 -> (T1 T0)))
2 task(s)
Current task T0:
  Premises:
    x1: ¬P
    x0: ¬¬P
  Goal: ¬P
? use x1
================================================
Theorem: ¬¬P ⇒ P
Proof: (fun x0 -> (fun x1 -> (T1 x1)))
1 task(s)
Current task T1:
  Premises:
    x1: ¬P
    x0: ¬¬P
  Goal: ¬P ⇒ ⊥
? ~e
================================================
Theorem: ¬¬P ⇒ P
Proof: (fun x0 -> (fun x1 -> (T1 x1)))
1 task(s)
Current task T1:
  Premises:
    x1: ¬P
    x0: ¬¬P
  Goal: ¬¬P
? use x0
================================================
Theorem: ¬¬P ⇒ P
Proof: (fun x0 -> (fun x1 -> (x0 x1)))
No tasks
? latex ex3.tex