% % 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. % % Previous results % formulas(assumptions). % Lemma 4.3 (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) end_of_list. % % Current problem (Lemma 4.4) % formulas(goals). x -> ((y v x) -> z) = x -> z # label("(4.9)"). % Lemma 4.4 (1) x -> (~x v y) = x -> y # label("(4.10)"). % Lemma 4.4 (2) end_of_list. % % Hints extracted from previously found proofs. % formulas(hints). x -> ((y v x) -> z) = x -> z # label("(4.9)"). % Lemma 4.4 (1) x -> (~x v y) = x -> y # label("(4.10)"). % Lemma 4.4 (2) x v y = y v x. x ^ y = y ^ x. x v (x ^ y) = x. 1 => x = x. x * y = y * x. (x * y) => z = x => (y => z). x ^ ((x => y) => y) = x. x -> y = x => (x => y). x => (x => y) = x -> y. ~ x = x => 0. x => 0 = ~ x. x => (x => (x => y)) = x => (x => y). ~ ~ x = x. (x => y) => ((z => x) => (z => y)) = 1. x => (y => z) = y => (x => z). (x => y) ^ (x => z) = x => (y ^ z). (x => y) ^ (z => y) = (x v z) => y. ((x => y) * z) => (x => (y * z)) = 1. (x => y) ^ y = y. (x v y) => y = x => y. x -> (y => z) = y => (x -> z). x = (x ^ y) v x. (x ^ y) v x = x. ~ (x * y) = x => (y => 0). x => (y => 0) = ~ (x * y). x => (x -> y) = x => (x => y). (x => y) => (z => ((z => x) => y)) = 1. (x -> y) ^ (x => z) = x => ((x => y) ^ z). x => ((x => y) ^ z) = (x -> y) ^ (x => z). ~ x ^ (y => 0) = (x v y) => 0. (x * (y => z)) => (y => (z * x)) = 1. x = x ^ (y => x). x ^ (y => x) = x. x -> (y -> z) = y => (x -> (y => z)). x => (y -> (x => z)) = y -> (x -> z). x v (y => x) = y => x. x => ~ y = ~ (x * y). ~ (x * y) = x => ~ y. ~ (x => ~ y) = x * y. ~ (x => ~ y) = (x v ~ y) * y. (x v ~ y) * y = ~ (x => ~ y). x => (x -> y) = x -> y. x => (y -> z) = y => (x => (y -> z)). x => (y => (x -> z)) = y => (x -> z). (x -> y) ^ (z => (x -> y)) = (x v z) => (x -> y). ~ x ^ ~ y = (x v y) => 0. (x v y) => 0 = ~ x ^ ~ y. ~ x ^ ~ y = ~ (x v y). x ^ ~ y = ~ (~ x v y). ~ (~ x v y) = x ^ ~ y. ~ (x v ~ y) = y ^ ~ x. ~ (x v (y => ~ z)) = (y * z) ^ ~ x. (x v ~ y) * y = x * y. x * y = y * (x v ~ y). x * (y v ~ x) = y * x. 1 = x => ((y => z) => ((x => y) => z)). x => ((y => z) => ((x => y) => z)) = 1. 1 = x => ((y * (x => z)) => (z * y)). x => ((y * (x => z)) => (z * y)) = 1. x => (x => (y -> z)) = y -> (x -> z). x => (((x => y) => z) => ((x -> y) => z)) = 1. x => (y => ((x => z) => (z * y))) = 1. x -> (y -> z) = y -> (x -> z). 1 = x -> ((x => y) => (y * x)). x -> ((x => y) => (y * x)) = 1. x -> ((x => y) => (x * y)) = 1. 1 = (x => y) => (x -> (x * y)). (x => y) => (x -> (x * y)) = 1. ~ (x => ~ y) = (x * y) ^ ~ ~ y. (x * y) ^ ~ ~ y = ~ (x => ~ y). (x * y) ^ ~ ~ y = x * y. (x * y) ^ y = x * y. x => (y ^ (x => z)) = (x -> z) ^ (x => y). x => ((x -> y) => (((x => y) => z) => z)) = 1. x => ((x => y) ^ (x => z)) = (x -> z) ^ (x -> y). x => ((x -> y) => (1 => (x -> (x * y)))) = 1. x => ((x -> y) => (x -> (x * y))) = 1. 1 = (x -> y) => (x -> (x * y)). (x -> y) => (x -> (x * y)) = 1. (x -> y) ^ (1 => (x -> (x * y))) = x -> y. (x -> y) ^ (x -> (x * y)) = x -> y. x => (x => (y ^ z)) = (x -> z) ^ (x -> y). (x -> y) ^ (x -> z) = x -> (z ^ y). x -> ((x * y) ^ y) = x -> y. x -> (x * y) = x -> y. x -> (y * x) = x -> (y v ~ x). x -> (y v ~ x) = x -> (y * x). x -> (y v ~ x) = x -> (x * y). x -> (y v ~ x) = x -> y. x -> (~ x v y) = x -> y. x -> y = (x v z) => (x -> y). (x v y) => (x -> z) = x -> z. (x v y) => (x -> z) = (x v y) -> (x -> z). (x v y) -> (x -> z) = (x v y) => (x -> z). (x v y) -> (x -> z) = x -> z. (x v y) -> (y -> z) = y -> z. x -> y = x -> ((z v x) -> y). x -> ((y v x) -> z) = x -> z. end_of_list.