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...


% 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)



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


% 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.

  • $\begingroup$ 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. $\endgroup$ – Michael Lee Finney Oct 11 '15 at 14:24
  • $\begingroup$ 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. $\endgroup$ – user278201 Oct 11 '15 at 15:05
  • $\begingroup$ 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. $\endgroup$ – Michael Lee Finney Oct 11 '15 at 19:01

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.