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

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

A1.  ~~(P -> (P -> ~P)) -> (~~(P -> (P -> ~P)) -> ~(~P -> (~P -> ~~P)))

A2.  ~~(~~(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)))))))

A3.  ~~(~~(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)))))

A4.  ~~(~~(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)))))))

A5.  ~~(~(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)))))

A6.  ~~(~(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)))))

A7.  ~~(~(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)))

A8.  ~~(~(~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)))))

A9.  ~~(P -> (P -> ~~~P)) -> (~~(P -> (P -> ~~~P)) -> ~(~P -> (~P ->
~~~~P)))

A10.  ~~(~(~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)))))

A11.  ~~((~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)))))

A12.  ~~((~~(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)))))))

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

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

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

A16.  ~~((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))