Theory Second_Way_Reconstructions

theory Second_Way_Reconstructions
  imports Foundation_Separations
begin

section ‹An Explicit Essentially Ordered-Series Interface›

text ‹
  The phrase essentially ordered is not identified with well-foundedness.  We
  expose one additional, source-facing predicate @{term derivative} for one
  explicit formal explication of the claim that members of a selected causal
  series have derivative causal efficacy.  In this explication, on the
  selected ancestry, derivative status is tied to the dependency relation
  itself: a member is derivative exactly when it has an immediate predecessor
  in the carrier.  Thus an independent member is a genuine non-derivative
  endpoint of the series, rather than merely receiving an arbitrary
  annotation.  This is a modeling choice, not a definition of derivative
  causal efficacy in every metaphysical respect.  The separate possession and
  exercise interface in the research layer deliberately tests a different
  local reading.  Well-foundedness remains a separate hypothesis,
  so this interface can describe an infinite derivative series as well as a
  founded one.
›

definition essentially_ordered_series ::
  "'a set ⇒ ('a ⇒ 'a ⇒ bool) ⇒
   ('a ⇒ bool) ⇒ 'a ⇒ bool"
where
  "essentially_ordered_series C D derivative a ⟷
     a ∈ C ∧ derivative a ∧ grounded_in C D a ∧
     (∀x. dependency_ancestor C D x a ⟶
       (derivative x ⟷ grounded_in C D x))"

lemma essentially_ordered_seriesD:
  assumes "essentially_ordered_series C D derivative a"
  shows "a ∈ C" "derivative a" "grounded_in C D a"
    and "∀x. dependency_ancestor C D x a ⟶
      (derivative x ⟷ grounded_in C D x)"
  using assms by (auto simp: essentially_ordered_series_def)

lemma essentially_ordered_series_derivative_iff:
  assumes "essentially_ordered_series C D derivative a"
    and "dependency_ancestor C D x a"
  shows "derivative x ⟷ grounded_in C D x"
  using assms by (auto simp: essentially_ordered_series_def)

lemma essentially_ordered_series_has_non_derivative_endpoint:
  assumes "essentially_ordered_series C D derivative a"
    and "first_member_in C D f a"
  shows "¬ derivative f"
proof -
  have ancestor: "dependency_ancestor C D f a"
    using first_member_inD[OF assms(2)] by blast
  have independent: "independent_in C D f"
    using first_member_inD[OF assms(2)] by blast
  have not_grounded: "¬ grounded_in C D f"
    using independent by (auto simp: grounded_in_def independent_in_def)
  have derivative_iff: "derivative f ⟷ grounded_in C D f"
    using essentially_ordered_series_derivative_iff[OF assms(1) ancestor] .
  then show ?thesis
    using not_grounded by blast
qed

lemma integer_predecessor_is_essentially_ordered:
  "essentially_ordered_series UNIV integer_predecessor_cause
    (λ_. True) (0 :: int)"
proof -
  have incoming0:
      "∃y. integer_predecessor_cause y (0 :: int)"
    using integer_predecessor_has_incoming[of "0 :: int"] .
  have incoming:
      "∀x. ∃y. integer_predecessor_cause y x"
    using integer_predecessor_has_incoming by blast
  show ?thesis
    unfolding essentially_ordered_series_def
    using incoming0 incoming
    by (auto simp: grounded_in_def integer_predecessor_cause_def)
qed

theorem essentially_ordered_does_not_mean_well_founded:
  "essentially_ordered_series UNIV integer_predecessor_cause
    (λ_. True) (0 :: int) ∧
   ¬ well_founded_on UNIV integer_predecessor_cause"
  using integer_predecessor_is_essentially_ordered
    integer_predecessor_not_well_founded_on by blast

section ‹Cohoe-Style Formal Translation Package›

text ‹
  The formal Cohoe-style translation keeps three interpretive commitments separate:
  there is a caused target, every caused target belongs to an essentially
  ordered derivative series, and a full-grounding relation supplies a
  foundation witness.  These are formal explications of source-level claims,
  not literal quotations.  The series predicate itself already states that its
  target lies in the carrier, so carrier membership is not an independent
  premise.  Because it also states that the target is grounded, no duplicate
  predecessor premise is needed.  The endpoint, nonemptiness, and
  ancestry-closure bridges from plural grounding to binary dependence are
  explicit locale assumptions.
›

definition cohoe_second_way_premises ::
  "'a set ⇒ ('a ⇒ 'a ⇒ bool) ⇒
   ('a set ⇒ 'a ⇒ bool) ⇒
   ('a ⇒ bool) ⇒ ('a ⇒ bool) ⇒ bool"
where
  "cohoe_second_way_premises C D G derivative caused ⟷
     (∃a. caused a) ∧
     (∀a. caused a ⟶
       essentially_ordered_series C D derivative a) ∧
     full_foundation_on C D G C"

definition cohoe_second_way_conclusion ::
  "'a set ⇒ ('a ⇒ 'a ⇒ bool) ⇒
   ('a ⇒ bool) ⇒ ('a ⇒ bool) ⇒ bool"
where
  "cohoe_second_way_conclusion C D derivative caused ⟷
     (∀a. caused a ⟶
       (∃x. first_cause_in C D x a ∧ ¬ derivative x))"

locale cohoe_second_way_reconstruction =
  fixes C :: "'a set"
    and D :: "'a ⇒ 'a ⇒ bool"
    and G :: "'a set ⇒ 'a ⇒ bool"
    and derivative :: "'a ⇒ bool"
    and caused :: "'a ⇒ bool"
  assumes cohoe_assumptions:
    "cohoe_second_way_premises C D G derivative caused"
    and singleton_endpoint:
    "⋀x a. x ∈ C ⟹ a ∈ C ⟹ D x a ⟹
      partial_grounding_on C G x a"
    and full_nonempty:
    "⋀S a. full_grounding_on C G S a ⟹ S ≠ {}"
    and full_ancestry:
    "⋀S a x. full_grounding_on C G S a ⟹ x ∈ S ⟹
      dependency_ancestor C D x a"
begin

lemma cohoe_has_local_foundation:
  "local_foundation_on C D C"
proof -
  obtain "full_foundation_on C D G C"
    using cohoe_assumptions by (auto simp: cohoe_second_way_premises_def)
  then show ?thesis
    using full_foundation_implies_local_foundation[
      where C = C and D = D and G = G and R = C]
      singleton_endpoint full_nonempty full_ancestry by blast
qed

theorem cohoe_first_cause_of:
  assumes "caused a"
  shows "∃x. first_cause_in C D x a"
proof -
  have premises_expanded:
      "(∀a. caused a ⟶
        essentially_ordered_series C D derivative a)"
    using cohoe_assumptions by (auto simp: cohoe_second_way_premises_def)
  obtain series: "essentially_ordered_series C D derivative a"
    using premises_expanded assms by blast
  have aC: "a ∈ C"
    using series by (rule essentially_ordered_seriesD)
  have grounded: "grounded_in C D a"
    using series by (rule essentially_ordered_seriesD)
  have local:
      "∀u ∈ C. grounded_in C D u ⟶
        (∃f. first_member_in C D f u)"
    using cohoe_has_local_foundation
    by (simp add: local_foundation_on_def)
  have first_exists:
      "∃f. first_member_in C D f a"
    using local aC grounded by blast
  then obtain f where first_member: "first_member_in C D f a"
    by blast
  have f_neq: "f ≠ a"
  proof
    assume "f = a"
    have f_independent: "independent_in C D f"
      using first_member_inD[OF first_member] by blast
    obtain b where "b ∈ C" and "D b a"
      using grounded by (auto simp: grounded_in_def)
    then show False
      using f_independent ‹f = a›
      by (auto simp: independent_in_def)
  qed
  show ?thesis
    using first_member f_neq
    by (auto simp: first_cause_in_def)
