Theory Mechanized_Metasemantics

theory Mechanized_Metasemantics
  imports Main
begin

section ‹Object Language›

text ‹
  We introduce a small object language instead of using HOL bools directly.
  This allows object-language formulas to vary across possible worlds.
›

datatype formula =
    Atom nat
  | FNeg formula
  | FAnd formula formula
  | FOr  formula formula


section ‹Abstract Interpretive Structure›

text ‹
  Core schema:
  \[
    \mathrm{formula} \xrightarrow{\delta} D \xrightarrow{I} P(W)
  \]
  \[
    V = I \circ \delta
  \]

  D is not a semantic domain. It is a proof-theoretic / syntactic
  distinction space. Interpretation I transforms syntactic distinctions
  into possible-worlds truth-conditions.

  The locale abstracts the metasemantic factorization.
  Its assumptions do not add global axioms to HOL; they specify the
  class of interpretive structures to be instantiated below.
›

locale Interpretive_Structure =
  fixes negD  :: "'d ⇒ 'd"
    and andD  :: "'d ⇒ 'd ⇒ 'd"
    and orD   :: "'d ⇒ 'd ⇒ 'd"
    and derD  :: "'d ⇒ 'd ⇒ bool"   (infix "⊢D" 50)
    and delta :: "formula ⇒ 'd"
    and I     :: "'d ⇒ 'w ⇒ bool"
    and R     :: "'w ⇒ 'w ⇒ bool"

  assumes delta_neg:
    "delta (FNeg φ) = negD (delta φ)"

  assumes delta_and:
    "delta (FAnd φ ψ) = andD (delta φ) (delta ψ)"

  assumes delta_or:
    "delta (FOr φ ψ) = orD (delta φ) (delta ψ)"

  assumes I_neg:
    "I (negD d) w ⟷ ¬ I d w"

  assumes I_and:
    "I (andD d1 d2) w ⟷ I d1 w ∧ I d2 w"

  assumes I_or:
    "I (orD d1 d2) w ⟷ I d1 w ∨ I d2 w"

  assumes der_sound:
    "d1 ⊢D d2 ⟹ I d1 w ⟹ I d2 w"

begin


section ‹Valuation and Modal Operators›

definition V :: "formula ⇒ 'w ⇒ bool" where
  "V φ w ≡ I (delta φ) w"

text ‹
  Standard valuation is reconstructed as V = I o delta.
›

definition Box :: "formula ⇒ 'w ⇒ bool" where
  "Box φ w ≡ ∀v. R w v ⟶ V φ v"

definition Dia :: "formula ⇒ 'w ⇒ bool" where
  "Dia φ w ≡ ∃v. R w v ∧ V φ v"

definition Contingent :: "formula ⇒ 'w ⇒ bool" where
  "Contingent φ w ≡ Dia φ w ∧ Dia (FNeg φ) w"

definition ModalClosure :: "formula ⇒ 'w ⇒ bool" where
  "ModalClosure φ w ≡ ¬ Dia (FNeg φ) w"


section ‹Valuation Factorization›

lemma valuation_factorization:
  "V φ w ⟷ I (delta φ) w"
  by (simp add: V_def)

text ‹
  This is the formal core of the thesis:
  valuation does not eliminate interpretation; it factors through it.
›


section ‹Modal Operators Use Interpreted Distinction›

lemma box_uses_interpreted_distinction:
  "Box φ w ⟷ (∀v. R w v ⟶ I (delta φ) v)"
  by (simp add: Box_def V_def)

lemma dia_uses_interpreted_distinction:
  "Dia φ w ⟷ (∃v. R w v ∧ I (delta φ) v)"
  by (simp add: Dia_def V_def)


section ‹Negation and Modal Contrast›

lemma interpreted_negation:
  "I (delta (FNeg φ)) w ⟷ ¬ I (delta φ) w"
  using delta_neg I_neg by simp

lemma valuation_negation:
  "V (FNeg φ) w ⟷ ¬ V φ w"
  by (simp add: V_def interpreted_negation)

lemma dia_neg_as_false_possibility:
  "Dia (FNeg φ) w ⟷ (∃v. R w v ∧ ¬ I (delta φ) v)"
  by (simp add: Dia_def V_def interpreted_negation)

