% % 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). set(para_from_small). clear(back_demod). set(hyper_resolution). set(auto_denials). set(restrict_denials). % ************************************************************************** % Clauses for Section 5 (algebra) (based on file clsn2.pdf dated 2008-29-06) % ************************************************************************** % % Note: Throughout we make use of identities and quasi-identities % given in Part I. Modulo identity (5.6) below, all identities and % quasi-identities are labelled as in Part I. % 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 % % Note: This definition is not used explicitly in Part II. % %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 % % Note: This definition is not used explicitly in Part II. % %-x = x => (x => 0) # label("(- def)"). % % Identities axiomatising Alg Mod* NFL_ew, the equivalent quasivariety % semantics of the deductive system NFL_ew. % % Note: By the remarks following Lemma 5.4 of Part II, Alg Mod* NFL_ew % is the class of all 3-potent, distributive classical FL_ew-algebras % satisfying the identity % ((x => (x => y)) ^ (~y => (~y => ~x))) => (x => y) = 1. % % Note: The identity expressing classicality and the identity % ((x => (x => y)) ^ (~y => (~y => ~x))) => (x => y) = 1 % are expressed in terms of the definition defining strong % negation in Nelson FL_ew-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 => (x => y)) ^ (~y => (~y => ~x))) => (x => y) = 1 # label("(5.6)"). % % 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 5.5) % formulas(goals). (x => (x => y)) ^ (~y => (~y => ~x)) = x => y # label("N"). end_of_list. % % Hints extracted from previously found proofs. % formulas(hints). (x => (x => y)) ^ (~ y => (~ y => ~ x)) = x => y. x v y = y v x. x * 1 = x. ~ x = x => 0. x => 0 = ~ x. ~ ~ x = x. ((x => (x => y)) ^ (~ y => (~ y => ~ x))) => (x => y) = 1. x => (y => x) = 1. x => (y => z) = y => (x => z). (x => y) ^ (x => z) = x => (y ^ z). (x * (x => y)) v y = y. (x => y) ^ (z => y) = (x v z) => y. x => ~ y = y => (x => 0). x => (y => 0) = y => ~ x. x => (((x => (x => y)) ^ (~ y => (~ y => ~ x))) => y) = 1. x = x v (y * (y => x)). x v (y * (y => x)) = x. (x => y) v (y * 1) = x => y. (x => y) v (z * (x => (z => y))) = x => y. x => ~ y = y => ~ x. x => y = ~ y => ~ x. ~ x => ~ y = y => x. (x => y) v y = x => y. x => y = y v (x => y). x v (y => x) = y => x. (x => y) v (x => (z => y)) = z => (x => y). x => (((x => (x => y)) ^ (~ y => (x => y))) => y) = 1. x => (((x => (x => y)) ^ (x => (~ y => y))) => y) = 1. x => ((x => ((x => y) ^ (~ y => y))) => y) = 1. x => ((x => ((x v ~ y) => y)) => y) = 1. (x => y) v ((x => ((x v ~ y) => y)) * 1) = x => y. (x => y) v (x => ((x v ~ y) => y)) = x => y. x => y = (x v ~ y) => (x => y). (x v ~ y) => (x => y) = x => y. (x => (x => y)) ^ (~ y => (x => y)) = x => y. end_of_list.