‎

Arguments

A Triple Certified Proof that Core Logic is not Paraconsistent (2026-05-01, updated 2026-07-10) 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.
Descartes’s First Proof of God’s Existence in First-Order Logic (2021-07-21) 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.

From XFCE to EXWM: Living in Emacs Desktop on MX Linux (2026-07-12, updated 2026-07-13) Emacs is a text editor that, through EXWM (Emacs X Window Manager), can also be your window manager — meaning every X application on your screen becomes an Emacs buffer, managed with Emacs keybindings, Emacs windows, and Emacs workflows. This is the story of replacing XFCE with [[https://github.com/emacs-exwm/exwm][EXWM]] on MX Linux, why it took more than an afternoon to get right, and what the result actually looks like day to day. I am strongly indebted to [[https://claude.ai][claude.ai]] for help both with the EXWM setup and with this technical report.
Notes on building SWI-Prolog for WebAssembly (WASM) (2026-01-22)

SWI-Tinker for G4+: A SWI-Prolog F.O.L. Prover with nanoCop Cross-Validation (2025-11-17) 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.

Propositions pour l’enseignement supérieur (2022-12-28) À 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.