# Help with Prover9 for weak propositional systems

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


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.

• Thank you! That was the hint I needed. The -> was inside P simply because that was one of the many variations that I tried. The point of "rule" was to model the |- turnstile. I also tried = as well ->. I did not think to model the commas using & and use -> directly to model |-. I was trying to avoid the classical -p v q which is not valid in any of the logics I am examining. I did look at every Prover9 example and every web page returned by a Google search on Prover9. P.S. I upvoted your answer, but it won't take until I get more reputation points. – Michael Lee Finney Oct 11 '15 at 14:24
• A side note on "->": Prover9 does transform "p -> q" to "~p | q", but as far as I can see, this will not import the classical paradoxes into your logic (for example, if you will introduce negation, ex falso quodlibet will not automatically hold, since "P(x) & P(neg(x))" is something different, of course, from "P(x) & ~P(x)"). Only if your logic is substructural (for example, non-monotonic), you will need a more complicated construction. – user278201 Oct 11 '15 at 15:05
• The logics of interest are sub-structural, but they are all Hilbert. Given the pattern used so far (and it appears to be working when extended), I am probably ok except for meta-rules. I think that I can avoid those for the most part, so I should be good. I just need to learn to translate Prover9 proofs into more normal Hilbert style proofs. That should be doable. Thanks again. – Michael Lee Finney Oct 11 '15 at 19:01