86 Ex1 (binder "\<exists>!" 10) |
86 Ex1 (binder "\<exists>!" 10) |
87 |
87 |
88 finalconsts |
88 finalconsts |
89 False All Ex eq conj disj imp |
89 False All Ex eq conj disj imp |
90 |
90 |
91 axioms |
91 axiomatization where |
92 |
|
93 (* Equality *) |
92 (* Equality *) |
94 |
93 refl: "a=a" and |
95 refl: "a=a" |
|
96 subst: "a=b \<Longrightarrow> P(a) \<Longrightarrow> P(b)" |
94 subst: "a=b \<Longrightarrow> P(a) \<Longrightarrow> P(b)" |
97 |
95 |
|
96 |
|
97 axiomatization where |
98 (* Propositional logic *) |
98 (* Propositional logic *) |
99 |
99 conjI: "[| P; Q |] ==> P&Q" and |
100 conjI: "[| P; Q |] ==> P&Q" |
100 conjunct1: "P&Q ==> P" and |
101 conjunct1: "P&Q ==> P" |
101 conjunct2: "P&Q ==> Q" and |
102 conjunct2: "P&Q ==> Q" |
102 |
103 |
103 disjI1: "P ==> P|Q" and |
104 disjI1: "P ==> P|Q" |
104 disjI2: "Q ==> P|Q" and |
105 disjI2: "Q ==> P|Q" |
105 disjE: "[| P|Q; P ==> R; Q ==> R |] ==> R" and |
106 disjE: "[| P|Q; P ==> R; Q ==> R |] ==> R" |
106 |
107 |
107 impI: "(P ==> Q) ==> P-->Q" and |
108 impI: "(P ==> Q) ==> P-->Q" |
108 mp: "[| P-->Q; P |] ==> Q" and |
109 mp: "[| P-->Q; P |] ==> Q" |
|
110 |
109 |
111 FalseE: "False ==> P" |
110 FalseE: "False ==> P" |
112 |
111 |
|
112 axiomatization where |
113 (* Quantifiers *) |
113 (* Quantifiers *) |
114 |
114 allI: "(!!x. P(x)) ==> (ALL x. P(x))" and |
115 allI: "(!!x. P(x)) ==> (ALL x. P(x))" |
115 spec: "(ALL x. P(x)) ==> P(x)" and |
116 spec: "(ALL x. P(x)) ==> P(x)" |
116 |
117 |
117 exI: "P(x) ==> (EX x. P(x))" and |
118 exI: "P(x) ==> (EX x. P(x))" |
|
119 exE: "[| EX x. P(x); !!x. P(x) ==> R |] ==> R" |
118 exE: "[| EX x. P(x); !!x. P(x) ==> R |] ==> R" |
120 |
119 |
121 |
120 |
122 axioms |
121 axiomatization where |
123 |
|
124 (* Reflection, admissible *) |
122 (* Reflection, admissible *) |
125 |
123 eq_reflection: "(x=y) ==> (x==y)" and |
126 eq_reflection: "(x=y) ==> (x==y)" |
|
127 iff_reflection: "(P<->Q) ==> (P==Q)" |
124 iff_reflection: "(P<->Q) ==> (P==Q)" |
128 |
125 |
129 |
126 |
130 lemmas strip = impI allI |
127 lemmas strip = impI allI |
131 |
128 |