Arguments

  • Core Logic is not paraconsistent: one proof, six certifications (2026-05-01, updated 2026-08-04) 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

Provers

  • G4m and nkm provers for modal logic (2026-10-18) Two provers for propositional modal logic run in the browser, in SWI-Tinker, beside the first-order prover G4+. For a formula and a modal system (K, D, T, B, K4, S4, S5, K5, KD45), they first look for a countermodel; if there is none, /G4m/ gives a proof in a labelled sequent calculus of the G4 family, and names the weakest logic in which the formula holds (minimal, intuitionistic or classical); then /nkm/ gives a proof in labelled natural deduction, as a tree and in the Fitch style of Fitch's /Symbolic Logic/ (1952). This page is a guide for reading these outputs. It assumes no knowledge of modal logic: it explains the possible worlds, the systems, the labels, and then each kind of proof on examples that can be run with one click.
  • A temporal logic prover from Volpe’s work (2026-10-16) nkt is a temporal logic prover built on the labeled natural deduction systems of Marco Volpe's thesis ...
  • 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.