Help with Prover9 for weak propositional systems

Question

I am trying to get Prover9 to work, but apparently am not using exactly the correct commands. Can someone give me a hint, please? This is just a test case, but there are two rules, no disjunction or negation in the system. Here is my input file...

formulas(assumptions).

% Implication Axioms

P(rule(x,imp(x,y)) -> y)      # label(Im_1).   % x, x -> y  |-  y

P(rule(x,y) -> and(x,y))      # label(Cn_1).   % x, y  |-  x & y

P(imp(and(x,y),x))            # label(Cn_2).   % x & y -> x
P(imp(and(x,y),y))            # label(Cn_3).   % x & y -> y
P(imp(and(imp(x,y),imp(x,z)),imp(x,and(y,z))))  # label(Cn_4).   % (x -> y) & (x -> z) -> (x -> y & z)

end_of_list.

formulas(goals).

P(imp(and(x,y),and(y,x)))     # label(And_Commutativity).

end_of_list.

% Expected, something related to the following...

%  P(imp(and(x,y),y))                                                    Cn_3  x & y -> y                                      
%  P(imp(and(x,y),x))                                                    Cn_2  x & y -> x                                      
%  P(and(imp(and(x,y),y),imp(and(x,y),x)))                               Cn_1  (x & y -> y) & (x & y -> x)                     
%  P(and(imp(and(x,y),y),imp(and(x,y),x)) -> imp(and(x,y),and(y,x))))    Cn_4  (x & y -> y) & (x & y -> x) -> (x & y -> y & x) 
%  P(imp(and(x,y), and(y,x)))                                            Im_1  x & y -> y & x                                  

Answer 1

It is unclear to me why you wrote the implication arrow inside the predicate 'P'. Be that as it may, the main issue seems to me that the 'rule'-predicate occurs only as the antecedent of a conditional. For if you have, say, a conditional $p \rightarrow q$, you only know that $q$ is true if $p$ is true, but you do not know whether $p$ is actually true. Your first two lines are non-starters, so to speak.

Indeed, I did not see the point in the 'rule'-predicate at all. I have modified your first two lines such:

P(x) & P(imp(x,y)) -> P(y).
P(x) & P(y) -> P(and(x,y)).

I interpret the 'P'-predicate as meaning something like 'is provable'. Then, the first line says that if $x$ is provable, and $imp(x,y)$ is provable, then $y$ is provable either - which I take to be the result you wanted. Similarly, the second line says that if $x$ is provable and $y$ is provable, then $and(x,y)$ is provable.

Your other three assumption lines are fine. After these modifications, all your expected results could be proven (except the fourth, which had a syntax error, and which I rewrote to

P(and(imp(and(x,y),y),imp(and(x,y),x))) -> P(imp(and(x,y),and(y,x))).

I didn't cross-check whether "unexpected" results are indeed disprovable, but will leave this up to you.