lemma box_as_no_false_possibility:
  "Box φ w ⟷ ¬ (∃v. R w v ∧ ¬ I (delta φ) v)"
proof -
  have "Box φ w ⟷ (∀v. R w v ⟶ I (delta φ) v)"
    by (simp add: box_uses_interpreted_distinction)
  also have "... ⟷ ¬ (∃v. R w v ∧ ¬ I (delta φ) v)"
    by blast
  finally show ?thesis .
qed

text ‹
  This theorem states the modal-semantic content of necessity:
  Box phi means that no accessible world realizes the interpreted contrast
  corresponding to not-phi.
›


section ‹Possibility and Contingency›

lemma contingency_requires_interpreted_contrast:
  "Contingent φ w ⟷
    (∃v. R w v ∧ I (delta φ) v) ∧
    (∃u. R w u ∧ ¬ I (delta φ) u)"
  by (simp add: Contingent_def Dia_def V_def interpreted_negation)

text ‹
  Contingency requires interpreted variation across possible worlds.
›


section ‹Necessity as Modal Closure›

lemma box_iff_modal_closure:
  "Box φ w ⟷ ModalClosure φ w"
proof -
  have "Box φ w ⟷ ¬ (∃v. R w v ∧ ¬ I (delta φ) v)"
    by (simp add: box_as_no_false_possibility)
  also have "... ⟷ ¬ Dia (FNeg φ) w"
    by (simp add: Dia_def V_def interpreted_negation)
  finally show ?thesis
    by (simp add: ModalClosure_def)
qed

text ‹
  Necessity is modal closure against the interpreted false possibility.
›


section ‹No Semantics Without Interpretation›

text ‹
  The following definitions mark the philosophical distinction:
  syntactic distinction alone is not yet modal semantic status.
›

definition Interpretable :: "'d ⇒ bool" where
  "Interpretable d ≡ ∀w. I d w ∨ ¬ I d w"

definition Modally_Evaluable :: "formula ⇒ bool" where
  "Modally_Evaluable φ ≡ Interpretable (delta φ)"

lemma any_delta_interpretable:
  "Interpretable (delta φ)"
  unfolding Interpretable_def
  by simp

lemma modal_evaluation_requires_interpretability:
  assumes "Box φ w ∨ Dia φ w"
  shows "Interpretable (delta φ)"
  using any_delta_interpretable by simp

text ‹
  This lemma is intentionally weak, because in HOL every boolean is
  evaluable once I is given. Philosophically, the point is that modal
  evaluation in this framework is always evaluation of I(delta phi).
›


section ‹Main Thesis Theorems›

theorem necessity_requires_interpretive_factorization:
  "Box φ w ⟷ (∀v. R w v ⟶ I (delta φ) v)"
  by (simp add: box_uses_interpreted_distinction)

theorem possibility_requires_interpretive_factorization:
  "Dia φ w ⟷ (∃v. R w v ∧ I (delta φ) v)"
  by (simp add: dia_uses_interpreted_distinction)

theorem necessity_as_interpreted_false_possibility_block:
  "Box φ w ⟷ ¬ (∃v. R w v ∧ ¬ I (delta φ) v)"
  by (simp add: box_as_no_false_possibility)

text ‹
  Final formal slogan:

  Necessity is not grounded in valuation alone.
  Since V phi w is definitionally I (delta phi) w,
  modal necessity is grounded in interpreted distinction.
›

end


section ‹A Conservative Concrete Model›

text ‹
  We now give a concrete instance of the abstract locale.

  The concrete Boolean model is used only as a conservative witness:
  it shows that the locale assumptions are jointly satisfiable and that
  the factorized semantics admits genuine contingency.

  The model uses:
  \[
    W_0 = \mathrm{bool}
  \]
  \[
    D_0 = W_0 \Rightarrow \mathrm{bool}
  \]

  Thus distinctions are truth-conditions over the two-world frame.
  Interpretation is simply application.
›

type_synonym W0 = bool
type_synonym D0 = "W0 ⇒ bool"


subsection ‹Concrete Distinction Operations›

definition negD0 :: "D0 ⇒ D0" where
  "negD0 d ≡ (λw. ¬ d w)"

