% problem-set/logic.problems/morgan/morgan.five.ver1.clauses
% created : 07/15/86
% revised : 07/15/88

% description:
%
% Problem five sent by Charles Morgan of Victoria University:
% Can we deduce from these four axioms alone that       
% not(not(a)) implies a?

% 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 4
-P(i(x1,x2)) | -P(x1) | P(x2).

% axiom 3
P(i(i(n(x1),n(x2)),i(x2,x1))).

% negation of hypothesis  
-P(i(n(n(a)),a)).