Abstract
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.
License
Note
AI assistance was used for proof engineering. The final definitions, statements, and proofs are checked by Isabelle.
Topics
- Logic/Philosophical aspects
- Logic/General logic/Mechanization of proofs
- Mathematics/Graph theory
- Mathematics/Order
Related publications
- Cohoe, C. (2013). There must be a First: Why Thomas Aquinas Rejects Infinite, Essentially Ordered, Causal Series. British Journal for the History of Philosophy, 21(5), 838–856. https://doi.org/10.1080/09608788.2013.816934
- Romero, G. E., & Pérez, D. (2012). New remarks on the cosmological argument. International Journal for Philosophy of Religion, 72(2), 103–113. https://doi.org/10.1007/s11153-012-9337-6
- Bliss, R. (2014). Viciousness and Circles of Ground. Metaphilosophy, 45(2), 245–256. Portico. https://doi.org/10.1111/meta.12072
- Rabin, G. O., & Rabern, B. (2015). Well Founding Grounding Grounding. Journal of Philosophical Logic, 45(4), 349–379. https://doi.org/10.1007/s10992-015-9376-4
- Dixon, T. S. (2016). What Is the Well-Foundedness of Grounding? Mind, 125(498), 439–468. https://doi.org/10.1093/mind/fzv112
- Pearson, O. (2022). Grounding, Well-Foundedness, and Terminating Chains. Philosophia, 51(3), 1539–1554. https://doi.org/10.1007/s11406-022-00593-x
Session Thomistic_Causal_Arguments
- Preliminaries
- Dependency_Structures
- Foundation_Principles
- Foundation_Implications
- Foundation_Separations
- Finite_Foundation_Checker
- Second_Way_Reconstructions
- Research_Results
- Premise_Minimality
- Finite_Foundation_Analysis
- Thomistic_Causal_Arguments