Rule of Constancy

Here we take Johnson's 1892 equational axiom system for propositional logic, as related in Meredith and Prior's 1967 paper Equational Logic, and write it in Eqthy:

axiom (#conj-comm)   conj(X, Y) = conj(Y, X)
axiom (#conj-assoc)  conj(X, conj(Y, Z)) = conj(conj(X, Y), Z)
axiom (#conj-idem)   conj(X, X) = X
axiom (#neg-invol)   not(not(X)) = X
axiom (#axiom5)      not(X) = conj(not(conj(X, Y)), not(conj(X, not(Y))))

I wish I had a better name than "axiom5" for that last axiom, but I don't know if it originally came with one.

Anyway, with these we can prove the "Rule of Constancy". But first, let's introduce a couple of lemmas to make the proof less tiresome.

theorem (#conj-rot)
    conj(A, conj(B, C)) = conj(B, conj(A, C))
proof
    A = A
    conj(A, conj(B, C)) = conj(A, conj(B, C))     [by substitution of conj(A, conj(B, C)) into A]
    conj(A, conj(B, C)) = conj(conj(A, B), C)
    conj(A, conj(B, C)) = conj(conj(B, A), C)
    conj(A, conj(B, C)) = conj(B, conj(A, C))
qed

theorem (#conj-perm-dbca)
    conj(A, conj(B, conj(C, D))) = conj(D, conj(B, conj(C, A)))
proof
    A = A
    conj(A, conj(B, conj(C, D))) = conj(A, conj(B, conj(C, D)))     [by substitution of conj(A, conj(B, conj(C, D))) into A]
    conj(A, conj(B, conj(C, D))) = conj(A, conj(B, conj(D, C)))
    conj(A, conj(B, conj(C, D))) = conj(A, conj(D, conj(B, C)))
    conj(A, conj(B, conj(C, D))) = conj(D, conj(A, conj(B, C)))
    conj(A, conj(B, conj(C, D))) = conj(D, conj(B, conj(A, C)))
    conj(A, conj(B, conj(C, D))) = conj(D, conj(B, conj(C, A)))
qed

OK, now the theorem.

theorem (#rule-of-constancy)
    conj(A, not(A)) = conj(C, not(C))
proof
    A = A
    conj(A, not(A)) = conj(A, not(A))     [by substitution of conj(A, not(A)) into A]
    conj(A, not(A)) = conj(not(not(A)), not(A))
    conj(A, not(A)) = conj(
                        not(not(A)),
                        conj(not(conj(A, C)), not(conj(A, not(C))))
                      ) [by #axiom5 with X=A, Y=C]
    conj(A, not(A)) = conj(
                        conj(not(conj(not(A), C)), not(conj(not(A), not(C)))),
                        conj(not(conj(A, C)), not(conj(A, not(C))))
                      ) [by #axiom5 with X=A, Y=C]

    conj(A, not(A)) = conj(
                        conj(not(conj(not(A), C)), not(conj(not(A), not(C)))),
                        conj(not(conj(A, C)), not(conj(not(C), A)))
                      ) [by #conj-comm]
    conj(A, not(A)) = conj(
                        conj(not(conj(not(A), C)), not(conj(not(A), not(C)))),
                        conj(not(conj(C, A)), not(conj(not(C), A)))
                      ) [by #conj-comm]
    conj(A, not(A)) = conj(
                        conj(not(conj(not(A), C)), not(conj(not(C), not(A)))),
                        conj(not(conj(C, A)), not(conj(not(C), A)))
                      ) [by #conj-comm]
    conj(A, not(A)) = conj(
                        conj(not(conj(C, not(A))), not(conj(not(C), not(A)))),
                        conj(not(conj(C, A)), not(conj(not(C), A)))
                      ) [by #conj-comm]

    conj(A, not(A)) = conj(
                        not(conj(C, not(A))),
                        conj(
                            not(conj(not(C), not(A))),
                            conj(
                                not(conj(C, A)),
                                not(conj(not(C), A))
                            )
                        )
                    )

    conj(A, not(A)) = conj(
                        not(conj(not(C), A)),
                        conj(
                            not(conj(not(C), not(A))),
                            conj(
                                not(conj(C, A)),
                                not(conj(C, not(A)))
                            )
                        )
                    ) [by #conj-perm-dbca]

    conj(A, not(A)) = conj(
                        conj(
                            not(conj(not(C), A)),
                            not(conj(not(C), not(A)))
                        ),
                        conj(
                            not(conj(C, A)),
                            not(conj(C, not(A)))
                        )
                    ) [by #conj-assoc]

    conj(A, not(A)) = conj(
                        not(not(C)),
                        conj(not(conj(C, A)), not(conj(C, not(A))))
                      ) [by #axiom5 with X=C, Y=A]

    conj(A, not(A)) = conj(not(not(C)), not(C)) [by #axiom5 with X=C, Y=A]

    conj(A, not(A)) = conj(C, not(C))
qed

Now a question: Why did Johnson feel the need to do this? To show that conj(A, not(A)) is invariant, no matter one's choice of A. And thus, it's a constant, and we can call this constant "Falsism".

But is this whole rigamarole necessary? Didn't Johnson allow substitution as a rule? Yes, but uniform substition won't get us there: if you substitute C for A you just get conj(C, not(C)) = conj(C, not(C)), which doesn't tell you anything. The application of axiom5 really does pull an arbitrary entity out of nowhere, of the form conj(C, not(C)), which gets folded, spindled, and mutilated, and shown to be equal to conj(A, not(A)).

It does still feel a bit like the Rule of Constancy is simply latent in axiom5 - we can say the LHS of axiom5 is equal to its RHS exactly because the extra entity pulled out of nowhere doesn't change anything.

It would overall be more satisfying if the justification for axiom5 looking the way it does, was more apparent.