%
% Prover9 commands
%
clear(auto).
op(400,infix,[^,v,"->","=>",*]).
op(200,prefix,[~,-]).
lex([0,1,*,^,=>,->,v,~,-]).
assign(order,kbo).
set(lex_order_vars).
set(paramodulation).
set(para_units_only).
clear(back_demod).
set(hyper_resolution).
set(auto_denials).
%set(restrict_denials).
% **************************************************************************
% Clauses for Section 4
% **************************************************************************
formulas(assumptions).
%
% Identities axiomatising lattices
%
(x v y) v z = x v (y v z) # label("(D1)").
(x ^ y) ^ z = x ^ (y ^ z) # label("(D2)").
x v y = y v x # label("(D3)").
x ^ y = y ^ x # label("(D4)").
x v (x ^ y) = x # label("(D5)").
x ^ (x v y) = x # label("(D6)").
%
% Identities and quasi-identities axiomatising BCK-algebras
%
(x => y) => ((y => z) => (x => z)) = 1 # label("(BCK1)").
1 => x = x # label("(BCK2)").
x => 1 = 1 # label("(BCK3)").
x => y != 1 | y => x != 1 | x = y # label("(BCK4)").
%
% Identities axiomatising partially ordered, commutative integral
% residuated monoids (pocrims)
%
% Note: These identities axiomatise pocrims when taken in
% conjunction with the identities and quasi-identities axiomatising
% BCK-algebras given above.
%
x * 1 = x # label("(M1)").
x * y = y * x # label("(M2)").
(x * y) * z = x * (y * z) # label("(M3)").
(x * y) => z = x => (y => z) # label("(P)").
%
% Identities axiomatising commutative, integral residuated lattices
%
% Note: These identities axiomatise commutative, integral residuated
% lattices when taken in conjunction with the identities and
% quasi-identities axiomatising pocrims given above.
%
% Note: This quasi-equational basis for commutative, integral
% residuated lattices axiomatises them as structures
% , 1> with a lattice reduct ,
% a pocrim reduct , 1>, such that (i) 1 is the greatest
% element with respect to the lattice partial ordering; and
% (ii) the lattice partial order and BCK-algebra partial orders
% coincide.
%
x ^ 1 = x # label("(D10)").
x ^ ((x => y) => y) = x # label("(3.7)").
(x ^ y) => y = 1 # label("(3.11)").
%
% Identities axiomatising FL_ew-algebras
%
% Note: These identities axiomatise FL_ew-algebras
% when taken in conjunction with the identities and
% quasi-identities axiomatising commutative, integral
% residuated lattices given above.
%
x v 0 = x # label("(D9)").
%
% Definitions mapping Nelson FL_ew-algebras to Nelson algebras
%
% Definition of -> (weak implication) in Nelson FL_ew-algebras
x -> y = x => (x => y) # label("(-> def)").
% Definition of ~ (strong negation) in Nelson FL_ew-algebras.
~x = x => 0 # label("(~ def)").
% Definition of - (weak negation) in Nelson FL_ew-algebras
-x = x => (x => 0) # label("(- def)").
%
% Identities axiomatising Nelson FL_ew-algebras.
%
% Note: Nelson FL_algebras are 3-potent, distributive classical
% FL_ew-algebras satisfying the Nelson identity (N).
%
% Note: The identities expressing classicality and the Nelson identity
% are expressed in terms of the definitions mapping Nelson FL_ew-algebras
% into Nelson algebras.
%
x => (x => (x => y)) = x => (x => y) # label("(E_2)"). % 3-potency
(x v y) ^ (x v z) = x v (y ^ z) # label("(D7)"). % Distributivity
(x ^ y) v (x ^ z) = x ^ (y v z) # label("(D8)").
~(~x) = x # label("(DN)"). % Classicality
(x -> y) ^ (~y -> ~x) = x => y # label("(N)"). % Nelson identity
%
% Identities which are known consequences of the theory of FL_ew-algebras
%
% Note: The following identities are known to hold for BCK-algebras, and
% hence hold for Nelson FL_ew-algebras.
%
(x => y) => ((z => x) => (z => y)) = 1 # label("(BCK1')").
x => ((x => y) => y) = 1 # label("(BCK5)").
x => x = 1 # label("(3.16)").
x => (y => x) = 1 # label("(3.17)").
x => (y => z) = y => (x => z) # label("(3.18)").
%
% Note: The following identities are known to hold for commutative,
% integral residuated lattices, and hence hold for Nelson FL_ew-algebras.
%
(x * y) v (x * z) = x * (y v z) # label("(4.1)").
(x => y) ^ (x => z) = x => (y ^ z) # label("(4.2)").
(x * (x => y)) v y = y # label("(4.3)").
(x => y) ^ (z => y) = (x v z) => y # label("(4.4)").
((x => y) * z) => (x => (y * z)) = 1 # label("(4.5)").
end_of_list.
%
% Current problem (Lemma 4.3)
%
formulas(assumptions).
% multi-part lemma negated by hand
(A => B) ^ B != B % (3.13), Lemma 4.3 (1)
| (A v B) => B != A => B % (4.6), Lemma 4.3 (2)
| A -> (B => C) != B => (A -> C) % (4.7), Lemma 4.3 (3)
| A ^ (~A => B) != A % (4.8), Lemma 4.3 (4)
# answer("(Lemma 4.3, 4 parts)").
end_of_list.
%
% Hints extracted from previously found proofs.
%
formulas(hints).
(x => y) ^ y = y # label("(3.13)"). % Lemma 4.3 (1)
(x v y) => y = x => y # label("(4.6)"). % Lemma 4.3 (2)
x -> (y => z) = y => (x -> z) # label("(4.7)"). % Lemma 4.3 (3)
x ^ (~x => y) = x # label("(4.8)"). % Lemma 4.3 (4)
x v y = y v x.
x ^ y = y ^ x.
1 => x = x.
x ^ 1 = x.
x ^ ((x => y) => y) = x.
x -> y = x => (x => y).
x => (x => y) = x -> y.
~ x = x => 0.
x => 0 = ~ x.
~ ~ x = x.
x => x = 1.
x => (y => x) = 1.
x => (y => z) = y => (x => z).
(x => y) ^ (z => y) = (x v z) => y.
x = 1 ^ x.
1 ^ x = x.
~ x => 0 = x.
x => (y -> z) = y => (x => (y => z)).
x => (y => (x => z)) = y => (x -> z).
x => ~ y = y => (x => 0).
x => (y => 0) = y => ~ x.
1 ^ (x => y) = (y v x) => y.
(x v y) => x = 1 ^ (y => x).
x => y = ~ y => ~ x.
~ x => ~ y = y => x.
~ x => y = ~ y => x.
x => (~ x => y) = 1.
x ^ (1 => (~ x => y)) = x.
x ^ (~ x => y) = x.
x ^ (y => x) = x.
x = (y => x) ^ x.
(x => y) ^ y = y.
(x v y) => x = y => x.
(x v y) => y = x => y.
x => (x => (y => z)) = y => (x -> z).
x => (y -> z) = y -> (x => z).
x -> (y => z) = y => (x -> z).
end_of_list.