Next: About this document ...
Up: Natural Deduction Language
Previous: Existential quantifier elimination
  Contents
Below are the verbatim contents of the file examples.ndl that comes
with the NDL distribution. The user can load this file all at once
and observe the output, or experiment by cutting and pasting
bits and pieces. Regarding comments: everything from
a double slash // all the way to the end of the line
is ignored.
//********************************************************************
//********************************************************************
//
// Some examples illustrating proofs in NDL.
//
// Last updated on July 31, 2004.
//
// Konstantine Arkoudas, konstantine@alum.mit.edu
//********************************************************************
//********************************************************************
// We begin by introducing a small "signature": a few
// relation symbols and a couple of constant symbols.
// The notation S:n indicates that the arity of the
// symbol S is n.
Relations P:1, Q:1, R:2, S:1, T:1, A:0, B:0.
Constants c, d.
//******************************************************
// EXAMPLE 1
//******************************************************
// The first proof derives the tautology
// A & B ==> B & A
assume A & B
begin
left-and A & B; // this gives you A
right-and A & B; // this gives B
both B, A // this gets B & A
end
//******************************************************
// EXAMPLE 2
//******************************************************
// The second proof derives the tautology
// (forall x P(x)) ==> ~ (exists x ~ P(x))
//
// E.g., if everything is red then there isn't anything
// that is NOT red.
assume (forall x P(x))
suppose-absurd (exists x ~P(x))
pick-witness w for (exists x ~P(x)) // we now have ~P(w)
begin
P(w) BY pecialize (forall x P(x)) with w;
absurd P(w), ~P(w)
end.
//******************************************************
// EXAMPLE 3
//******************************************************
// The third proof derives the tautology
// [forall x P(x) & Q(x)] ==> [(forall y P(y)) & (forall y Q(y))]
assume [forall x P(x) & Q(x)]
begin
pick-any y
begin
specialize (forall x P(x) & Q(x)) with y;
left-and P(y) & Q(y)
end;
pick-any y
begin
specialize (forall x P(x) & Q(x)) with y;
right-and P(y) & Q(y)
end;
both (forall y P(y)), (forall (y) Q(y))
end
//******************************************************
// EXAMPLE 4
//******************************************************
// The fourth proof derives the tautology
// ~ [forall x P(x)] ==> [exists x ~P(x)]
//
// I.e., if it's not the case that everything is red, there must be
// something that is not red. (Recall that in first-order logic the
// universe of discourse is always non-empty.)
assume ~(forall x P(x))
begin
suppose-absurd ~(exists x ~P(x))
begin
pick-any y
begin
suppose-absurd ~P(y)
begin
ex-generalize (exists x ~P(x)) from y;
absurd (exists x ~P(x)), ~(exists x ~P(x))
end;
double-negation ~~P(y)
end;
absurd (forall x P(x)), ~(forall x P(x))
end;
double-negation ~~(exists x ~P(x))
end
//******************************************************
// EXAMPLE 5
//******************************************************
// The fifth proof derives the tautology
// [forall x (forall y R(x,y))] ==>
// [forall x (forall y R(y,x))]
assume (forall x (forall y R(x,y)))
pick-any x1
pick-any x2
begin
specialize (forall x (forall y R(x,y))) with x2;
specialize (forall y R(x2,y)) with x1
end
//******************************************************
// EXAMPLE 6
//******************************************************
// The sixth proof derives the tautology
// [forall x P(x) & Q(x)] ==>
// [forall x Q(x) ==> T(x)] ==> (forall y T(y))
assume (forall x P(x) & Q(x))
assume (forall x Q(x) ==> T(x))
pick-any y
begin
specialize (forall x P(x) & Q(x)) with y;
right-and P(y) & Q(y);
specialize (forall x Q(x) ==> T(x)) with y;
modus-ponens Q(y) ==> T(y), Q(y)
end
//******************************************************
// EXAMPLE 7
//******************************************************
// The seventh proof derives the tautology
// [forall x P(y) ==> Q(x)] ==> [P(y) ==> (forall x Q(x))]
//
assume (forall x P(y) ==> Q(x))
assume P(y)
pick-any z
begin
specialize (forall x P(y) ==> Q(x)) with z;
modus-ponens P(y) ==> Q(z), P(y)
end
//******************************************************
// EXAMPLE 8
//******************************************************
// The eigth proof derives the tautology
// [forall x P(x) ==> Q(x)] ==>
// [exists x S(x) & P(x)] ==> [exists x Q(x) & S(x)]
assume (forall x P(x) ==> Q(x))
assume (exists x S(x) & P(x))
pick-witness z for (exists x S(x) & P(x))
begin
right-and S(z) & P(z);
specialize (forall x P(x) ==> Q(x)) with z;
modus-ponens P(z) ==> Q(z), P(z);
left-and S(z) & P(z);
both Q(z), S(z);
ex-generalize (exists y Q(y) & S(y)) from z
end
//******************************************************
// EXAMPLE 9
//******************************************************
// The ninth proof derives the tautology
// [exists x (exists y R(x,y))] ==> [exists y (exists x R(x,y))]
assume (exists x (exists y R(x,y)))
pick-witness x1 for (exists x (exists y R(x,y)))
pick-witness y1 for (exists y R(x1,y))
begin
ex-generalize (exists foo R(foo,y1)) from x1;
ex-generalize (exists y (exists x R(x,y))) from y1
end
2004-08-06