Email Gateway (Oct 28 2026 at 15:17): Email Gateway (Oct 28 2026 at 15:17):From: Jasmin Blanchette <jasmin.blanchette@ifi.lmu.de>
Subject: [isabelle] New AFP entry: Foundations and Limits of Essentially Ordered Causal Regress Arguments
Dear all,
I am pleased to announce the following new AFP entry on philosophy:
Foundations and Limits of Essentially Ordered Causal Regress Arguments
Arthur Freitas Ramos, David Barros Hulak, and Ruy Jose Guerra Barretto de Queiroz
https://isa-afp.org/entries/Thomistic_Causal_Arguments.html
This entry formalizes a carrier-restricted theory of causal and grounding regress arguments in Isabelle/HOL. It distinguishes acyclicity, well-foundedness, explicit chain termination, local foundation, global foundation, and full grounding, and proves the valid implications together with finite and infinite separation models. An executable finite checker returns either an exact independent-root certificate or a concrete missing-foundation witness. A bounded cycle analyzer produces explicit finite return-path certificates, and a certified finite profile links five declarative properties to two executable tests. The entry also formalizes Cohoe-style and Romero-Pérez-style Second-Way reconstructions with explicit translation assumptions and premise-deletion countermodels. All conclusions are conditional on stated dependency premises; no formal first cause is identified with God, and the First and Third Ways are deliberately outside scope.
Enjoy!
Jasmin
Last updated: Oct 29 2026 at 04:52 UTC