Arguments
- Core Logic is not paraconsistent: one proof, six certifications (2026-05-01, updated 2026-07-31) This note provides a proof that asserting Tennant's Core logic \(\mathbb{C}\) to be paraconsistent — by claiming that the antisequent \[\lnot A, A \nvdash B\] is justified in \(\mathbb{C}\) — entails a contradiction within \(\mathbb{C}\) and, consequently, if this paraconsistency claim about \(\mathbb{C}\) is not rejected as false, renders \(\mathbb{C}\) inconsistent. The proof is purely logical and proceeds in four steps within a five-rule fragment \(\mathcal{F}\) of Core logic and its refutation system in the sense of Łukasiewicz and Goranko. Each step has been machine-verified in three certifications — Coq, Lean 4 and Athena — under each of the two structural readings of \(\mathcal{F}\), six in all.
- Descartes’s First Proof of God’s Existence in First-Order Logic (2021-07-21, updated 2026-07-31) 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/ ( ...
Code
- The rules of \(\mathcal{F}\) across \(\LaTeX\), Coq, Lean, Athena and Prolog (2026-07-20, updated 2026-07-31) This note is a companion to ...
- From XFCE to EXWM: Living in Emacs Desktop on MX Linux (2026-07-12, updated 2026-07-20) 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 ...
- Notes on building SWI-Prolog for WebAssembly (WASM) (2026-01-22, updated 2026-07-31)
Provers
- How Prolog corroborates the proof that Core Logic is not paraconsistent (2026-07-21, updated 2026-07-31) The proof that Core Logic is not paraconsistent has been ...
- 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.
En français
- 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.