src/HOL/ex/Intuitionistic.thy
author kleing
Sat, 01 Mar 2003 16:45:51 +0100
changeset 13840 399c8103a98f
parent 12450 1162b280700a
child 16417 9bc16273c2d4
permissions -rw-r--r--
keep a copy of generated files in repository
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
12450
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
     1
(*  Title:      HOL/ex/Intuitionistic.thy
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
     2
    ID:         $Id$
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
     4
    Copyright   1991  University of Cambridge
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
     5
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
     6
Higher-Order Logic: Intuitionistic predicate calculus problems
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
     7
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
     8
Taken from FOL/ex/int.ML
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
     9
*)
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    10
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    11
theory Intuitionistic = Main:
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    12
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    13
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    14
(*Metatheorem (for PROPOSITIONAL formulae...):
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    15
  P is classically provable iff ~~P is intuitionistically provable.
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    16
  Therefore ~P is classically provable iff it is intuitionistically provable.  
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    17
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    18
Proof: Let Q be the conjuction of the propositions A|~A, one for each atom A
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    19
in P.  Now ~~Q is intuitionistically provable because ~~(A|~A) is and because
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    20
~~ distributes over &.  If P is provable classically, then clearly Q-->P is
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    21
provable intuitionistically, so ~~(Q-->P) is also provable intuitionistically.
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    22
The latter is intuitionistically equivalent to ~~Q-->~~P, hence to ~~P, since
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    23
~~Q is intuitionistically provable.  Finally, if P is a negation then ~~P is
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    24
intuitionstically equivalent to P.  [Andy Pitts] *)
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    25
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    26
lemma "(~~(P&Q)) = ((~~P) & (~~Q))"
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    27
  by rules
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    28
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    29
lemma "~~ ((~P --> Q) --> (~P --> ~Q) --> P)"
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    30
  by rules
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    31
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    32
(* ~~ does NOT distribute over | *)
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    33
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    34
lemma "(~~(P-->Q))  = (~~P --> ~~Q)"
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    35
  by rules
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    36
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    37
lemma "(~~~P) = (~P)"
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    38
  by rules
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    39
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    40
lemma "~~((P --> Q | R)  -->  (P-->Q) | (P-->R))"
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    41
  by rules
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    42
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    43
lemma "(P=Q) = (Q=P)"
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    44
  by rules
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    45
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    46
lemma "((P --> (Q | (Q-->R))) --> R) --> R"
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    47
  by rules
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    48
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    49
lemma "(((G-->A) --> J) --> D --> E) --> (((H-->B)-->I)-->C-->J)
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    50
      --> (A-->H) --> F --> G --> (((C-->B)-->I)-->D)-->(A-->C)
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    51
      --> (((F-->A)-->B) --> I) --> E"
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    52
  by rules
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    53
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    54
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    55
(* Lemmas for the propositional double-negation translation *)
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    56
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    57
lemma "P --> ~~P"
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    58
  by rules
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    59
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    60
lemma "~~(~~P --> P)"
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    61
  by rules
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    62
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    63
lemma "~~P & ~~(P --> Q) --> ~~Q"
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    64
  by rules
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    65
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    66
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    67
(* de Bruijn formulae *)
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    68
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    69
(*de Bruijn formula with three predicates*)
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    70
lemma "((P=Q) --> P&Q&R) &
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    71
       ((Q=R) --> P&Q&R) &
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    72
       ((R=P) --> P&Q&R) --> P&Q&R"
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    73
  by rules
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    74
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    75
(*de Bruijn formula with five predicates*)
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    76
lemma "((P=Q) --> P&Q&R&S&T) &
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    77
       ((Q=R) --> P&Q&R&S&T) &
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    78
       ((R=S) --> P&Q&R&S&T) &
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    79
       ((S=T) --> P&Q&R&S&T) &
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    80
       ((T=P) --> P&Q&R&S&T) --> P&Q&R&S&T"
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    81
  by rules
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    82
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    83
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    84
(*** Problems from Sahlin, Franzen and Haridi, 
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    85
     An Intuitionistic Predicate Logic Theorem Prover.
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    86
     J. Logic and Comp. 2 (5), October 1992, 619-656.
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    87
***)
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    88
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    89
(*Problem 1.1*)
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    90
lemma "(ALL x. EX y. ALL z. p(x) & q(y) & r(z)) =
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    91
       (ALL z. EX y. ALL x. p(x) & q(y) & r(z))"
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    92
  by (rules del: allE elim 2: allE')
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    93
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    94
(*Problem 3.1*)
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    95
lemma "~ (EX x. ALL y. p y x = (~ p x x))"
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    96
  by rules
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    97
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    98
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
    99
(* Intuitionistic FOL: propositional problems based on Pelletier. *)
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   100
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   101
(* Problem ~~1 *)
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   102
lemma "~~((P-->Q)  =  (~Q --> ~P))"
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   103
  by rules
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   104
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   105
(* Problem ~~2 *)
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   106
lemma "~~(~~P  =  P)"
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   107
  by rules
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   108
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   109
(* Problem 3 *)
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   110
lemma "~(P-->Q) --> (Q-->P)"
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   111
  by rules
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   112
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   113
(* Problem ~~4 *)
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   114
lemma "~~((~P-->Q)  =  (~Q --> P))"
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   115
  by rules
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   116
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   117
(* Problem ~~5 *)
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   118
lemma "~~((P|Q-->P|R) --> P|(Q-->R))"
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   119
  by rules
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   120
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   121
(* Problem ~~6 *)
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   122
lemma "~~(P | ~P)"
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   123
  by rules
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   124
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   125
(* Problem ~~7 *)
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   126
lemma "~~(P | ~~~P)"
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   127
  by rules
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   128
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   129
(* Problem ~~8.  Peirce's law *)
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   130
lemma "~~(((P-->Q) --> P)  -->  P)"
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   131
  by rules
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   132
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   133
(* Problem 9 *)
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   134
lemma "((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)"
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   135
  by rules
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   136
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   137
(* Problem 10 *)
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   138
lemma "(Q-->R) --> (R-->P&Q) --> (P-->(Q|R)) --> (P=Q)"
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   139
  by rules
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   140
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   141
(* 11.  Proved in each direction (incorrectly, says Pelletier!!) *)
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   142
lemma "P=P"
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   143
  by rules
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   144
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   145
(* Problem ~~12.  Dijkstra's law *)
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   146
lemma "~~(((P = Q) = R)  =  (P = (Q = R)))"
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   147
  by rules
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   148
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   149
lemma "((P = Q) = R)  -->  ~~(P = (Q = R))"
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   150
  by rules
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   151
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   152
(* Problem 13.  Distributive law *)
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   153
lemma "(P | (Q & R))  = ((P | Q) & (P | R))"
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   154
  by rules
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   155
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   156
(* Problem ~~14 *)
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   157
lemma "~~((P = Q) = ((Q | ~P) & (~Q|P)))"
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   158
  by rules
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   159
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   160
(* Problem ~~15 *)
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   161
lemma "~~((P --> Q) = (~P | Q))"
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   162
  by rules
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   163
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   164
(* Problem ~~16 *)
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   165
lemma "~~((P-->Q) | (Q-->P))"
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   166
by rules
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   167
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   168
(* Problem ~~17 *)
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   169
lemma "~~(((P & (Q-->R))-->S) = ((~P | Q | S) & (~P | ~R | S)))"
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   170
  oops
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   171
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   172
(*Dijkstra's "Golden Rule"*)
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   173
lemma "(P&Q) = (P = (Q = (P|Q)))"
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   174
  by rules
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   175
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   176
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   177
(****Examples with quantifiers****)
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   178
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   179
(* The converse is classical in the following implications... *)
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   180
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   181
lemma "(EX x. P(x)-->Q)  -->  (ALL x. P(x)) --> Q"
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   182
  by rules
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   183
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   184
lemma "((ALL x. P(x))-->Q) --> ~ (ALL x. P(x) & ~Q)"
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   185
  by rules
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   186
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   187
lemma "((ALL x. ~P(x))-->Q)  -->  ~ (ALL x. ~ (P(x)|Q))"
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   188
  by rules
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   189
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   190
lemma "(ALL x. P(x)) | Q  -->  (ALL x. P(x) | Q)"
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   191
  by rules 
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   192
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   193
lemma "(EX x. P --> Q(x)) --> (P --> (EX x. Q(x)))"
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   194
  by rules
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   195
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   196
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   197
(* Hard examples with quantifiers *)
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   198
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   199
(*The ones that have not been proved are not known to be valid!
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   200
  Some will require quantifier duplication -- not currently available*)
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   201
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   202
(* Problem ~~19 *)
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   203
lemma "~~(EX x. ALL y z. (P(y)-->Q(z)) --> (P(x)-->Q(x)))"
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   204
  by rules
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   205
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   206
(* Problem 20 *)
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   207
lemma "(ALL x y. EX z. ALL w. (P(x)&Q(y)-->R(z)&S(w)))
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   208
    --> (EX x y. P(x) & Q(y)) --> (EX z. R(z))"
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   209
  by rules
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   210
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   211
(* Problem 21 *)
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   212
lemma "(EX x. P-->Q(x)) & (EX x. Q(x)-->P) --> ~~(EX x. P=Q(x))"
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   213
  by rules
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   214
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   215
(* Problem 22 *)
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   216
lemma "(ALL x. P = Q(x))  -->  (P = (ALL x. Q(x)))"
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   217
  by rules
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   218
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   219
(* Problem ~~23 *)
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   220
lemma "~~ ((ALL x. P | Q(x))  =  (P | (ALL x. Q(x))))"
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   221
  by rules
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   222
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   223
(* Problem 25 *)
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   224
lemma "(EX x. P(x)) &
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   225
       (ALL x. L(x) --> ~ (M(x) & R(x))) &
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   226
       (ALL x. P(x) --> (M(x) & L(x))) &
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   227
       ((ALL x. P(x)-->Q(x)) | (EX x. P(x)&R(x)))
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   228
   --> (EX x. Q(x)&P(x))"
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   229
  by rules
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   230
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   231
(* Problem 27 *)
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   232
lemma "(EX x. P(x) & ~Q(x)) &
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   233
             (ALL x. P(x) --> R(x)) &
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   234
             (ALL x. M(x) & L(x) --> P(x)) &
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   235
             ((EX x. R(x) & ~ Q(x)) --> (ALL x. L(x) --> ~ R(x)))
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   236
         --> (ALL x. M(x) --> ~L(x))"
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   237
  by rules
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   238
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   239
(* Problem ~~28.  AMENDED *)
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   240
lemma "(ALL x. P(x) --> (ALL x. Q(x))) &
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   241
       (~~(ALL x. Q(x)|R(x)) --> (EX x. Q(x)&S(x))) &
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   242
       (~~(EX x. S(x)) --> (ALL x. L(x) --> M(x)))
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   243
   --> (ALL x. P(x) & L(x) --> M(x))"
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   244
  by rules
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   245
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   246
(* Problem 29.  Essentially the same as Principia Mathematica *11.71 *)
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   247
lemma "(((EX x. P(x)) & (EX y. Q(y))) -->
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   248
   (((ALL x. (P(x) --> R(x))) & (ALL y. (Q(y) --> S(y)))) =
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   249
    (ALL x y. ((P(x) & Q(y)) --> (R(x) & S(y))))))"
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   250
  by rules
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   251
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   252
(* Problem ~~30 *)
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   253
lemma "(ALL x. (P(x) | Q(x)) --> ~ R(x)) &
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   254
       (ALL x. (Q(x) --> ~ S(x)) --> P(x) & R(x))
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   255
   --> (ALL x. ~~S(x))"
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   256
  by rules
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   257
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   258
(* Problem 31 *)
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   259
lemma "~(EX x. P(x) & (Q(x) | R(x))) & 
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   260
        (EX x. L(x) & P(x)) &
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   261
        (ALL x. ~ R(x) --> M(x))
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   262
    --> (EX x. L(x) & M(x))"
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   263
  by rules
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   264
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   265
(* Problem 32 *)
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   266
lemma "(ALL x. P(x) & (Q(x)|R(x))-->S(x)) &
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   267
       (ALL x. S(x) & R(x) --> L(x)) &
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   268
       (ALL x. M(x) --> R(x))
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   269
   --> (ALL x. P(x) & M(x) --> L(x))"
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   270
  by rules
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   271
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   272
(* Problem ~~33 *)
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   273
lemma "(ALL x. ~~(P(a) & (P(x)-->P(b))-->P(c)))  =
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   274
       (ALL x. ~~((~P(a) | P(x) | P(c)) & (~P(a) | ~P(b) | P(c))))"
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   275
  oops
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   276
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   277
(* Problem 36 *)
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   278
lemma
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   279
     "(ALL x. EX y. J x y) &
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   280
      (ALL x. EX y. G x y) &
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   281
      (ALL x y. J x y | G x y --> (ALL z. J y z | G y z --> H x z))
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   282
  --> (ALL x. EX y. H x y)"
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   283
  by rules
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   284
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   285
(* Problem 39 *)
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   286
lemma "~ (EX x. ALL y. F y x = (~F y y))"
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   287
  by rules
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   288
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   289
(* Problem 40.  AMENDED *)
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   290
lemma "(EX y. ALL x. F x y = F x x) -->
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   291
             ~(ALL x. EX y. ALL z. F z y = (~ F z x))"
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   292
  by rules
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   293
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   294
(* Problem 44 *)
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   295
lemma "(ALL x. f(x) -->
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   296
             (EX y. g(y) & h x y & (EX y. g(y) & ~ h x y)))  &
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   297
             (EX x. j(x) & (ALL y. g(y) --> h x y))
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   298
             --> (EX x. j(x) & ~f(x))"
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   299
  by rules
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   300
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   301
(* Problem 48 *)
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   302
lemma "(a=b | c=d) & (a=c | b=d) --> a=d | b=c"
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   303
  by rules
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   304
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   305
(* Problem 51 *)
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   306
lemma "((EX z w. (ALL x y. (P x y = ((x = z) & (y = w))))) -->
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   307
  (EX z. (ALL x. (EX w. ((ALL y. (P x y = (y = w))) = (x = z))))))"
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   308
  by rules
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   309
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   310
(* Problem 52 *)
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   311
(*Almost the same as 51. *)
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   312
lemma "((EX z w. (ALL x y. (P x y = ((x = z) & (y = w))))) -->
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   313
   (EX w. (ALL y. (EX z. ((ALL x. (P x y = (x = z))) = (y = w))))))"
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   314
  by rules
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   315
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   316
(* Problem 56 *)
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   317
lemma "(ALL x. (EX y. P(y) & x=f(y)) --> P(x)) = (ALL x. P(x) --> P(f(x)))"
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   318
  by rules
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   319
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   320
(* Problem 57 *)
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   321
lemma "P (f a b) (f b c) & P (f b c) (f a c) &
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   322
     (ALL x y z. P x y & P y z --> P x z) --> P (f a b) (f a c)"
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   323
  by rules
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   324
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   325
(* Problem 60 *)
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   326
lemma "ALL x. P x (f x) = (EX y. (ALL z. P z y --> P z (f x)) & P x y)"
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   327
  by rules
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   328
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
diff changeset
   329
end