definition andD0 :: "D0 ⇒ D0 ⇒ D0" where
  "andD0 d1 d2 ≡ (λw. d1 w ∧ d2 w)"

definition orD0 :: "D0 ⇒ D0 ⇒ D0" where
  "orD0 d1 d2 ≡ (λw. d1 w ∨ d2 w)"

definition derD0 :: "D0 ⇒ D0 ⇒ bool" where
  "derD0 d1 d2 ≡ (∀w. d1 w ⟶ d2 w)"


subsection ‹Concrete Parsing, Interpretation, and Accessibility›

text ‹
  Atom 0 varies across worlds.
  Other atoms are interpreted as constantly true, only for simplicity.
›

primrec delta0 :: "formula ⇒ D0" where
  "delta0 (Atom n) = (λw. if n = 0 then w else True)"
| "delta0 (FNeg φ) = negD0 (delta0 φ)"
| "delta0 (FAnd φ ψ) = andD0 (delta0 φ) (delta0 ψ)"
| "delta0 (FOr φ ψ) = orD0 (delta0 φ) (delta0 ψ)"

definition I0 :: "D0 ⇒ W0 ⇒ bool" where
  "I0 d w ≡ d w"

definition R0 :: "W0 ⇒ W0 ⇒ bool" where
  "R0 w v ≡ True"


subsection ‹Locale Interpretation›

interpretation Concrete_Model:
  Interpretive_Structure negD0 andD0 orD0 derD0 delta0 I0 R0
proof
  fix φ ψ :: formula

  show "delta0 (FNeg φ) = negD0 (delta0 φ)"
    by simp

  show "delta0 (FAnd φ ψ) = andD0 (delta0 φ) (delta0 ψ)"
    by simp

  show "delta0 (FOr φ ψ) = orD0 (delta0 φ) (delta0 ψ)"
    by simp

next
  fix d :: D0 and w :: W0

  show "I0 (negD0 d) w ⟷ ¬ I0 d w"
    by (simp add: I0_def negD0_def)

next
  fix d1 d2 :: D0 and w :: W0

  show "I0 (andD0 d1 d2) w ⟷ I0 d1 w ∧ I0 d2 w"
    by (simp add: I0_def andD0_def)

next
  fix d1 d2 :: D0 and w :: W0

  show "I0 (orD0 d1 d2) w ⟷ I0 d1 w ∨ I0 d2 w"
    by (simp add: I0_def orD0_def)

next
  fix d1 d2 :: D0 and w :: W0

  assume h1: "derD0 d1 d2"
  assume h2: "I0 d1 w"

  show "I0 d2 w"
    using h1 h2 by (simp add: derD0_def I0_def)
qed


section ‹Concrete Non-Vacuity Witnesses›

text ‹
  The concrete model contains a non-trivial distinction varying across worlds.
›

lemma concrete_has_nontrivial_distinction:
  "∃d :: D0. I0 d True ∧ ¬ I0 d False"
proof
  let ?d = "λw :: W0. w"
  show "I0 ?d True ∧ ¬ I0 ?d False"
    by (simp add: I0_def)
qed

lemma concrete_atom0_varies:
  "I0 (delta0 (Atom 0)) True ∧ ¬ I0 (delta0 (Atom 0)) False"
  by (simp add: I0_def)

lemma concrete_has_accessible_variation:
  "∃d :: D0. ∃w v :: W0.
      R0 w v ∧ I0 d v ∧ (∃u. R0 w u ∧ ¬ I0 d u)"
proof -
  let ?d = "λx :: W0. x"
  have "R0 False True ∧ I0 ?d True ∧ (∃u. R0 False u ∧ ¬ I0 ?d u)"
    by (rule conjI, simp add: R0_def,
        rule conjI, simp add: I0_def,
        rule exI[where x=False], simp add: R0_def I0_def)
  then show ?thesis
    by blast
qed


section ‹Concrete Object-Language Modal Witnesses›

text ‹
  Since Atom 0 varies across worlds and R0 is universal, Atom 0 is
  genuinely contingent at either world.
›

lemma concrete_dia_atom0:
  "Concrete_Model.Dia (Atom 0) w"
