‎

Arguments

A Triple Certified Proof that Core Logic is not Paraconsistent (2026-05-01, updated 2026-07-17) This note establishes, with machine-checked certifications in Coq, Lean 4 and Athena, that Core logic is not paraconsistent: Tennant's Claim 1 — the antisequent \(\lnot A, A \nvdash B\) — entails a contradiction in Core logic. The proof is purely logical, in four steps within a five-rule fragment \(\mathcal{F}\) of Core logic and its refutation system in the sense of Łukasiewicz and Goranko; every step is certified.
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.