]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/ng_TPTP/LCL157-1.ma
arithmetics for λδ
[helm.git] / matita / matita / contribs / ng_TPTP / LCL157-1.ma
1 include "logic/equality.ma".
2
3 (* Inclusion of: LCL157-1.p *)
4
5 (* -------------------------------------------------------------------------- *)
6
7 (*  File     : LCL157-1 : TPTP v3.7.0. Released v1.0.0. *)
8
9 (*  Domain   : Logic Calculi (Wajsberg Algebra) *)
10
11 (*  Problem  : The 5th alternative Wajsberg algebra axiom *)
12
13 (*  Version  : [Bon91] (equality) axioms. *)
14
15 (*  English  :  *)
16
17 (*  Refs     : [FRT84] Font et al. (1984), Wajsberg Algebras *)
18
19 (*           : [AB90]  Anantharaman & Bonacina (1990), An Application of the  *)
20
21 (*           : [Bon91] Bonacina (1991), Problems in Lukasiewicz Logic *)
22
23 (*  Source   : [Bon91] *)
24
25 (*  Names    : W' axiom 5 [Bon91] *)
26
27 (*  Status   : Unsatisfiable *)
28
29 (*  Rating   : 0.00 v2.2.1, 0.22 v2.2.0, 0.29 v2.1.0, 0.38 v2.0.0 *)
30
31 (*  Syntax   : Number of clauses     :   17 (   0 non-Horn;  17 unit;   2 RR) *)
32
33 (*             Number of atoms       :   17 (  17 equality) *)
34
35 (*             Maximal clause size   :    1 (   1 average) *)
36
37 (*             Number of predicates  :    1 (   0 propositional; 2-2 arity) *)
38
39 (*             Number of functors    :    9 (   3 constant; 0-2 arity) *)
40
41 (*             Number of variables   :   33 (   0 singleton) *)
42
43 (*             Maximal term depth    :    4 (   2 average) *)
44
45 (*  Comments :  *)
46
47 (* -------------------------------------------------------------------------- *)
48
49 (* ----Include Wajsberg algebra axioms  *)
50
51 (* Inclusion of: Axioms/LCL001-0.ax *)
52
53 (* -------------------------------------------------------------------------- *)
54
55 (*  File     : LCL001-0 : TPTP v3.7.0. Released v1.0.0. *)
56
57 (*  Domain   : Logic Calculi (Wajsberg Algebras) *)
58
59 (*  Axioms   : Wajsberg algebra axioms *)
60
61 (*  Version  : [Bon91] (equality) axioms. *)
62
63 (*  English  :  *)
64
65 (*  Refs     : [FRT84] Font et al. (1984), Wajsberg Algebras *)
66
67 (*           : [Bon91] Bonacina (1991), Problems in Lukasiewicz Logic *)
68
69 (*           : [MW92]  McCune & Wos (1992), Experiments in Automated Deductio *)
70
71 (*  Source   : [MW92] *)
72
73 (*  Names    : MV Sentential Calculus [MW92] *)
74
75 (*  Status   :  *)
76
77 (*  Syntax   : Number of clauses    :    4 (   0 non-Horn;   4 unit;   0 RR) *)
78
79 (*             Number of atoms      :    4 (   4 equality) *)
80
81 (*             Maximal clause size  :    1 (   1 average) *)
82
83 (*             Number of predicates :    1 (   0 propositional; 2-2 arity) *)
84
85 (*             Number of functors   :    3 (   1 constant; 0-2 arity) *)
86
87 (*             Number of variables  :    8 (   0 singleton) *)
88
89 (*             Maximal term depth   :    4 (   2 average) *)
90
91 (*  Comments :  *)
92
93 (* -------------------------------------------------------------------------- *)
94
95 (* -------------------------------------------------------------------------- *)
96
97 (* ----Include Wajsberg algebra and and or definitions  *)
98
99 (* Inclusion of: Axioms/LCL001-2.ax *)
100
101 (* -------------------------------------------------------------------------- *)
102
103 (*  File     : LCL001-2 : TPTP v3.7.0. Released v1.0.0. *)
104
105 (*  Domain   : Logic Calculi (Wajsberg Algebras) *)
106
107 (*  Axioms   : Wajsberg algebra AND and OR definitions *)
108
109 (*  Version  : [AB90] (equality) axioms. *)
110
111 (*  English  :  *)
112
113 (*  Refs     : [FRT84] Font et al. (1984), Wajsberg Algebras *)
114
115 (*           : [AB90]  Anantharaman & Bonacina (1990), An Application of the  *)
116
117 (*           : [Bon91] Bonacina (1991), Problems in Lukasiewicz Logic *)
118
119 (*  Source   : [Bon91] *)
120
121 (*  Names    :  *)
122
123 (*  Status   :  *)
124
125 (*  Syntax   : Number of clauses    :    6 (   0 non-Horn;   6 unit;   0 RR) *)
126
127 (*             Number of atoms      :    6 (   6 equality) *)
128
129 (*             Maximal clause size  :    1 (   1 average) *)
130
131 (*             Number of predicates :    1 (   0 propositional; 2-2 arity) *)
132
133 (*             Number of functors   :    4 (   0 constant; 1-2 arity) *)
134
135 (*             Number of variables  :   14 (   0 singleton) *)
136
137 (*             Maximal term depth   :    4 (   3 average) *)
138
139 (*  Comments : Requires LCL001-0.ax *)
140
141 (* -------------------------------------------------------------------------- *)
142
143 (* ----Definitions of or and and, which are AC  *)
144
145 (* -------------------------------------------------------------------------- *)
146
147 (* ----Include Alternative Wajsberg algebra definitions  *)
148
149 (* Inclusion of: Axioms/LCL002-1.ax *)
150
151 (* -------------------------------------------------------------------------- *)
152
153 (*  File     : LCL002-1 : TPTP v3.7.0. Released v1.0.0. *)
154
155 (*  Domain   : Logic Calculi (Wajsberg Algebras) *)
156
157 (*  Axioms   : Alternative Wajsberg algebra definitions *)
158
159 (*  Version  : [AB90] (equality) axioms. *)
160
161 (*  English  :  *)
162
163 (*  Refs     : [FRT84] Font et al. (1984), Wajsberg Algebras *)
164
165 (*           : [AB90]  Anantharaman & Bonacina (1990), An Application of the  *)
166
167 (*           : [Bon91] Bonacina (1991), Problems in Lukasiewicz Logic *)
168
169 (*  Source   : [Bon91] *)
170
171 (*  Names    :  *)
172
173 (*  Status   :  *)
174
175 (*  Syntax   : Number of clauses    :    6 (   0 non-Horn;   6 unit;   1 RR) *)
176
177 (*             Number of atoms      :    6 (   6 equality) *)
178
179 (*             Maximal clause size  :    1 (   1 average) *)
180
181 (*             Number of predicates :    1 (   0 propositional; 2-2 arity) *)
182
183 (*             Number of functors   :    7 (   2 constant; 0-2 arity) *)
184
185 (*             Number of variables  :   11 (   0 singleton) *)
186
187 (*             Maximal term depth   :    4 (   2 average) *)
188
189 (*  Comments : Requires LCL001-0.ax LCL001-2.ax *)
190
191 (* -------------------------------------------------------------------------- *)
192
193 (* ----Definitions of and_star and xor, where and_star is AC and xor is C  *)
194
195 (* ---I guess the next two can be derived from the AC of and *)
196
197 (* ----Definition of false in terms of truth  *)
198
199 (* -------------------------------------------------------------------------- *)
200
201 (* -------------------------------------------------------------------------- *)
202 ntheorem prove_alternative_wajsberg_axiom:
203  (∀Univ:Type.∀X:Univ.∀Y:Univ.∀Z:Univ.
204 ∀myand:∀_:Univ.∀_:Univ.Univ.
205 ∀and_star:∀_:Univ.∀_:Univ.Univ.
206 ∀falsehood:Univ.
207 ∀implies:∀_:Univ.∀_:Univ.Univ.
208 ∀not:∀_:Univ.Univ.
209 ∀or:∀_:Univ.∀_:Univ.Univ.
210 ∀truth:Univ.
211 ∀x:Univ.
212 ∀xor:∀_:Univ.∀_:Univ.Univ.
213 ∀H0:eq Univ (not truth) falsehood.
214 ∀H1:∀X:Univ.∀Y:Univ.eq Univ (and_star X Y) (and_star Y X).
215 ∀H2:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (and_star (and_star X Y) Z) (and_star X (and_star Y Z)).
216 ∀H3:∀X:Univ.∀Y:Univ.eq Univ (and_star X Y) (not (or (not X) (not Y))).
217 ∀H4:∀X:Univ.∀Y:Univ.eq Univ (xor X Y) (xor Y X).
218 ∀H5:∀X:Univ.∀Y:Univ.eq Univ (xor X Y) (or (myand X (not Y)) (myand (not X) Y)).
219 ∀H6:∀X:Univ.∀Y:Univ.eq Univ (myand X Y) (myand Y X).
220 ∀H7:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (myand (myand X Y) Z) (myand X (myand Y Z)).
221 ∀H8:∀X:Univ.∀Y:Univ.eq Univ (myand X Y) (not (or (not X) (not Y))).
222 ∀H9:∀X:Univ.∀Y:Univ.eq Univ (or X Y) (or Y X).
223 ∀H10:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (or (or X Y) Z) (or X (or Y Z)).
224 ∀H11:∀X:Univ.∀Y:Univ.eq Univ (or X Y) (implies (not X) Y).
225 ∀H12:∀X:Univ.∀Y:Univ.eq Univ (implies (implies (not X) (not Y)) (implies Y X)) truth.
226 ∀H13:∀X:Univ.∀Y:Univ.eq Univ (implies (implies X Y) Y) (implies (implies Y X) X).
227 ∀H14:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (implies (implies X Y) (implies (implies Y Z) (implies X Z))) truth.
228 ∀H15:∀X:Univ.eq Univ (implies truth X) X.eq Univ (and_star x falsehood) falsehood)
229 .
230 #Univ ##.
231 #X ##.
232 #Y ##.
233 #Z ##.
234 #myand ##.
235 #and_star ##.
236 #falsehood ##.
237 #implies ##.
238 #not ##.
239 #or ##.
240 #truth ##.
241 #x ##.
242 #xor ##.
243 #H0 ##.
244 #H1 ##.
245 #H2 ##.
246 #H3 ##.
247 #H4 ##.
248 #H5 ##.
249 #H6 ##.
250 #H7 ##.
251 #H8 ##.
252 #H9 ##.
253 #H10 ##.
254 #H11 ##.
255 #H12 ##.
256 #H13 ##.
257 #H14 ##.
258 #H15 ##.
259 nauto by H0,H1,H2,H3,H4,H5,H6,H7,H8,H9,H10,H11,H12,H13,H14,H15 ##;
260 ntry (nassumption) ##;
261 nqed.
262
263 (* -------------------------------------------------------------------------- *)