proof -
  have "R0 w True ∧ Concrete_Model.V (Atom 0) True"
    by (simp add: R0_def Concrete_Model.V_def I0_def)
  then show ?thesis
    unfolding Concrete_Model.Dia_def
    by blast
qed

lemma concrete_dia_not_atom0:
  "Concrete_Model.Dia (FNeg (Atom 0)) w"
proof -
  have "R0 w False ∧ Concrete_Model.V (FNeg (Atom 0)) False"
    by (simp add: R0_def Concrete_Model.V_def I0_def negD0_def)
  then show ?thesis
    unfolding Concrete_Model.Dia_def
    by blast
qed

lemma concrete_atom0_contingent:
  "Concrete_Model.Contingent (Atom 0) w"
  by (simp add:
      Concrete_Model.Contingent_def
      concrete_dia_atom0
      concrete_dia_not_atom0)

lemma concrete_exists_contingent_formula:
  "∃φ w. Concrete_Model.Contingent φ w"
  using concrete_atom0_contingent by blast


section ‹Concrete Modal Sanity Checks›

lemma concrete_not_box_atom0:
  "¬ Concrete_Model.Box (Atom 0) w"
proof -
  have "R0 w False ∧ ¬ Concrete_Model.V (Atom 0) False"
    by (simp add: R0_def Concrete_Model.V_def I0_def)
  then show ?thesis
    unfolding Concrete_Model.Box_def
    by blast
qed

lemma concrete_not_box_not_atom0:
  "¬ Concrete_Model.Box (FNeg (Atom 0)) w"
proof -
  have "R0 w True ∧ ¬ Concrete_Model.V (FNeg (Atom 0)) True"
    by (simp add: R0_def Concrete_Model.V_def I0_def negD0_def)
  then show ?thesis
    unfolding Concrete_Model.Box_def
    by blast
qed

text ‹
  This is the main no-collapse witness: possibility does not imply
  necessity for Atom 0 in the concrete model.
›

lemma concrete_no_modal_collapse_atom0:
  "Concrete_Model.Dia (Atom 0) w ∧ ¬ Concrete_Model.Box (Atom 0) w"
  by (simp add: concrete_dia_atom0 concrete_not_box_atom0)

lemma concrete_no_modal_collapse_not_atom0:
  "Concrete_Model.Dia (FNeg (Atom 0)) w ∧ ¬ Concrete_Model.Box (FNeg (Atom 0)) w"
  by (simp add: concrete_dia_not_atom0 concrete_not_box_not_atom0)


section ‹Concrete Unfolding of the Main Thesis›

lemma concrete_valuation_factorization:
  "Concrete_Model.V φ w ⟷ I0 (delta0 φ) w"
  by (simp add: Concrete_Model.valuation_factorization)

lemma concrete_box_unfolding:
  "Concrete_Model.Box φ w ⟷ (∀v. R0 w v ⟶ I0 (delta0 φ) v)"
  by (simp add: Concrete_Model.box_uses_interpreted_distinction)

lemma concrete_possibility_unfolding:
  "Concrete_Model.Dia φ w ⟷ (∃v. R0 w v ∧ I0 (delta0 φ) v)"
  by (simp add: Concrete_Model.dia_uses_interpreted_distinction)

lemma concrete_necessity_as_no_false_possibility:
  "Concrete_Model.Box φ w ⟷ ¬ (∃v. R0 w v ∧ ¬ I0 (delta0 φ) v)"
  by (simp add: Concrete_Model.necessity_as_interpreted_false_possibility_block)


section ‹Summary of Contributions›

text ‹
  This theory provides:

  1. an abstract locale for interpretive modal metasemantics;
  2. an explicit object language of formulas;
  3. a parsing map delta from formulas into syntactic distinctions;
  4. valuation factorization V = I o delta;
  5. modal necessity as closure against interpreted false possibility;
  6. a conservative concrete model witnessing consistency of the locale;
  7. a non-trivial distinction witness at the D-level;
  8. an object-language contingent formula witness;
  9. a no-modal-collapse sanity check for Atom 0.

  Thus modal evaluation is formally shown to operate over interpreted
  distinctions rather than over valuation alone.
›

end