1 include "logic/equality.ma".
3 (* Inclusion of: LCL109-6.p *)
5 (* -------------------------------------------------------------------------- *)
7 (* File : LCL109-6 : TPTP v3.7.0. Released v1.0.0. *)
9 (* Domain : Logic Calculi (Wajsberg Algebra) *)
11 (* Problem : A ntheorem in the lattice structure of Wajsberg algebras *)
13 (* Version : [Bon91] (equality) axioms : Augmented. *)
15 (* Theorem formulation : Alternative Wajsberg algebras lattice *)
21 (* Refs : [FRT84] Font et al. (1984), Wajsberg Algebras *)
23 (* : [AB90] Anantharaman & Bonacina (1990), An Application of the *)
25 (* : [Bon91] Bonacina (1991), Problems in Lukasiewicz Logic *)
27 (* Source : [Bon91] *)
29 (* Names : Lattice structure ntheorem 8 [Bon91] *)
31 (* Status : Unsatisfiable *)
33 (* Rating : 0.11 v3.4.0, 0.12 v3.3.0, 0.14 v3.1.0, 0.11 v2.7.0, 0.09 v2.6.0, 0.17 v2.5.0, 0.00 v2.4.0, 0.00 v2.2.1, 0.67 v2.2.0, 0.71 v2.1.0, 0.88 v2.0.0 *)
35 (* Syntax : Number of clauses : 14 ( 0 non-Horn; 14 unit; 2 RR) *)
37 (* Number of atoms : 14 ( 14 equality) *)
39 (* Maximal clause size : 1 ( 1 average) *)
41 (* Number of predicates : 1 ( 0 propositional; 2-2 arity) *)
43 (* Number of functors : 8 ( 4 constant; 0-2 arity) *)
45 (* Number of variables : 19 ( 1 singleton) *)
47 (* Maximal term depth : 5 ( 2 average) *)
51 (* -------------------------------------------------------------------------- *)
53 (* ----Include Alternative Wajsberg algebra axioms *)
55 (* Inclusion of: Axioms/LCL002-0.ax *)
57 (* -------------------------------------------------------------------------- *)
59 (* File : LCL002-0 : TPTP v3.7.0. Released v1.0.0. *)
61 (* Domain : Logic Calculi (Wajsberg Algebras) *)
63 (* Axioms : Alternative Wajsberg algebra axioms *)
65 (* Version : [AB90] (equality) axioms. *)
69 (* Refs : [FRT84] Font et al. (1984), Wajsberg Algebras *)
71 (* : [AB90] Anantharaman & Bonacina (1990), An Application of the *)
73 (* : [Bon91] Bonacina (1991), Problems in Lukasiewicz Logic *)
75 (* Source : [Bon91] *)
81 (* Syntax : Number of clauses : 8 ( 0 non-Horn; 8 unit; 0 RR) *)
83 (* Number of atoms : 8 ( 8 equality) *)
85 (* Maximal clause size : 1 ( 1 average) *)
87 (* Number of predicates : 1 ( 0 propositional; 2-2 arity) *)
89 (* Number of functors : 5 ( 2 constant; 0-2 arity) *)
91 (* Number of variables : 10 ( 1 singleton) *)
93 (* Maximal term depth : 5 ( 2 average) *)
95 (* Comments : To be used in conjunction with the LAT003 alternative *)
97 (* Wajsberg algebra definitions. *)
99 (* -------------------------------------------------------------------------- *)
101 (* -------------------------------------------------------------------------- *)
103 (* -------------------------------------------------------------------------- *)
105 (* ----Include some Alternative Wajsberg algebra definitions *)
107 (* include('Axioms/LCL002-1.ax'). *)
109 (* ----Definition that and_star is AC and xor is C *)
111 (* ----Definition of false in terms of true *)
113 (* ----Include the definition of implies in terms of xor and and_star *)
114 ntheorem prove_wajsberg_mv_4:
115 (∀Univ:Type.∀X:Univ.∀Y:Univ.∀Z:Univ.
117 ∀and_star:∀_:Univ.∀_:Univ.Univ.
120 ∀implies:∀_:Univ.∀_:Univ.Univ.
123 ∀xor:∀_:Univ.∀_:Univ.Univ.
124 ∀H0:∀X:Univ.∀Y:Univ.eq Univ (implies X Y) (xor truth (and_star X (xor truth Y))).
125 ∀H1:eq Univ (not truth) falsehood.
126 ∀H2:∀X:Univ.∀Y:Univ.eq Univ (and_star X Y) (and_star Y X).
127 ∀H3:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (and_star (and_star X Y) Z) (and_star X (and_star Y Z)).
128 ∀H4:∀X:Univ.∀Y:Univ.eq Univ (xor X Y) (xor Y X).
129 ∀H5:∀X:Univ.∀Y:Univ.eq Univ (and_star (xor (and_star (xor truth X) Y) truth) Y) (and_star (xor (and_star (xor truth Y) X) truth) X).
130 ∀H6:∀X:Univ.∀Y:Univ.eq Univ (xor X (xor truth Y)) (xor (xor X truth) Y).
131 ∀H7:∀X:Univ.eq Univ (and_star (xor truth X) X) falsehood.
132 ∀H8:∀X:Univ.eq Univ (and_star X falsehood) falsehood.
133 ∀H9:∀X:Univ.eq Univ (and_star X truth) X.
134 ∀H10:∀X:Univ.eq Univ (xor X X) falsehood.
135 ∀H11:∀X:Univ.eq Univ (xor X falsehood) X.
136 ∀H12:∀X:Univ.eq Univ (not X) (xor X truth).eq Univ (implies (implies (implies a b) (implies b a)) (implies b a)) truth)
163 nauto by H0,H1,H2,H3,H4,H5,H6,H7,H8,H9,H10,H11,H12 ##;
164 ntry (nassumption) ##;
167 (* -------------------------------------------------------------------------- *)