next up previous contents
Next: About this document ... Up: Natural Deduction Language Previous: Existential quantifier elimination   Contents

Examples

Below are the verbatin 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 a for (exists x ~P(x)) 
      begin
        specialize (forall x P(x)) with a;
        absurd P(a), ~P(a)
      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) & Q(x)) ==> (exists x ~P(x))
//
// I.e., if there isn't anything 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-04