qed

theorem cohoe_non_derivative_first_cause_of:
  assumes "caused a"
  shows "∃x. first_cause_in C D x a ∧ ¬ derivative x"
proof -
  have premises_expanded:
      "(∀a. caused a ⟶
        essentially_ordered_series C D derivative a)"
    using cohoe_assumptions by (auto simp: cohoe_second_way_premises_def)
  obtain series: "essentially_ordered_series C D derivative a"
    using premises_expanded assms by blast
  obtain x where first_cause: "first_cause_in C D x a"
    using cohoe_first_cause_of[OF assms] by blast
  have first_member: "first_member_in C D x a"
    using first_cause_inD[OF first_cause] by blast
  have not_derivative: "¬ derivative x"
    using essentially_ordered_series_has_non_derivative_endpoint
      [OF series first_member] .
  then show ?thesis
    using first_cause by blast
qed

theorem cohoe_exact_conclusion:
  "cohoe_second_way_conclusion C D derivative caused"
  unfolding cohoe_second_way_conclusion_def
  using cohoe_non_derivative_first_cause_of by blast

theorem cohoe_global_first_cause:
  assumes "∃a. caused a"
  shows "∃x. independent_in C D x"
proof -
  obtain a where "caused a"
    using assms by blast
  obtain x where first_cause: "first_cause_in C D x a"
    using cohoe_first_cause_of[OF ‹caused a›] by blast
  have first_member: "first_member_in C D x a"
    using first_cause_inD[OF first_cause] by blast
  have independent: "independent_in C D x"
    using first_member_inD[OF first_member] by blast
  then show ?thesis by blast
