(N. Megill 14-Dec-03)

A system with modus ponens as the only rule is described in G. Kalmbach,
_Orthomodular Lattices_ (1983), pp. 236ff.

Kalmbach's system has 15 axioms, A1-A15, plus one rule of inference, R1
(modus ponens).  It has primitive connectives v, ^, ~, and ->.  The use
of multiple primitive connectives allows it to be expressed more
compactly.  I don't think that her system is complete.  If I am right,
the mistake was that she proved the completeness of a system without ->,
then she introduced the -> connective after the fact without adding
enough axioms for it.  For example, I don't believe P -> P can be proved
in her system.  (Someday I'll try to show this rigorously.)  Anyway I
added an extra axiom, A16, that I believe is necessary.  Also, I have
proved that A1, A11, and A15 are redundant (i.e. can be derived from the
others).

With the addition of my A16, here is Kalmbach's system:

R1.  Rule of inference:  From P and P -> Q, infer Q
A1.  P <-> P
A2.  ~(P <-> Q) v (~(Q <-> R) v (P <-> R))
A3.  ~(P <-> Q) v (~P <-> ~Q)
A4.  ~(P <-> Q) v ((P ^ R) <-> (Q ^ R))
A5.  (P ^ Q) <-> (Q ^ P)
A6.  (P ^ (Q ^ R)) <-> ((P ^ Q) ^ R)
A7.  (P ^ (P v Q)) <-> P
A8.  (~P ^ P) <-> ((~P ^ P) ^ Q)
A9.  P <-> ~~P
A10.  ~(P v Q) <-> (~P ^ ~Q)
A11.  (P v (~P ^ (P v Q))) <-> (P v Q)
A12.  (P <-> Q) <-> (Q <-> P)
A13.  ~(P <-> Q) v (~P v Q)
A14.  (~P v Q) -> (P -> (P -> Q))
A15.  ~(P -> Q) v (~P v Q)
A16.  (P -> Q) <-> (((~P ^ Q) v (~P ^ ~Q)) v (P ^ (~P v Q)))

where P <-> Q is defined as (P ^ Q) v (~P ^ ~Q).

To obtain axioms with only ~ and ->, we can replace P v Q with ~P -> (~P
-> Q) and P ^ Q with ~(P -> (P -> ~Q)).  When this is done, we end up
with the system below with only the connectives ~ and ->.  While they
are hardly manageable in this form, I show them below to dramatize how
far there is to go to make them "elegant".  As a practical matter one
would of course use the system above.  But if we only want to have just
the connectives ~ and -> then the system below is the best that we have
so far.  (Some double negatives can probably be deleted, but where we
can do that without upsetting completeness is far from obvious:  for
example, removing the double negative in A9 above would render the
system incomplete.)

QR1.  Rule of inference:  From P and P -> Q, infer Q

QA1.  ~~(P -> (P -> ~P)) -> (~~(P -> (P -> ~P)) -> ~(~P -> (~P -> ~~P)))

QA2.  ~~(~~(P -> (P -> ~Q)) -> (~~(P -> (P -> ~Q)) -> ~(~P -> (~P ->
~~Q)))) -> (~~(~~(P -> (P -> ~Q)) -> (~~(P -> (P -> ~Q)) -> ~(~P -> (~P
-> ~~Q)))) -> (~~(~~(Q -> (Q -> ~R)) -> (~~(Q -> (Q -> ~R)) -> ~(~Q ->
(~Q -> ~~R)))) -> (~~(~~(Q -> (Q -> ~R)) -> (~~(Q -> (Q -> ~R)) -> ~(~Q
-> (~Q -> ~~R)))) -> (~~(P -> (P -> ~R)) -> (~~(P -> (P -> ~R)) -> ~(~P
-> (~P -> ~~R)))))))

QA3.  ~~(~~(P -> (P -> ~Q)) -> (~~(P -> (P -> ~Q)) -> ~(~P -> (~P ->
~~Q)))) -> (~~(~~(P -> (P -> ~Q)) -> (~~(P -> (P -> ~Q)) -> ~(~P -> (~P
-> ~~Q)))) -> (~~(~P -> (~P -> ~~Q)) -> (~~(~P -> (~P -> ~~Q)) -> ~(~~P
-> (~~P -> ~~~Q)))))

QA4.  ~~(~~(P -> (P -> ~Q)) -> (~~(P -> (P -> ~Q)) -> ~(~P -> (~P ->
~~Q)))) -> (~~(~~(P -> (P -> ~Q)) -> (~~(P -> (P -> ~Q)) -> ~(~P -> (~P
-> ~~Q)))) -> (~~(~(P -> (P -> ~R)) -> (~(P -> (P -> ~R)) -> ~~(Q -> (Q
-> ~R)))) -> (~~(~(P -> (P -> ~R)) -> (~(P -> (P -> ~R)) -> ~~(Q -> (Q
-> ~R)))) -> ~(~~(P -> (P -> ~R)) -> (~~(P -> (P -> ~R)) -> ~~~(Q -> (Q
-> ~R)))))))

QA5.  ~~(~(P -> (P -> ~Q)) -> (~(P -> (P -> ~Q)) -> ~~(Q -> (Q -> ~P))))
-> (~~(~(P -> (P -> ~Q)) -> (~(P -> (P -> ~Q)) -> ~~(Q -> (Q -> ~P))))
-> ~(~~(P -> (P -> ~Q)) -> (~~(P -> (P -> ~Q)) -> ~~~(Q -> (Q -> ~P)))))

QA6.  ~~(~(P -> (P -> ~~(Q -> (Q -> ~R)))) -> (~(P -> (P -> ~~(Q -> (Q ->
~R)))) -> ~~(~(P -> (P -> ~Q)) -> (~(P -> (P -> ~Q)) -> ~R)))) ->
(~~(~(P -> (P -> ~~(Q -> (Q -> ~R)))) -> (~(P -> (P -> ~~(Q -> (Q ->
~R)))) -> ~~(~(P -> (P -> ~Q)) -> (~(P -> (P -> ~Q)) -> ~R)))) -> ~(~~(P
-> (P -> ~~(Q -> (Q -> ~R)))) -> (~~(P -> (P -> ~~(Q -> (Q -> ~R)))) ->
~~~(~(P -> (P -> ~Q)) -> (~(P -> (P -> ~Q)) -> ~R)))))

QA7.  ~~(~(P -> (P -> ~(~P -> (~P -> Q)))) -> (~(P -> (P -> ~(~P -> (~P
-> Q)))) -> ~P)) -> (~~(~(P -> (P -> ~(~P -> (~P -> Q)))) -> (~(P -> (P
-> ~(~P -> (~P -> Q)))) -> ~P)) -> ~(~~(P -> (P -> ~(~P -> (~P -> Q))))
-> (~~(P -> (P -> ~(~P -> (~P -> Q)))) -> ~~P)))

QA8.  ~~(~(~P -> (~P -> ~P)) -> (~(~P -> (~P -> ~P)) -> ~~(~(~P -> (~P ->
~P)) -> (~(~P -> (~P -> ~P)) -> ~Q)))) -> (~~(~(~P -> (~P -> ~P)) ->
(~(~P -> (~P -> ~P)) -> ~~(~(~P -> (~P -> ~P)) -> (~(~P -> (~P -> ~P))
-> ~Q)))) -> ~(~~(~P -> (~P -> ~P)) -> (~~(~P -> (~P -> ~P)) -> ~~~(~(~P
-> (~P -> ~P)) -> (~(~P -> (~P -> ~P)) -> ~Q)))))

QA9.  ~~(P -> (P -> ~~~P)) -> (~~(P -> (P -> ~~~P)) -> ~(~P -> (~P ->
~~~~P)))

QA10.  ~~(~(~P -> (~P -> Q)) -> (~(~P -> (~P -> Q)) -> ~~(~P -> (~P ->
~~Q)))) -> (~~(~(~P -> (~P -> Q)) -> (~(~P -> (~P -> Q)) -> ~~(~P -> (~P
-> ~~Q)))) -> ~(~~(~P -> (~P -> Q)) -> (~~(~P -> (~P -> Q)) -> ~~~(~P ->
(~P -> ~~Q)))))

QA11.  ~~((~P -> (~P -> ~(~P -> (~P -> ~(~P -> (~P -> Q)))))) -> ((~P ->
(~P -> ~(~P -> (~P -> ~(~P -> (~P -> Q)))))) -> ~(~P -> (~P -> Q)))) ->
(~~((~P -> (~P -> ~(~P -> (~P -> ~(~P -> (~P -> Q)))))) -> ((~P -> (~P
-> ~(~P -> (~P -> ~(~P -> (~P -> Q)))))) -> ~(~P -> (~P -> Q)))) ->
~(~(~P -> (~P -> ~(~P -> (~P -> ~(~P -> (~P -> Q)))))) -> (~(~P -> (~P
-> ~(~P -> (~P -> ~(~P -> (~P -> Q)))))) -> ~~(~P -> (~P -> Q)))))

QA12.  ~~((~~(P -> (P -> ~Q)) -> (~~(P -> (P -> ~Q)) -> ~(~P -> (~P ->
~~Q)))) -> ((~~(P -> (P -> ~Q)) -> (~~(P -> (P -> ~Q)) -> ~(~P -> (~P ->
~~Q)))) -> ~(~~(Q -> (Q -> ~P)) -> (~~(Q -> (Q -> ~P)) -> ~(~Q -> (~Q ->
~~P)))))) -> (~~((~~(P -> (P -> ~Q)) -> (~~(P -> (P -> ~Q)) -> ~(~P ->
(~P -> ~~Q)))) -> ((~~(P -> (P -> ~Q)) -> (~~(P -> (P -> ~Q)) -> ~(~P ->
(~P -> ~~Q)))) -> ~(~~(Q -> (Q -> ~P)) -> (~~(Q -> (Q -> ~P)) -> ~(~Q ->
(~Q -> ~~P)))))) -> ~(~(~~(P -> (P -> ~Q)) -> (~~(P -> (P -> ~Q)) ->
~(~P -> (~P -> ~~Q)))) -> (~(~~(P -> (P -> ~Q)) -> (~~(P -> (P -> ~Q))
-> ~(~P -> (~P -> ~~Q)))) -> ~~(~~(Q -> (Q -> ~P)) -> (~~(Q -> (Q ->
~P)) -> ~(~Q -> (~Q -> ~~P)))))))

QA13.  ~~(~~(P -> (P -> ~Q)) -> (~~(P -> (P -> ~Q)) -> ~(~P -> (~P ->
~~Q)))) -> (~~(~~(P -> (P -> ~Q)) -> (~~(P -> (P -> ~Q)) -> ~(~P -> (~P
-> ~~Q)))) -> (~~P -> (~~P -> Q)))

QA14.  (~~P -> (~~P -> Q)) -> (P -> (P -> Q))

QA15.  ~~(P -> Q) -> (~~(P -> Q) -> (~~P -> (~~P -> Q)))

QA16.  ~~((P -> Q) -> ((P -> Q) -> ~(~(~~(~P -> (~P -> ~Q)) -> (~~(~P ->
(~P -> ~Q)) -> ~(~P -> (~P -> ~~Q)))) -> (~(~~ (~P -> (~P -> ~Q)) ->
(~~(~P -> (~P -> ~Q)) -> ~(~P -> (~P -> ~~Q)))) -> ~(P -> (P -> ~(~~P ->
(~~P -> Q)))))))) -> (~~((P -> Q) -> ((P -> Q) -> ~(~(~~(~P -> (~P ->
~Q)) -> (~~(~P -> (~P -> ~Q)) -> ~(~P -> (~P -> ~~Q)))) -> (~(~~(~P ->
(~P -> ~Q)) -> (~~(~P -> (~P -> ~Q)) -> ~(~P -> (~P -> ~~Q)))) -> ~(P ->
(P -> ~(~~P -> (~~P -> Q)))))))) -> ~(~(P -> Q) -> (~(P -> Q) -> ~
~(~(~~(~P -> (~P -> ~Q)) -> (~~(~P -> (~P -> ~Q)) -> ~(~P -> (~P ->
~~Q)))) -> (~(~~(~P -> (~P -> ~Q)) -> (~~(~P -> (~P -> ~Q)) -> ~(~P ->
(~P -> ~~Q)))) -> ~(P -> (P -> ~(~~P -> (~~P -> Q)))))))))


Here is a list of some random theorems of the above logic.  They might
interesting to look at in a search for a shorter axiomatization.

Notes:

1. All 1-variable theorems as the same as for classical propositional
calculus.

2. There is a decision procedure to verify all 2-variable theorems (I
have a program to do this, and also to iteratively list all for a given
number of connectives).

3. I have formal proofs of 178 theorems in this system (contact me if
you want them).


P -> P
P -> ~~P
~~P -> P
P -> (Q -> Q)
P -> (P -> (Q -> P))
P -> (Q -> (Q -> P))
~P -> (P -> (P -> Q))
~P -> (P -> (~P -> Q))
P -> ((P -> Q) -> P)
(P -> Q) -> (P -> (P -> Q))
~(P -> Q) -> ((P -> Q) -> P)
P -> (P -> ((Q -> ~P) -> ~Q))
P -> (P -> (Q -> ~(Q -> ~P)))
~(P -> ~Q) -> (P -> (P -> Q))
P -> ((P -> Q) -> ( ~Q ->  ~P))
(P -> Q) -> (P -> ( ~Q ->  ~P))
( ~Q ->  ~P) -> (P -> (P -> Q))
(P -> ( ~Q ->  ~P)) -> (P -> Q)
(P -> ( ~Q ->  ~P)) -> (P -> Q)
(P -> Q) -> ((P -> Q) -> (~Q -> ~P))
(P -> (P -> (P -> Q))) -> (P -> (P -> Q))
(P -> Q) -> ((P -> Q) -> ((Q -> P) -> ((Q -> P) ->
      ((R -> (R -> P)) -> (R -> (R -> Q))))))
(P -> Q) -> ((P -> Q) -> ((Q -> P) -> ((Q -> P) ->
      ((Q -> R) -> ((Q -> R) -> ((R -> Q) -> ((R -> Q) -> (P -> R))))))))

Other results:

Define:
P v Q  =def=  ~P -> (~P -> Q)
P ^ Q  =def=  ~(~P v ~Q)
Then:
All OML =1 laws hold; e.g. x v x' = 1 means P v ~P holds

If P -> (Q -> P) and Q -> (R -> Q), then {P,Q,R} is distributive triple
e.g. (P ^ (Q v R)) -> ((P ^ Q) v (P ^ R)),
     ((P ^ Q) v (P ^ R)) -> (P ^ (Q v R)),
     (Q ^ (P v R)) -> ((Q ^ P) v (Q ^ R)),
     ((Q ^ P) v (Q ^ R)) -> (Q ^ (P v R))