george: User Manual

[ Introduction ] [ File Structure ] [ #check PROP ] [ #check PRED ] [ #check PREDTYPES ] [ #check TP ]
[ #check ND ] [ #check ST ] [ Arithmetic ] [ Sets ] [ #check Z ] [ #check PC ]
[ Contributions by Students ] [ Credits ] Keywords ]

Natural Deduction Proofs (#check ND)

Here is an example of the response to a question that requires a natural deduction proof:

#check ND

p => !p  |-  !p

1) p => !p premise
2) disprove p {
  3) !p by imp_e on 1,2 
  4) false by not_e on 2, 3
}
5) !p by raa on 2-4

The same directive (#check ND) is used for both propositional and predicate logic natural deduction proofs.

The lines are labelled by a string (e.g., the "1" in "1)" at the beginning of a line). The string may not include ".". These strings must be unique, but they do not have to follow a linear order.

After the directive (#check ND), george expects the first non-comment line to be the goal of the proof (a line that includes |-). Following this line should be a sequence of proof steps, where each proof step is of one of the following forms:

• For the premises of the proof:

  n) formula premise 
  

• For the rules that do not require subproofs,

   
  n) formula by rule on x,y,... 
  

  These rules are:

  Introduction	Elimination
  true
  and_i	and_e
  or_i	or_e
  lem
  	imp_e
  	not_e
  not_not_i	not_not_e
  iff_i	iff_e
  trans	iff_mp
  exists_i
  	forall_e
  eq_i	eq_e

• For rules that require subproofs with subproofopenings/subproofrules:

  n) subproofopening formula {
     n1) ...
     n2) proof steps
     n3)...
  }
  n4) formula by subproofrule on relevant_line_labels
  

  These rules are:

  Subproof opening	Subproof rule	Relevant Line Labels
  disprove	raa	beginning of subproof - end of subproof
  case	cases	label of disjunction of case split, beginning of 1st case subproof - end of 1st case subproof, beginning of 2nd case subproof - end of 2nd case subproof, etc.
  assume	imp_i	beginning of subproof - end of subproof
  for every _var_name_	forall_i	beginning of subproof - end of subproof
  for some _var_name_ assume	exists_e	label of exists formula, beginning of subproof - end of subproof

  Subproofs must be enclosed in "{" ... "}". Indentation and whitespace is not required but recommended for readability.

These rules are summarized on our summary page on natural deduction for propositional logic .

Here is an example of a natural deduction proof that uses the cases rule:

#check ND

a | b, a => c, b => c  |-  c

1) a | b    premise
2) a => c   premise
3) b => c   premise
4) case a {
    5) c by imp_e on 4,2
    }
6) case b {
    7) c by imp_e on 6,3
    }
8) c by cases on 1, 4-5, 6-7

Here is an example using the forall_i rule:

#check ND

forall x . P(x) => Q(x), forall x . P(x)   |-  forall x . Q(x)

1) forall x. P(x) => Q(x) premise
2) forall x . P(x) premise
3) for every xg {
	4) P(xg) => Q(xg)   by forall_e on 1
	5) P(xg)            by forall_e on 2
	6) Q(xg)            by imp_e on 4,5
	}
7) forall x. Q(x)           by forall_i on 3-6

Here is an example using the exists_e rule:

#check ND

forall x . P(x) => Q(x),  exists x . P(x) |- exists x . Q(x)

1) forall x . P(x) => Q(x) 	premise
2) exists x. P(x) 		premise
3) for some xu assume P(xu) {
   4) P(xu) => Q(xu)    by forall_e on 1
   5) Q(xu)             by imp_e on 3,4
   6) exists x . Q(x)   by exists_i on 5
   }
7) exists x . Q(x)           by exists_e on 2, 3-6

These rules are summarized on our summary page on natural deduction for propositional logic .

George matches the rule with any commutative/associative variants of a top-level conjunction/disjunction formula. It does NOT consider commutative/associative variants at any deeper level.

george supports one additional rule to allows you make progress on your proof in a non-linear manner: the ``magic'' rule. The magic rule allows you to conclude any formula at any step in the proof. For example, if you were unable to complete the subproof in the earlier example, you could do:

#q 5

#check ND

p => !p  |-  !p

1) p => !p premise
2) disprove p {
  3) false by magic
}

george will state an error that you have used the magic rule and give you feedback regarding whether the other proof steps are correct or not. Of course, the TAs will notice that you have used ``magic'' and you will not receive full marks for the question!

What does george check?

For natural deduction proofs, george checks:

• Each formula is syntactically correct.
• Each formula typechecks.
• The name of each proof rule is a valid rule.
• The format of the proof is correct.
• The proof rule has been correctly applied unless checking correctness times out. This includes checking that the line number the rule uses are the correct ones and that the substitutions are correct.

If george encounters an error in the proof, it provides you with feedback and then continues its correctness analysis as if the incorrect line had been correct (i.e., as if it had been a magic step) in order to provide you with as much feedback as possible.