% problem-set/logic.problems/morgan/morgan.three.ver1.clauses % created : 07/15/86 % revised : 07/15/88 % description: % % Problem three sent by Charles Morgan of Victoria University: % Can we deduce from these four axioms and the statement proven % by morgan_two.ver1, that a implies not(not(a)), this time with % both the negation of the hypothesis and the proven statement in % the set of support? % representaion: % % declare_predicate(1,P). % declare_function(2,i). % declare_function(1,n). % declare_constants([a,b,c]). % declare_variables([x1,x2,x3]). % % The axioms are as follows: % % 1. P(i(x,i(y,x))) % 2. P(i(i(x,i(y.z)),i(i(x,y),i(x,z)))) % 3. P(i(i(n(x),n(y)),i(y,x))) % 4. If P(i(x,y)) & P(x) then P(y) % % P means "is provable", i means "implies", and n means "not". % Thus Axiom 4 represents the inference rule of modus ponens. % axiom 1 P(i(x1,i(x2,x1))). % axiom 2 P(i(i(x1,i(x2,x3)),i(i(x1,x2),i(x1,x3)))). % axiom 3 P(i(i(n(x1),n(x2)),i(x2,x1))). % axiom 4 -P(i(x1,x2)) | -P(x1) | P(x2). % negation of hypothesis -P(i(a,n(n(a)))). % statement proven by morgan_two.ver1 P(i(n(n(x1)),x1)).