Proof checkers

2021-01-28, updated 2024-03-01 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):

\begin{equation} \tag{11} \forall y \lnot(y > d),\lnot(c = d), \forall x \forall y(Sxy \to x \geqslant y), \forall y(Rcy \to \exists x Sxy), Rcd \vdash \lnot Scd \land \exists x(Sxd \land (x = d)) \end{equation}

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

\forall y \lnot(Byd) , \lnot Ecd  , \forall y(Rcy \rightarrow \exists x
Sxy ) , Rcd , \forall  x \forall y(Sxy \rightarrow (Bxy \lor Exy)) |=
\lnot Scd \land \exists x(Sxd \land 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.