qed

end

section ‹Romero--Pérez Reconstruction›

text ‹
  Romero and Pérez present a first-order reconstruction in the source
  discussion.  The Isabelle/HOL encoding below is not itself a first-order
  sentence: @{term well_founded_on} is a higher-order predicate quantifying
  over carrier subsets.  The section therefore separates the source-level
  presentation from the formal encoding.  Its conclusion is the existence of
  at least one member of the carrier with no immediate dependency predecessor.
  It does not assert uniqueness, necessity, agency, or that the first member is
  the cause of the universe.  The equivalence between well-foundedness and
  absence of an infinite descending sequence uses Isabelle/HOL's classical
  well-foundedness library, including its standard choice-based background.
›

definition romero_perez_second_way_premises ::
  "'a set ⇒ ('a ⇒ 'a ⇒ bool) ⇒
   ('a ⇒ bool) ⇒ bool"
where
  "romero_perez_second_way_premises C D caused ⟷
     (∃a ∈ C. caused a) ∧
     (∀a. caused a ⟶
       a ∈ C ∧ (∃b ∈ C. D b a)) ∧
     well_founded_on C D"

definition romero_perez_second_way_conclusion ::
  "'a set ⇒ ('a ⇒ 'a ⇒ bool) ⇒ bool"
where
  "romero_perez_second_way_conclusion C D ⟷
     (∃x ∈ C. independent_in C D x)"

locale romero_perez_second_way_reconstruction =
  fixes C :: "'a set"
    and D :: "'a ⇒ 'a ⇒ bool"
    and caused :: "'a ⇒ bool"
  assumes rp_assumptions:
    "romero_perez_second_way_premises C D caused"
begin

lemma romero_perez_well_founded:
  "well_founded_on C D"
  using rp_assumptions by (auto simp: romero_perez_second_way_premises_def)

theorem romero_perez_exact_conclusion:
  "romero_perez_second_way_conclusion C D"
proof -
  obtain a where "a ∈ C" and "caused a"
    using rp_assumptions by (auto simp: romero_perez_second_way_premises_def)
  obtain x where "x ∈ C"
    and "dependency_ancestor C D x a"
    and "independent_in C D x"
    using well_founded_has_minimal_ancestor[
      OF romero_perez_well_founded ‹a ∈ C›] .
  then show ?thesis
    by (auto simp: romero_perez_second_way_conclusion_def)
qed

theorem romero_perez_first_cause_of:
  assumes "caused a"
  shows "∃x. first_cause_in C D x a"
proof -
  have aC: "a ∈ C"
    using rp_assumptions assms
    by (auto simp: romero_perez_second_way_premises_def)
  have predecessor: "∃b ∈ C. D b a"
    using rp_assumptions assms
    by (auto simp: romero_perez_second_way_premises_def)
  have grounded: "grounded_in C D a"
    using aC predecessor by (auto simp: grounded_in_def)
  obtain f where first_member: "first_member_in C D f a"
    using well_founded_implies_local_foundation[
      OF romero_perez_well_founded, of C]
      unfolding local_foundation_on_def
    using aC grounded by blast
  have f_neq: "f ≠ a"
  proof
    assume "f = a"
    have f_independent: "independent_in C D f"
      using first_member_inD[OF first_member] by blast
    obtain b where "b ∈ C" and "D b a"
      using predecessor by blast
    then show False
      using f_independent ‹f = a›
      by (auto simp: independent_in_def)
  qed
  show ?thesis
    using first_member f_neq
    by (auto simp: first_cause_in_def)
qed

end

section ‹Comparison and Separation Summary›

theorem cohoe_conclusion_implies_global_independence:
  assumes "cohoe_second_way_conclusion C D derivative caused"
    and "∃a. caused a"
  shows "∃x. independent_in C D x"
  using assms
  unfolding cohoe_second_way_conclusion_def
  by (meson first_cause_inD first_member_inD)

theorem romero_perez_premises_imply_cohoe_style_conclusion:
  assumes "romero_perez_second_way_premises C D caused"
  shows "∀a. caused a ⟶
    (∃x. first_cause_in C D x a)"
proof (intro allI impI)
  fix a
  assume "caused a"
  interpret R: romero_perez_second_way_reconstruction C D caused
    by (rule romero_perez_second_way_reconstruction.intro[OF assms])
  show "∃x. first_cause_in C D x a"
    using R.romero_perez_first_cause_of[OF ‹caused a›] .
qed

theorem local_foundation_does_not_imply_well_founded:
  "local_foundation_on UNIV pedestal_dependency UNIV ∧
   ¬ well_founded_on UNIV pedestal_dependency"
  using pedestal_local_foundation pedestal_not_well_founded by blast

theorem global_foundation_does_not_imply_full_foundation:
  "local_foundation_on {0, 1, 2} paired_dependency {2} ∧
   partial_grounding_on {0, 1, 2} paired_full_grounding 0 2 ∧
   ¬ full_foundation_on {0, 1, 2} paired_dependency
     paired_full_grounding {2}"
  using partial_full_grounding_diverge by blast

theorem second_way_reconstruction_comparison:
  "(∀a. caused a ⟶
      (∃x. first_cause_in C D x a)) ⟶
      ((∃a. caused a) ⟶ (∃x. independent_in C D x))"
  by (auto simp: first_cause_in_def first_member_in_def
    independent_in_def)

theorem second_way_separation_summary:
  "(∃a. essentially_ordered_series UNIV
      integer_predecessor_cause (λ_. True) (a :: int)) ∧
   ¬ well_founded_on UNIV integer_predecessor_cause ∧
   local_foundation_on UNIV pedestal_dependency UNIV ∧
   global_foundation_on UNIV pedestal_dependency UNIV ∧
   ¬ well_founded_on UNIV pedestal_dependency ∧
   partial_grounding_on {0, 1, 2} paired_full_grounding 0 2 ∧
   ¬ full_foundation_on {0, 1, 2} paired_dependency
     paired_full_grounding {2}"
  using integer_predecessor_is_essentially_ordered
    integer_predecessor_not_well_founded_on
    foundation_without_well_foundedness_pedestal
    partial_full_grounding_diverge by blast

theorem second_way_foundation_headline:
  assumes "(∀a. caused a ⟶
      (∃x. first_cause_in C D x a))"
  shows "(∃a. caused a) ⟶ (∃x. independent_in C D x)"
  using second_way_reconstruction_comparison assms by blast

end