Odintsov Proofs in Dogelog Player

Last updated at 2024-07-14Posted at 2024-07-09

We have retracted our simple λμ-calculus blog post until we have explored its model and proof theory more thoroughly. Some of the model theory has already been completed in a post on medium.com . We here report on a puzzle stone in proof theory.

One loose end concerns the Peirce's logic where we made a reference to a result by Segerberg 1968. Namely that over minimal logic the rule of Curry's Refutation (JE) is equivalent to the rule of Peirce's Law (JP). Can we show JE = JP with Prolog?

Motivating Example

Segerberg 1968 had in passing a short introduction to Hilbert Style calculi. He used modus ponens and these two axioms:

He then claimed that this here is derivable, whereby later in the paper he presented a derivation:

He also said its not easy to find such a proof
and that he was helped! Can Prolog help?

Combinatory Logic

To solve the problem we use ideas from combinatory logic. Combinators were introduced by Moses Schönfinkel in 1920 with the idea of eliminating variables from predicate logic. We use a typed version, basically adding a Curry-Howard isomorphism to it.

:- dynamic typeof/2.

/* modus ponens */
typeof((S*T), B) :-
   typeof(S, (A -> B)),
   typeof(T, A).
/* K axiom */
typeof(k, (A -> _ -> C)) :-
   unify_with_occurs_check(A,C).
/* S axiom */
typeof(s, ((A -> B -> C) -> (D -> F) -> (E -> G))) :-
   unify_with_occurs_check(A,D),
   unify_with_occurs_check(A,E),
   unify_with_occurs_check(B,F),
   unify_with_occurs_check(C,G).

To prevents cyclic types during pattern matching of the axioms we had to massage the axioms. The approach is to replace two occurrences of a variable .. V .. V .. by a new fresh variable .. V .. W ... and a unify_with_occurs_check/2 guard.

?- typeof((s*s*s), X).
false.

?- typeof((k*k*k), X).
X = (_A->_->_A).

The above shows what the typeof/2 predicate already can do. If a combinatory logic expression is given, the predicate calculates the principle type of it, if any such type exists. Ìf no such type exists, the predicate terminates with failure.

Proof Search

Instead of determining the type of a given expression, we want to go the other way around. Namely we want to give a type and ask a Prolog program what expression could give this type. To solve that inhabitation problem we have to study meta interpreters:

/* vanilla interpreter */
solve(true).
solve((A,B)) :- solve(A), solve(B).
solve(typeof(P, T)) :- 
   clause(typeof(P, T), B), solve(B).
solve(unify_with_occurs_check(A,B)) :-
   unify_with_occurs_check(A,B).

The above vanilla interpreter still correctly determines a principal type, but it will go astray for the inhabitation problem, because typeof/2 doesn't terminate anymore.

?- solve(typeof(k, X)).
X = (_A->_->_A).

?- solve(typeof(X, a->a)).
ERROR: Stack limit (1.0Gb) exceeded

What we can do here, is limit what solve/2 does, in that we give it a further parameter. In the literature one finds different approaches to limit solve/2, for example a depth parameter. We opt for a count down of the number of typeof/2 invocations:

/* vanilla interpreter with typeof/2 counting */
search(true, N, N).
search((A,B), N, M) :- search(A, N, H), search(B, H, M).
search(typeof(P, T), N, M) :- N>0, H is N-1,
   clause(typeof(P, T), B), search(B, H, M).
search(unify_with_occurs_check(A,B), N, N) :-
   unify_with_occurs_check(A,B).

Aarmed with such a meta-interpreter we can try different counts, increasingly from 1 to N. This will try expressions of increasing size, but also fast fail when some principal type doesn't work out. If we are lucky we can solve the inhabitation problem:

?- between(1,6,N), search(typeof(X, a->a), N, 0).
N = 5,
X = s*k*k

Peirce's Law

The expression is indeed the proof that is given in Segerberg 1968 paper. Unfortuantely that is the only time he uses Hilbert Style calculus. He later abandons this type of proof:

In particular his proofs get increasingly complex. He not only starts using semantic methods and juggles with set theory, the proof we are interested in that Peirce's Law equals Curry's Refutation, is only a byproduct of a more complex proof.

It turns out that we can stay with the combinatory logic approach, and derive the theorem as combinators. Lets begin with Peirce's Law and its companion Ex Falso Quodlibet. These are two axiom schemas P and E:

What we don't show here that we also added Schonfinkels I, B and C combinator, and combinators for disjunction introduction i1 and i2 and elimination []. This gives us a nice playground, and we can already derive a double negation elimination:

Since minimal logic with double negation elimination is classical logic, the derivation shows that classical logic proofs can be mapped to proofs with E and P. The converse is also true, since E and P are in fact also derivable from double negation elimination.

Odintsov Proofs

The previous two combinators E and P worked for the implicational fragment, but they give classical logic also for extended minimal logic which is minimal logic with disjunction. We now turn to two combinators Z and L that say something about disjunction:

First some words about the currious combinator Z, we picked it up from a paper by Odintsov 2004. It allows us to derive the so called Disjunctive Syllogism as follows, the derivation does not need L, extended minimal logic plus Z is sufficient:

Giving a more basic explanation to this reasoning:

cat_is_dead | cat_eats_food
~cat_eats_food
--------------------------------------
cat_is_dead

But we could also make Disjunctive Syllogism a first principle. Using combinatory logic we could then model Disjunctive Syllogism as a combinator, as it happens we would then find an expressions for Z using this combinator, showing inter definability.

Segerberg's Result

Without Z, the resoning doesn’t work, its not that a Schrödinger Cat emerges, but negation becomes too weak because of what Segerberg 1968 calls abnormal worlds. Since negation is defined as ~A = A => f, and abnormal worlds is where falsum f is true.

The above model finder works for Z and L, does it also work for E and P ? Segerberg 1968 showed JE = JP as a corollary of a more elaborate theorem. For the same case we can use our brute force combinatorial search to show inter definability.

First the axioms Z and L expressed in the axioms E and P:

Then the axioms E and P expressed in the axioms Z and L:

Conclusions

With the help of combinatorial logic, unify_with_occurs_check/2 and a meta-interpreter we can solve the type inhabitation problem brute force in Prolog. This method is powerful enough to assist us in a direct proof of Segerbergs 1968 result that JE = JP.