# Proof checkers

2020-01-02, updated 2020-01-05 next - previous

I am used to check with different programs the proofs that I provide in my papers. In this post, I check the proofs given in this blog.

## 1 Descartes’s Argument

In this post, the first argument that Descartes gave in his
*Meditations* to prove the existence of God is expressed in
first-order logic by sequent (11):

To check the validity of 11, copy the latex code below (where
predicates *B* and *E* stand for respectively relations \( > \) and \(
= \))

y Byd) , Ecd , y(Rcy x Sxy ) , Rcd , x y(Sxy (Bxy Exy)) |= Scd x(Sxd Exd)

and paste it into the Tree Proof Generator.

Nevertheless, this nice prover written by Wolfgang Schwartz, is a
prover for *classical* first-order logic and therefore it does not
make any difference between formulas that are intuitionistically valid
and formulas that are valid in classical logic only. To get an
automated check that (11) is valid in intuitionnistic logic, it is
necessary to use an intuitionistic prover for intuitionistic
first-order logic, for example with imogen written by Sean McLaughlin:

```
imogen fol prove -i "(forall Y.(~b(Y,d)) & ~e(c,d) & forall Y.(r(c,Y) -> exists X.(s(X,Y))) & r(c,d) & forall X.forall Y.(s(X,Y) -> (b(X,Y) | e(X,Y)))) -> (~s(c,d) & exists X.(s(X,d) & e(X,d)))"
Warning: extending by default sort: d ι
Warning: extending by default sort: c ι
Provable.
```

or with ileantap_swi.pl written by Jens Otten:

?- prove((all Y:(~b(Y,d)), ~e(c,d), all Y:(r(c,Y) => ex X:(s(X,Y))) , r(c,d), all X:all Y:(s(X,Y) => (b(X,Y) ; e(X,Y)))) => (~s(c,d) , ex X:(s(X,d) , e(X,d)))). 1 2 3 4 5 6 7 8 0.00285059500000001131 2 3 4 5 6 7 8 % 4,926 inferences, 0.001 CPU in 0.001 seconds (100% CPU, 4321652 Lips) true

Last, here is Descartes’s argument given in natural deduction in
Fitch style that corresponds to the proof in Gentzen style given at the end of this
subsection (in the proof below \(P(x,y)\) means that the perfection of
*x* is strictly greater than *y’s* and \(Q(x,y)\) means that *x* and
*y* have the same degree of perfection):

>>> check_proof(DESCARTES) first-descartes-argument (0) Comment Ay.~P(y,d) (1) Given ~Q(c,d) (2) Given Ax.Ay.(S(x,y) -> (P(x,y) v Q(x,y))) (3) Given Ay.(R(c,y) -> Ex.S(x,y)) (4) Given R(c,d) (5) Given ~P(c,d) (6) A-Elimination (1) Ay.(S(c,y) -> (P(c,y) v Q(c,y))) (7) A-Elimination (3) S(c,d) -> (P(c,d) v Q(c,d)) (8) A-Elimination (7) |S(c,d) (9) Assumption |P(c,d) v Q(c,d) (10) Implication-Elimination (Modus Ponens) (8) (9) ||P(c,d) (11) Assumption ||F (12) Contradiction (11) (6) |~P(c,d) (13) Reductio Ad Absurdum (11) (12) |Q(c,d) (14) Or-Elimination (Left) (10) (13) |F (15) Contradiction (14) (2) ~S(c,d) (16) Reductio Ad Absurdum (9) (15) R(c,d) -> Ex.S(x,d) (17) A-Elimination (4) Ex.S(x,d) (18) Implication-Elimination (Modus Ponens) (17) (5) Ay.(S(b,y) -> (P(b,y) v Q(b,y))) (19) A-Elimination (3) S(b,d) -> (P(b,d) v Q(b,d)) (20) A-Elimination (19) |Let b satisfy S(b,d) (21) Assumption |P(b,d) v Q(b,d) (22) Implication-Elimination (Modus Ponens) (20) (21) ||P(b,d) (23) Assumption ||~P(b,d) (24) A-Elimination (1) ||F (25) Contradiction (23) (24) |~P(b,d) (26) Reductio Ad Absurdum (23) (25) |Q(b,d) (27) Or-Elimination (Left) (22) (26) |S(b,d) & Q(b,d) (28) And-Introduction (21) (27) |Ex.(S(x,d) & Q(x,d)) (29) E-Introduction (28) Ex.(S(x,d) & Q(x,d)) (30) E-Elimination (18) (21) (29) ~S(c,d) & Ex.(S(x,d) & Q(x,d)) (31) And-Introduction (16) (30) True

This output is the proof checked via FLiP, a Logical Framework in Python, a program that can also be downloaded here.