Arguments

  • Descartes’s First Proof of God’s Existence in First-Order Logic (2021-07-21, updated 2026-06-03) In the language of first-order logic, I provide in this post a proof in natural deduction which translates the argument that Descartes gave as evidence of the existence of God. (A French version of my posts on Anselm and Descartes has been published in the Brasilian Review /Revista de Filosofia moderna e contemporânea/ ([[https://periodicos.unb.br/index.php/fmc/issue/view/1952][v. 8 n. 1 (2020): Dossiê "Formas da Razão"]]). This paper which can be downloaded [[https://periodicos.unb.br/index.php/fmc/article/view/31015/26518][here]] or [[https://www.vidal-rosset.net/vidal-rosset-2020.pdf][there]] contains a reply to this last question.
  • A Triple Certified Proof that Core Logic is not Paraconsistent (2026-05-01, updated 2026-06-03) This note provides a proof that Tennant's two claims — that his own logical system is paraconsistent, and that it overlaps minimal logic — are both false. This proof is triple certified: by Coq, by Lean 4 and by Athena.

Code

Provers

  • SWI-Tinker for G4+: A SWI-Prolog F.O.L. Prover with nanoCop Cross-Validation (2025-11-17, updated 2026-06-03) G4+ is a Prolog prover for minimal, intuitionistic and classical logic, with cross-validation with nanoCoP. Put a in SWI-Tinker, it provides LaTeX proofs in three formats: sequent calculus, natural deduction in tree style, and natural deduction in flag style. It is the main prover of the Prover section of this blog.

En français

  • Propositions pour l’enseignement supérieur (2022-12-28, updated 2026-06-03) À quelques années de mon départ en retraite, je fais ici quelques propositions de réforme pour l’enseignement supérieur en philosophie. Ce texte n’engage que moi.