Dogelog Player is a Prolog system 100% written in Prolog itself that targets the JavaScript and the Python platform. On the JavaScript platform the Prolog system can directly run in the browser. There exists a DOM-API in the form of library(markup).
Related approaches were already pioneered by Tau-Prolog. We recently developed a sequent system proof search in Prolog for minimal logic, and used the library to display natural deduction proofs. We report about an extension to first order logic.
Drinker Paradox
The drinker paradox is a theorem of classical predicate logic that can be stated: There is someone in the pub such that, if he or she is drinking, then everyone in the pub is drinking. If we take the pub as the domain of discourse, and if we don't have existential quantifier only forall quantifier, we can write the theorem as:
¬ ∀x: ¬ (d(x) -> ∀y:d(y))
The paradox was popularised by the mathematical logician Raymond Smullyan, who called it the "drinking principle" in his book "What is the Name of this Book?". A deeper analysis of the theorem shows its dependency on a non-empty domain assumption. Further the theorem is not minimal logic valid, depends on further logical principles.
The paradox has made regular appearance as an example in automated theorem proving. The example can serve as a hardening of the universal generalization rule. This rule has a free variable side condition. Using the Prolog technology theorem prover leanSeq from Jens Otten, we find that sequent system inference rule (∀L) gets used two times:
?- prove((~ (![X]:(~ (d(X) => ![Y]:d(Y)))))).
iteration 1
iteration 2
true
Unfortunately Jens Ottens theorem prover doesn't show us a proof. It only ends with yes or no, or a third possibility that we need to abort it. We could change the situation and naively display a sequent system proof, but such a proof is hardly readable. We therefore aim at a new natural deduction style display.
Firstorder Backtracking
To archive a natural deduction style display we decided to extend our minimal logic sequent system proof search. This proof search uses backtracking so far, and we can therefore easily add new inference rules to it. If we extract a simple type lambda expression proof tree for every new inference rule, we are done.
Γ, x:A->f |- t:f
----------------------- (Raa)
Γ |- raa(λx:A->f.t):A
The newly added principle goes by different names such as Reductio Ad Absurdum or Proof by Contradiction. It states that to prove Γ |- A we can take the negation A->f of A and attempt to prove Γ, A->f |- f. The principle is quite powerful and allows for example the derivation of Peirce Law:
The extracted lambda expression has a new constant "raa" that is combinator for the axiom ((A->f)->f)->A polymorphic in formulas A. This constant is detected during proof rendering, and the Conclusion statement for λx:A->f.t is omitted, and instead a Reduction statement is shown.
We can further extend the calculus by two universal quantifier rules. Their implementation during proof search is similar to the the universal quantifier in leanSeq by Jens Otten. We use copy_term/2 and skolem functions but have the additional benefit of proof term extraction:
Γ |- t:A
-------------------- x ∉ Γ (∀R)
Γ |- (λx:U.t):∀x.A
Γ, x:∀w.A, y:A[w/z] |- t:B
---------------------------------------- (∀L)
Γ, x:∀w.A |- ((λy:A[w/z].t) (x z:U)):B
The constant U plays the role of the domain of discourse. The rules (∀R) and (∀L) do not have a subproof requirement for x:U and t:U. These assumptions are implicitly discharged since we assume that the domain is non-empty and that non-ground terms denote for all their possible instantiations.
The above shows some proof attempts in classical first order logics with the universal quantifier rules in place. The proof search terminates for the first two examples in short time. But the Drinker Paradox doesn't get solved in reasonable time, due to the search space explosion in backtracking.
Firstorder Non-Backtracking
To remove backtracking from the propositional proof search and from some of the first order proof search we deployed insights from Gerhard Gentzens paper “Untersuchungen über das logische Schließen” in 1934. In the propositional case and for the calculus LJ the (->L) and (->R) already act as passivator and activator. Only the (->L) rule doesn't terminate, since it repeats the formula A->B.
In the classical case the calculus LK doesn't need to repeat the formula A->B, and we can use a Reductio Ad Absurdum as a second passivator. Unlike (->R) which passivates an implication formula in the left hand side of the sequent, until it gets considered again by (->L), we arranged that (Raa) passivates an atom in the right hand side of the sequent for indefinite time:
LK Calculus:
Γ, x:A |- t:B, Δ
------------------ (Ax) ------------------------- (->R)
Γ, x:A |- x:A, Δ Γ |- (λx:A.t):A->B, Δ
Γ |- s:A, Δ Γ, y:B |- t:f, Δ
---------------------------------------- (->L)
Γ, x:A->B |- ((λy:B.t) (x s)):f, Δ
-------------------------- (Ax')
Γ, x:A |- (y x):f, y:A, Δ
Γ |- t:f, x:A, Δ
--------------------------- (Raa)
Γ |- raa(λx:A->f.t):A, Δ
In LK we can make (->R) greedy and not only (->L), so that for classical propositional logic, we don't need any iterative deepening anymore. The greedyness assures that the inference rule (Ax), (Ax') and (Raa) only acts on atomic formulas or the falsum f in case of (Ax). Sometimes proofs now turn out a little longer, but we can still prove Peirce Law with the same number of steps:
The resulting proof search is somewhat similar to Melvin Fittings leanTap revisited, only that we do not preprocess negation normal form, adhering to the leanSeq approach. We extract a lambda expression, to display a natural deduction style proof. After integrating the universal quantifier, it is now possible to automatically prove the Drinker Paradox:
There are still some optimizations on our wish list. The alternative identity rule (Ax') has currently a quadratic effort deploying two member/2 calls for the left sequent and the right sequent, doing this everytime before passivation via (Raa). It can be done with linear effort everytime a formula is passivated on the left sequent via (->R).
Conclusions
Gerhard Gentzens paper “Untersuchungen über das logische Schließen” in 1934 is a real treasure when it comes to theorem proving. In the classical case it highlights a number of optimizations, which we could realize in a Prolog technology prover, that despite the cut-elimination can extract and display natural deduction proofs for classical first order logic.
Example 52: Firstorder Backtracking
https://www.dogelog.ch/littab/doclet/docs/05_supplement/07_unicorn/example52/package.html
Example 54: Firstorder Non-Backtracking
https://www.dogelog.ch/littab/doclet/docs/05_supplement/07_unicorn/example54/package.html
Image generated with:
https://scribblediffusion.com/