Theory Thomistic_Causal_Arguments

theory Thomistic_Causal_Arguments
  imports
    Dependency_Structures
    Foundation_Principles
    Foundation_Implications
    Foundation_Separations
    Finite_Foundation_Checker
    Second_Way_Reconstructions
    Research_Results
    Premise_Minimality
    Finite_Foundation_Analysis
begin

section ‹Summary›

text ‹
  This session formalizes a carrier-restricted theory of causal and grounding
  regress arguments.  It distinguishes acyclicity, well-foundedness, chain
  termination, local foundation, global foundation, and full grounding; proves
  the valid implications and finite equivalences; and supplies infinite and
  finite separation models, including a rooted-cycle witness showing that
  foundation and acyclicity are incomparable on arbitrary carriers.  It also
  contains an executable finite checker with exact certificate correctness,
  explicit finite cycle paths, premise-deletion countermodels, and two explicit
  Second-Way reconstruction packages.  The Cohoe package additionally records
  the proved redundancy of a separate carrier premise.
  The entry deliberately does not formalize the First or Third Ways: substantive
  treatments would require richer act/potency and modal semantics.
  All positive conclusions remain conditional on the dependency structures and
  bridge premises stated in the theories, and no formal first cause is named as
  God.
›

end