From d922d2447f0f7a2a5e2adbf2a427fff9e970543c Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Tue, 27 Oct 2026 11:44:49 -0700 Subject: [PATCH 1/2] refactor(Logic/Modal): extensionality via DependsOn, textbook headers --- Linglib/Logic/Modal/Basic.lean | 60 ++++-- Linglib/Logic/Modal/Defs.lean | 73 ++++--- Linglib/Logic/Modal/Epistemic.lean | 47 +++-- Linglib/Logic/Modal/Extensional.lean | 199 +++++++++++------- .../Modal/FirstOrder/Correspondence.lean | 98 ++++----- Linglib/Logic/Modal/FirstOrder/Semantics.lean | 56 +++-- Linglib/Logic/Modal/FirstOrder/Syntax.lean | 32 ++- .../Modification/Classification.lean | 6 +- Linglib/Semantics/Reference/Rigidity.lean | 26 ++- Studies/Kamp1975.lean | 47 +++-- Studies/Kripke1980.lean | 2 +- Studies/Zimmermann2026.lean | 24 ++- references.bib | 8 +- 13 files changed, 397 insertions(+), 281 deletions(-) diff --git a/Linglib/Logic/Modal/Basic.lean b/Linglib/Logic/Modal/Basic.lean index 4bd36642e7..004250f4e7 100644 --- a/Linglib/Logic/Modal/Basic.lean +++ b/Linglib/Logic/Modal/Basic.lean @@ -6,22 +6,40 @@ public import Mathlib.Data.Fintype.Basic public import Mathlib.Order.Lattice /-! -# Modal logic over accessibility relations - -This file proves the order theory of `□` and `◇` beyond their Galois connection -(`diamond_box_gc`): antitonicity in the relation (conversational backgrounds -strengthen necessity by shrinking accessibility), necessity along the transitive closure as the -infinite conjunction of iterated necessity, and the modal square of opposition. It also defines -the bundled frame classes `IsS5Frame`, `IsKD45Frame`, `IsK45Frame`, `IsKTBFrame`, and the -indicial operators, with Montague's S5 `□`/`◇` as the universal-accessibility case -`R = .univ`. On propositions as sets necessity along the transitive closure is mathlib's +# Accessibility and the strength of modals + +Necessity grows stronger as accessibility shrinks: +[necessity is antitone in the accessibility relation](##box_restrict) and possibility is +monotone, so a conversational background that rules out more worlds yields a stronger necessity +modal. Necessity along the transitive closure of a relation +[is the infinite conjunction](##box_transGen_iff) $\Box p \land \Box \Box p \land \cdots$, which +is the shape of common knowledge. Along a serial relation $\Box p$, $\Box \neg p$, $\Diamond p$ +and $\neg \Box p$ [form a square of opposition](##modalSquare_relations). + +The standard modal systems are named by the axioms their frames validate. An S5 frame is +reflexive and Euclidean, a K45 frame transitive and Euclidean, a KD45 frame, the frame of belief, +serial, transitive and Euclidean, and a KTB frame reflexive and symmetric. An operator on +propositions is *indicial* when it is necessity along some accessibility relation. Montague's +necessity, true of a proposition true at every world, is the indicial operator of the universal +relation. Not every operator is indicial: Gallin's example is Scott's present progressive. + +## Main definitions + +* `ModalLogic.modalSquare`: the modal square of opposition along a relation. +* `ModalLogic.IsS5Frame`, `ModalLogic.IsKD45Frame`, `ModalLogic.IsK45Frame`, + `ModalLogic.IsKTBFrame`: the frames of the standard systems. +* `ModalLogic.IsIndicial`: necessity along some relation. + +## Implementation notes + +On propositions as sets, necessity along the transitive closure is mathlib's `SetRel.core_transGen`. ## References * [kratzer-1981] — necessity strengthened by restricting accessibility * [carnielli-pizzi-2008] — the modal square of opposition -* [gallin-1975] — the indicial operator hierarchy +* [gallin-1975] — indicial operators * [dowty-wall-peters-1981] — Montague's S5 operators -/ @@ -45,7 +63,8 @@ theorem compl_box_compl (R : SetRel W W) (p : W → Prop) : (□[R] pᶜ)ᶜ = funext w simp [not_box] -/-- The **modal square of opposition** over `R`: `A = □p`, `E = □¬p`, `I = ◇p`, `O = ¬□p`. -/ +/-- The modal square of opposition along `R`, with corners $\Box p$, $\Box \neg p$, $\Diamond p$ +and $\neg \Box p$. -/ def modalSquare (R : SetRel W W) (p : W → Prop) : Aristotelian.Square (W → Prop) where A := □[R] p E := □[R] pᶜ @@ -94,31 +113,26 @@ theorem box_transGen_iff {p : W → Prop} {w : W} : /-! ### Bundled frame classes -/ -/-- `R` is an **S5 frame** if it is reflexive and Euclidean. -/ +/-- `R` is an *S5 frame* when it is reflexive and Euclidean. -/ class IsS5Frame : Prop extends R.IsRefl, IsEuclidean R -/-- `R` is a **KD45 frame**, the doxastic frame, if it is serial, transitive, and Euclidean. -/ +/-- `R` is a *KD45 frame*, the frame of belief, when it is serial, transitive and Euclidean. -/ class IsKD45Frame : Prop extends IsSerial R, R.IsTrans, IsEuclidean R -/-- `R` is a **K45 frame** if it is transitive and Euclidean. -/ +/-- `R` is a *K45 frame* when it is transitive and Euclidean. -/ class IsK45Frame : Prop extends R.IsTrans, IsEuclidean R -/-- `R` is a **KTB frame** if it is reflexive and symmetric. -/ +/-- `R` is a *KTB frame* when it is reflexive and symmetric. -/ class IsKTBFrame : Prop extends R.IsRefl, R.IsSymm theorem diamond_box_iff [IsKD45Frame R] {p : W → Prop} {w : W} : ◇[R] (□[R] p) w ↔ □[R] p w := ⟨box_of_diamond_box, diamond_box_of_box⟩ -/-! ### The Gallin hierarchy - -Operators `(W → Prop) → W → Prop` form a three-level hierarchy ([gallin-1975]): arbitrary -operators, the **indicial** (Kripke-definable) ones, `□[R]` for some accessibility relation, -and S5, the indicial case `R = .univ`. Tense and other non-Kripke operators live outside -`IsIndicial`. -/ +/-! ### Indicial operators -/ -/-- An operator on world-propositions is **indicial** (Kripke-definable) if it is `□[R]` for -some accessibility relation `R`. -/ +/-- An operator on propositions is *indicial* when it is necessity along some accessibility +relation [gallin-1975]. -/ def IsIndicial (N : (W → Prop) → W → Prop) : Prop := ∃ R : SetRel W W, N = □[R] theorem box_isIndicial : IsIndicial □[R] := ⟨R, rfl⟩ diff --git a/Linglib/Logic/Modal/Defs.lean b/Linglib/Logic/Modal/Defs.lean index e0d4ffdb6e..89a734f1d2 100644 --- a/Linglib/Logic/Modal/Defs.lean +++ b/Linglib/Logic/Modal/Defs.lean @@ -4,35 +4,43 @@ public import Linglib.Core.Relation.SetRel public import Mathlib.Order.GaloisConnection.Basic /-! -# Modal operators and frame conditions - -This file defines the necessity and possibility operators of Kripke semantics along an -accessibility relation `R : SetRel W' W`, as operators on propositions `W → Prop`: `□[R] p w` -holds when `p` holds at every `R`-successor of `w`, and `◇[R] p w` when it holds at some. It proves -the axioms K, T, D, B, 4, 5 and Alt₁ over their frames, and that each axiom defines its frame -condition. +# Necessity and possibility in Kripke frames + +In Kripke semantics a proposition is *necessary* at a world when it is true at every world +accessible from it, and *possible* when it is true at some. The accessibility relation fixes the +kind of modality: for knowledge it relates a world to the worlds compatible with what is known +there, for obligation to the worlds where the obligations are met. Necessity distributes over +implication along every relation, which is axiom K, and the other axioms hold along relations with +a matching property: T, $\Box p \to p$, along reflexive relations; D, $\Box p \to \Diamond p$, +along serial ones; B, $p \to \Box \Diamond p$, along symmetric ones; 4, +$\Box p \to \Box \Box p$, along transitive ones; and 5, $\Diamond p \to \Box \Diamond p$, along +Euclidean ones. Each axiom holds along a relation +[exactly when the relation has its property](##box_T_iff). + +Possibility along a relation is +[left adjoint to necessity along the converse relation](##diamond_box_gc), which gives the +monotonicity and distribution laws, and necessity along a composite relation is +[nested necessity](##box_comp). Some laws hold at a world exactly when the world has few +successors. Excluded middle for necessity, $\Box p \lor \Box \neg p$ for every $p$, holds at a +world [exactly when it accesses at most one world](##box_or_box_not_at_iff), and Negation Swap, +$\Box \neg p \leftrightarrow \neg \Box p$, holds everywhere +[exactly when the relation is the graph of a function](##box_compl_eq_iff), along which necessity +is [precomposition](##box_graph). ## Main definitions -* `ModalLogic.Box`, `ModalLogic.Diamond`, with notation `□[R]` and `◇[R]`. +* `ModalLogic.Box`, `ModalLogic.Diamond`: necessity and possibility along a relation, with + notation `□[R]` and `◇[R]`. * `ModalLogic.IsSerial`, `ModalLogic.IsEuclidean`: the frame conditions of D and 5. -## Main statements - -* `ModalLogic.diamond_box_gc`: `◇` along `R` is left adjoint to `□` along its converse, which - gives monotonicity and the normality laws for a relation between any two types. -* `ModalLogic.box_T_iff` and siblings: each axiom defines its frame condition. -* `ModalLogic.box_comp`: necessity along a composite relation is nested necessity. -* `ModalLogic.box_not_iff_not_box_at_iff`, `ModalLogic.box_compl_eq_iff`, `ModalLogic.box_graph`: - Negation Swap, `□¬p ↔ ¬□p` for every `p`, holds iff the relation is the graph of a function, - along which necessity is precomposition. - ## Implementation notes -`□[R]` and `◇[R]` are mathlib's `SetRel.core` and `SetRel.preimage` read on predicates -(`box_iff_mem_core`, `diamond_iff_mem_preimage`), so propositions stated as sets use mathlib's -`SetRel.image_core_gc`, `SetRel.core_mono`, `SetRel.core_inter`, `SetRel.core_univ` and -`SetRel.preimage_union`. Reflexivity, symmetry and transitivity are mathlib's. +Necessity and possibility are operators on propositions `W → Prop` along a relation +`R : SetRel W' W`, which may relate two types. They are mathlib's `SetRel.core` and +`SetRel.preimage` read on predicates (`box_iff_mem_core`, `diamond_iff_mem_preimage`), so +propositions stated as sets use mathlib's `SetRel.image_core_gc`, `SetRel.core_mono`, +`SetRel.core_inter`, `SetRel.core_univ` and `SetRel.preimage_union`. Reflexivity, symmetry and +transitivity are mathlib's. ## References @@ -52,10 +60,10 @@ section Operators variable {W W' : Type*} (R : SetRel W' W) (p : W → Prop) (w : W') -/-- Necessity along `R` holds of `p` at `w` when `p` holds at every `R`-successor of `w`. -/ +/-- `p` is necessary at `w` along `R` when it holds at every world `w` accesses. -/ def Box : Prop := ∀ v, w ~[R] v → p v -/-- Possibility along `R` holds of `p` at `w` when `p` holds at some `R`-successor of `w`. -/ +/-- `p` is possible at `w` along `R` when it holds at some world `w` accesses. -/ def Diamond : Prop := ∃ v, w ~[R] v ∧ p v @[inherit_doc] scoped notation:max "□[" R "]" => Box R @@ -79,8 +87,8 @@ theorem diamond_iff_mem_preimage : ◇[R] p w ↔ w ∈ R.preimage {v | p v} := simp [Box, Diamond, not_and] variable (R) in -/-- Necessity distributes over conjunction ([hintikka-1962]'s -`a believes A and B ↔ a believes A and a believes B`). -/ +/-- Necessity distributes over conjunction. For belief this is [hintikka-1962]'s principle that +*a* believes *A and B* exactly when *a* believes *A* and *a* believes *B*. -/ theorem box_and (q : W → Prop) : □[R] (fun v ↦ p v ∧ q v) w ↔ □[R] p w ∧ □[R] q w := by simp only [Box, imp_and, forall_and] @@ -119,8 +127,9 @@ theorem diamond_sup : ◇[R] (p ⊔ q) = ◇[R] p ⊔ ◇[R] q := theorem box_top : □[R] ⊤ = ⊤ := by simpa using (diamond_box_gc R.inv).u_top -/-- Over any relation, `p ≤ □_{R⁻¹} ◇_R p`, which is Prior's tense axiom of conversion `A ⊃ G P A`. -This is the unit of the adjunction. -/ +/-- Along any relation $p$ entails $\Box_{R^{-1}} \Diamond_R p$, the unit of the adjunction. For +tense this is Prior's axiom of conversion $A \supset GPA$: what is the case will always have been +the case. -/ theorem le_box_inv_diamond (p : W → Prop) : p ≤ □[R.inv] (◇[R] p) := (diamond_box_gc R).le_u_l p @@ -137,11 +146,11 @@ theorem diamond_comp (S : SetRel W W) (p : W → Prop) : ◇[R ○ S] p = ◇[R] /-! ### Frame conditions -/ -/-- `R` is *serial* if every world accesses at least one world. -/ +/-- `R` is *serial* when every world accesses some world. -/ class IsSerial : Prop where serial : ∀ w, ∃ v, w ~[R] v -/-- `R` is *Euclidean* if any two `R`-successors of a world access each other. -/ +/-- `R` is *Euclidean* when any two worlds accessed from one world access each other. -/ class IsEuclidean : Prop where eucl : ∀ w v u, w ~[R] v → w ~[R] u → v ~[R] u @@ -181,8 +190,8 @@ theorem box_T [R.IsRefl] (h : □[R] p w) : p w := h w R.rfl theorem box_D [IsSerial R] (h : □[R] p w) : ◇[R] p w := let ⟨v, hwv⟩ := IsSerial.serial (R := R) w; ⟨v, hwv, h v hwv⟩ -/-- If some `R`-successor of `w` is also an `S`-successor, then `□[R] p` at `w` gives `◇[S] p` -at `w`; `box_D` is the case `S = R`. -/ +/-- If `w` accesses some world along both `R` and `S`, then necessity along `R` at `w` entails +possibility along `S`; `box_D` is the case `S = R`. -/ theorem diamond_of_box {S : SetRel W W} (h : ◇[R] (w ~[S] ·) w) (hp : □[R] p w) : ◇[S] p w := let ⟨v, hR, hS⟩ := h; ⟨v, hS, hp v hR⟩ diff --git a/Linglib/Logic/Modal/Epistemic.lean b/Linglib/Logic/Modal/Epistemic.lean index 7884aee2b5..c62e18a5ec 100644 --- a/Linglib/Logic/Modal/Epistemic.lean +++ b/Linglib/Logic/Modal/Epistemic.lean @@ -4,31 +4,36 @@ public import Linglib.Discourse.CommonGround public import Linglib.Logic.Modal.Basic /-! -# Multi-agent epistemic logic - -The group knowledge operators of [fagin-halpern-moses-vardi-1995] over agent-indexed -accessibility `Rs : E → SetRel W W` are boxes along lattice combinations of the agents' -relations: agent `i` knows `p` at `w` when `□[Rs i] p w`, everyone in `G` knows it when -`□[⋃ i ∈ G, Rs i] p w`, it is distributed knowledge when `□[⋂ i ∈ G, Rs i] p w`, and the -hierarchy `C_G ≤ E_G ≤ Kᵢ ≤ D_G` is antitonicity in the relation (`ModalLogic.box_restrict`). -Common knowledge is the box along the transitive closure of the union: `p` holds at every world -reachable by a chain of members' accessibility ([lederman-2014] Appendix 2.B's construction), -equivalently the infinite conjunction `E_G p ∧ E_G (E_G p) ∧ ⋯` -(`commonKnowledge_iff_forall_iterate`). Belief is the same operator over a KD45 frame -(`ModalLogic.IsKD45Frame`). +# Group knowledge + +In epistemic logic an agent *knows* a proposition at a world when the proposition is true at +every world the agent cannot tell apart from it. A group of agents gives rise to three further +notions. A proposition is known by *everyone* in the group when each member knows it; it is +*distributed knowledge* when it is true at every world that all the members consider possible, so +that it follows from what they know together; and it is *common knowledge* when everyone knows +it, everyone knows that everyone knows it, and so on without end. Each is necessity along a +relation built from the members' relations: their union for everyone's knowledge, their +intersection for distributed knowledge, and the transitive closure of their union for common +knowledge, which [is the infinite conjunction of iterated knowledge by +everyone](##commonKnowledge_iff_forall_iterate). Since necessity is antitone in the relation, common knowledge entails everyone's knowledge, +which entails each member's knowledge, which entails distributed knowledge. Belief is the same +operator along a KD45 frame. + +A common ground is *grounded in* common knowledge when the worlds it leaves open are exactly +those at which every proposition it accepts is common knowledge. ## Main definitions -* `ModalLogic.CommonKnowledge`: `C_G`. -* `Filter.GroundedIn`: a common ground whose context set is exactly what is common - knowledge ([stalnaker-2002]). +* `ModalLogic.CommonKnowledge`: common knowledge in a group. +* `Filter.GroundedIn`: a common ground grounded in common knowledge. ## References * [fagin-halpern-moses-vardi-1995] — group knowledge and its reachability semantics * [halpern-2003] — the same operators in the uncertainty setting * [fagin-halpern-1994] — the probabilistic extension, `Studies/FaginHalpern1994.lean` -* [hintikka-1962] — knowledge as `□` +* [hintikka-1962] — knowledge as necessity +* [lederman-2014] — common knowledge as reachability (UNVERIFIED: Appendix 2.B) * [stalnaker-2002] — common ground as common knowledge -/ @@ -41,8 +46,8 @@ open SetRel variable {W E : Type*} {Rs : E → SetRel W W} {i : E} {G : Set E} {p : W → Prop} {w : W} variable (Rs G) in -/-- Common knowledge among `G`: `p` holds at every world reachable from `w` by a chain of -members' accessibility. -/ +/-- `p` is common knowledge among `G` at `w` when it holds at every world reachable from `w` +by a chain of worlds each accessible to some member from the one before. -/ def CommonKnowledge (p : W → Prop) (w : W) : Prop := □[transGen (⋃ i ∈ G, Rs i)] p w theorem box_of_commonKnowledge (hi : i ∈ G) (h : CommonKnowledge Rs G p w) : □[Rs i] p w := @@ -61,9 +66,9 @@ namespace Filter variable {W E : Type*} -/-- A common ground `cg : Filter W` is grounded in common knowledge when its context set -`cg.ker` is exactly the set of worlds where each accepted proposition is common knowledge -among `G` ([stalnaker-2002]). -/ +/-- A common ground `cg` is grounded in common knowledge among `G` when its context set +`cg.ker` is exactly the set of worlds at which every proposition it accepts is common knowledge +[stalnaker-2002]. -/ def GroundedIn (cg : Filter W) (Rs : E → SetRel W W) (G : Set E) : Prop := ∀ w, w ∈ cg.ker ↔ ∀ p ∈ cg, ModalLogic.CommonKnowledge Rs G (· ∈ p) w diff --git a/Linglib/Logic/Modal/Extensional.lean b/Linglib/Logic/Modal/Extensional.lean index 8e42088edd..c1ea3e6fbf 100644 --- a/Linglib/Logic/Modal/Extensional.lean +++ b/Linglib/Logic/Modal/Extensional.lean @@ -1,114 +1,161 @@ module -public import Mathlib.Logic.Function.Basic +public import Mathlib.Logic.Function.DependsOn public import Linglib.Logic.Modal.Defs /-! # Extensional operators -An operator `O` on intensions `W → α` is *extensional at* `w` when its value at `w` depends on -its argument only through the argument's extension at `w`, i.e. `O · w` factors through -evaluation at `w`. Equivalently, `O` cannot tell an argument whose index it binds from the same -argument with the index fixed at `w`, which is why a situation pronoun bound under an extensional -operator reads as if it were free. The pointwise connectives are extensional, and extensionality -is closed under them and under composition; the Kripke box `ModalLogic.Box R` is extensional at -`w` only when `w` reaches no index but itself. +An operator on intensions is *extensional* at an index when the value it yields there depends only +on the extension of its argument at that index. Negation is extensional: whether *it is not +raining* is true at a world depends only on whether *it is raining* is true there. Necessity is +not, since whether *it must be raining* is true at a world depends on whether *it is raining* is +true at the worlds accessible from it. Among adjectives, which map properties to properties, +*gray* is extensional and *skillful* is not: where the cobblers are exactly the darts players, the +gray cobblers are the gray darts players, but the skillful cobblers need not be the skillful darts +players. + +An operator is extensional exactly when it is +[a function on extensions applied index by index](##isExtensional_iff_exists_eq_piMap). At an +index where it is extensional, an operator +[gives the same value on an intension and on the constant intension with the same +extension](##isExtensionalAt_iff_forall_const), and so +[cannot tell a variable it binds from one fixed at that index](##isExtensionalAt_iff_forall_diag): +a situation variable bound under negation reads as if it were free. The truth-functional +connectives are extensional, and so are composites of extensional operators. + +In general the value of an operator at an index depends on its argument at some set of indices, +and the operator is extensional there when that set can be taken to be the index alone. Necessity +in a Kripke frame depends at a world on +[exactly the worlds accessible from it](##dependsOn_box_iff), so it is +[extensional only at a world that accesses no world but itself](##isExtensionalAt_box_iff). ## Main definitions -* `IsExtensionalAt O w`, `IsExtensional O`: local truth-functionality of an operator. +* `ModalLogic.IsExtensionalAt O w`: the value of `O` at `w` depends only on the extension of its + argument at `w`. +* `ModalLogic.IsExtensional O`: `O` is extensional at every index. -## Main results +## Implementation notes -* `isExtensionalAt_iff_forall_diag`: extensionality as the failure to distinguish a bound index - from a fixed one. -* `isExtensionalAt_box_iff`: when the box is extensional. -* `IsExtensionalAt.and`, `IsExtensionalAt.or`, `IsExtensionalAt.not`, - `IsExtensionalAt.comp`: closure of extensional operators. +Extensionality at `w` is the statement that `O · w` factors through evaluation at `w`, and that it +depends, in the sense of mathlib's `DependsOn`, on the coordinate `w` alone. Kamp's condition for +an extensional adjective takes a single function on extensions for every index; the function here +may vary with the index, as in his gloss of the condition and as his claim that every predicative +adjective is extensional requires. + +## References + +* [kamp-1975] +* [zimmermann-2026] -/ @[expose] public section namespace ModalLogic -variable {W α β : Type*} +open Function + +variable {W α β γ δ : Type*} -/-- `O` is extensional at `w` when its value at `w` depends on the argument intension only -through the argument's extension at `w`, that is, when `O · w` factors through evaluation at -`w`. -/ +/-- `O` is extensional at `w` when its value at `w` depends on its argument only through the +argument's extension at `w`. -/ def IsExtensionalAt (O : (W → α) → W → β) (w : W) : Prop := - ∀ p q : W → α, p w = q w → O p w = O q w + ∀ ⦃p q : W → α⦄, p w = q w → O p w = O q w -/-- `O` is extensional at every index. -/ +/-- `O` is extensional when it is extensional at every index. -/ def IsExtensional (O : (W → α) → W → β) : Prop := ∀ w, IsExtensionalAt O w -theorem isExtensionalAt_iff_factorsThrough (O : (W → α) → W → β) (w : W) : - IsExtensionalAt O w ↔ Function.FactorsThrough (O · w) (· w) := - ⟨fun h _ _ hpq => h _ _ hpq, fun h _ _ hpq => h hpq⟩ - -theorem not_isExtensionalAt_iff_exists_witness {O : (W → α) → W → β} {w : W} : - ¬ IsExtensionalAt O w ↔ ∃ p q, p w = q w ∧ O p w ≠ O q w := by - simp only [IsExtensionalAt, not_forall, exists_prop] - -/-- An operator is extensional at `w` exactly when it cannot tell an argument whose index it -binds, `fun v ↦ g v v`, from the same argument with the index fixed at `w`, `g w`. -/ -theorem isExtensionalAt_iff_forall_diag {O : (W → α) → W → β} {w : W} : - IsExtensionalAt O w ↔ ∀ g : W → W → α, O (fun v ↦ g v v) w = O (g w) w := by - classical - refine ⟨fun h g ↦ h _ _ rfl, fun h p q hpq ↦ ?_⟩ - have h' := h fun u v ↦ if u = w then q v else p v - have e₁ : (fun v ↦ if v = w then q v else p v) = p := by - funext v - by_cases hv : v = w - · subst hv; simp [hpq] - · simp [hv] - have e₂ : (fun v ↦ if w = w then q v else p v) = q := by simp - rwa [e₁, e₂] at h' +variable {O : (W → α) → W → β} {w : W} + +theorem isExtensionalAt_iff_factorsThrough : + IsExtensionalAt O w ↔ FactorsThrough (O · w) (· w) := + .rfl + +theorem isExtensionalAt_iff_dependsOn : IsExtensionalAt O w ↔ DependsOn (O · w) {w} := by + simp [IsExtensionalAt, DependsOn] + +theorem not_isExtensionalAt_iff : ¬ IsExtensionalAt O w ↔ ∃ p q, p w = q w ∧ O p w ≠ O q w := by + simp [IsExtensionalAt] + +/-- An operator is extensional at `w` exactly when it does not distinguish its argument from the +constant intension with the same extension at `w`. -/ +theorem isExtensionalAt_iff_forall_const : + IsExtensionalAt O w ↔ ∀ p, O p w = O (fun _ ↦ p w) w := + ⟨fun h _ ↦ h rfl, fun h p q hpq ↦ by rw [h p, h q, hpq]⟩ + +theorem isExtensionalAt_iff_exists : IsExtensionalAt O w ↔ ∃ f : α → β, ∀ p, O p w = f (p w) := + ⟨fun h ↦ ⟨fun a ↦ O (fun _ ↦ a) w, fun _ ↦ h rfl⟩, fun ⟨f, hf⟩ p q hpq ↦ by rw [hf, hf, hpq]⟩ + +/-- An operator is extensional exactly when it applies a function on extensions at each index. -/ +theorem isExtensional_iff_exists_eq_piMap : IsExtensional O ↔ ∃ f : W → α → β, O = Pi.map f := + ⟨fun h ↦ ⟨fun w a ↦ O (fun _ ↦ a) w, funext₂ fun _ w ↦ h w rfl⟩, + fun ⟨f, hf⟩ w _ _ hpq ↦ hf ▸ congrArg (f w) hpq⟩ + +theorem isExtensional_piMap (f : W → α → β) : IsExtensional (Pi.map f) := + isExtensional_iff_exists_eq_piMap.2 ⟨f, rfl⟩ + +/-- An operator is extensional at `w` exactly when it does not distinguish an argument whose index +it binds, `fun v ↦ g v v`, from the same argument with the index fixed at `w`, `g w`. -/ +theorem isExtensionalAt_iff_forall_diag : + IsExtensionalAt O w ↔ ∀ g : W → W → α, O (fun v ↦ g v v) w = O (g w) w := + ⟨fun h _ ↦ h rfl, fun h ↦ isExtensionalAt_iff_forall_const.2 fun p ↦ h fun u _ ↦ p u⟩ + +/-! ### The box -/ open SetRel in -/-- The box along `R` is extensional at `w` exactly when `w` reaches no index but itself. -/ -theorem isExtensionalAt_box_iff {R : SetRel W W} {w : W} : - IsExtensionalAt (Box R) w ↔ ∀ v, w ~[R] v → v = w := by - refine ⟨fun h v hv ↦ ?_, fun h p q hpq ↦ propext ⟨fun hp v hv ↦ ?_, fun hq v hv ↦ ?_⟩⟩ - · have := h (fun _ ↦ True) (· = w) (eq_true rfl).symm - exact (this ▸ fun _ _ ↦ trivial : Box R (· = w) w) v hv - · obtain rfl := h v hv - exact hpq ▸ hp v hv - · obtain rfl := h v hv - exact hpq ▸ hq v hv +/-- The value of the box along `R` at `w` depends on a set of indices exactly when the set +contains every `R`-successor of `w`. -/ +theorem dependsOn_box_iff {W' : Type*} {R : SetRel W' W} {w : W'} {s : Set W} : + DependsOn (□[R] · w) s ↔ {v | w ~[R] v} ⊆ s := by + refine ⟨fun h v hv ↦ by_contra fun hvs ↦ ?_, fun h p q hpq ↦ + propext <| forall₂_congr fun v hv ↦ iff_of_eq (hpq v (h hv))⟩ + have := @h (· ≠ v) (fun _ ↦ True) fun u hu ↦ eq_true (ne_of_mem_of_not_mem hu hvs) + exact this.mpr (fun _ _ ↦ trivial) v hv rfl -namespace IsExtensionalAt +open SetRel in +theorem isExtensionalAt_box_iff {R : SetRel W W} : + IsExtensionalAt □[R] w ↔ ∀ v, w ~[R] v → v = w := by + rw [isExtensionalAt_iff_dependsOn, dependsOn_box_iff, Set.subset_singleton_iff] + rfl -variable {w : W} +/-! ### Closure -/ -theorem eval : IsExtensionalAt (fun (p : W → α) w' => p w') w := - fun _ _ hpq => hpq +theorem isExtensionalAt_id : IsExtensionalAt (id : (W → α) → W → α) w := + fun _ _ ↦ id -theorem const (P : W → Prop) : IsExtensionalAt (fun (_ : W → α) w' => P w') w := - fun _ _ _ => rfl +theorem isExtensionalAt_const (c : W → β) : IsExtensionalAt (fun _ : W → α ↦ c) w := + fun _ _ _ ↦ rfl -/-- Pointwise negation is extensional, since negation is not an intensional operator. -/ -theorem neg : IsExtensionalAt (fun p (w' : W) => ¬ p w') w := - fun _ _ hpq => congrArg Not hpq +theorem isExtensionalAt_not : IsExtensionalAt (fun (p : W → Prop) v ↦ ¬ p v) w := + fun _ _ ↦ congrArg Not -theorem and {O₁ O₂ : (W → α) → W → Prop} (h₁ : IsExtensionalAt O₁ w) - (h₂ : IsExtensionalAt O₂ w) : IsExtensionalAt (fun p w' => O₁ p w' ∧ O₂ p w') w := - fun p q hpq => congrArg₂ And (h₁ p q hpq) (h₂ p q hpq) +namespace IsExtensionalAt -theorem or {O₁ O₂ : (W → α) → W → Prop} (h₁ : IsExtensionalAt O₁ w) - (h₂ : IsExtensionalAt O₂ w) : IsExtensionalAt (fun p w' => O₁ p w' ∨ O₂ p w') w := - fun p q hpq => congrArg₂ Or (h₁ p q hpq) (h₂ p q hpq) +theorem comp {O' : (W → β) → W → γ} (h' : IsExtensionalAt O' w) (h : IsExtensionalAt O w) : + IsExtensionalAt (O' ∘ O) w := + fun _ _ hpq ↦ h' (h hpq) + +theorem comp_left (h : IsExtensionalAt O w) (g : β → γ) : + IsExtensionalAt (fun p v ↦ g (O p v)) w := + fun _ _ hpq ↦ congrArg g (h hpq) + +theorem comp₂ {O' : (W → α) → W → γ} (h : IsExtensionalAt O w) (h' : IsExtensionalAt O' w) + (g : β → γ → δ) : IsExtensionalAt (fun p v ↦ g (O p v) (O' p v)) w := + fun _ _ hpq ↦ congrArg₂ g (h hpq) (h' hpq) theorem not {O : (W → α) → W → Prop} (h : IsExtensionalAt O w) : - IsExtensionalAt (fun p w' => ¬ O p w') w := - fun p q hpq => congrArg Not (h p q hpq) - -/-- Extensional operators compose, so scope-inertness lifts through a stack of them. -/ -theorem comp {O₁ : (W → α) → W → β} {O₂ : (W → β) → W → Prop} - (h₂ : IsExtensionalAt O₂ w) (h₁ : IsExtensionalAt O₁ w) : - IsExtensionalAt (fun p w' => O₂ (fun s => O₁ p s) w') w := - fun p q hpq => h₂ _ _ (h₁ p q hpq) + IsExtensionalAt (fun p v ↦ ¬ O p v) w := + h.comp_left Not + +theorem and {O O' : (W → α) → W → Prop} (h : IsExtensionalAt O w) (h' : IsExtensionalAt O' w) : + IsExtensionalAt (fun p v ↦ O p v ∧ O' p v) w := + h.comp₂ h' And + +theorem or {O O' : (W → α) → W → Prop} (h : IsExtensionalAt O w) (h' : IsExtensionalAt O' w) : + IsExtensionalAt (fun p v ↦ O p v ∨ O' p v) w := + h.comp₂ h' Or end IsExtensionalAt diff --git a/Linglib/Logic/Modal/FirstOrder/Correspondence.lean b/Linglib/Logic/Modal/FirstOrder/Correspondence.lean index 2b004a6330..8a615f71aa 100644 --- a/Linglib/Logic/Modal/FirstOrder/Correspondence.lean +++ b/Linglib/Logic/Modal/FirstOrder/Correspondence.lean @@ -4,29 +4,33 @@ public import Linglib.Core.ModelTheory.Binders public import Linglib.Logic.Modal.FirstOrder.Semantics /-! -# The correspondence language and the standard translation - -The standard translation of quantified modal logic into first-order logic, -for an arbitrary signature: modal formulas over `L` translate into plain -mathlib first-order formulas over the correspondence language -`L.correspondence` — every symbol world-relativized to one arity higher, -plus a binary accessibility relation and an individual-sort predicate — -interpreted on the two-sorted-as-one carrier `W ⊕ M`. `realize_st` is -satisfaction preservation. - -## Main declarations - -* `Language.correspondence` — the correspondence language of `L`; - `ModalStructure.correspondence` — the `W ⊕ M` encoding of a modal - structure as one mathlib structure. -* `ModalFormula.st` — the standard translation, total: the current world is - the free variable `Sum.inr k`, and `box` introduces the fresh world - variable `Sum.inr (k + 1)`. -* `realize_st` — satisfaction preservation: Kripke satisfaction at `w` is - first-order realization over `correspondence` at any sorted valuation - pinning `Sum.inr k` to `w`. -* `stClose` — sort-guarded existential closure of the current-world - variable, turning translations into sentence candidates. +# The standard translation + +The *standard translation* rewrites a modal formula as a first-order formula about worlds and +individuals, so that results about first-order logic apply to modal logic. A formula over a +signature `L` becomes a formula over the *correspondence language* of `L`, which has, for each +symbol of `L`, a symbol taking a world as an extra first argument, together with a binary +accessibility relation and a predicate true of individuals. Necessity becomes universal +quantification over the accessible worlds, and the quantifiers range over individuals. A Kripke +model becomes a single first-order structure whose domain contains both its worlds and its +individuals, and the translation [preserves satisfaction](##realize_st): a modal formula holds at +a world exactly when its translation holds with the current-world variable assigned that world. + +## Main definitions + +* `FirstOrder.Language.correspondence`: the correspondence language of a signature. +* `FirstOrder.Language.ModalStructure.correspondence`: a Kripke model as one first-order + structure on its worlds and individuals. +* `FirstOrder.Language.ModalFormula.st`: the standard translation. +* `FirstOrder.Language.stClose`: the existential closure of the current-world variable over + worlds. + +## Implementation notes + +World variables are numbered: the current world is the variable `Sum.inr k`, and necessity +quantifies the fresh variable `Sum.inr (k + 1)`. Worlds and individuals share the carrier +`W ⊕ M`, sorted by the predicate true of individuals; an atom applied to arguments of the wrong +sort is false, and a function symbol applied to them takes a default value. ## References @@ -41,9 +45,9 @@ variable {W M Var : Type*} /-! ### The correspondence language -/ -/-- The correspondence language of `L` has an `(n + 1)`-ary symbol for - each `n`-ary `L`-symbol — the new first argument the world — together - with an individual-sort predicate and an accessibility relation. -/ +/-- The correspondence language of `L`: an `(n + 1)`-ary symbol for each `n`-ary symbol of `L`, +whose first argument is a world, together with a predicate true of individuals and an +accessibility relation. -/ def correspondence (L : Language) : Language where Functions := fun n ↦ match n with | 0 => PEmpty @@ -58,7 +62,7 @@ abbrev corrFunc (f : L.Functions n) : L.correspondence.Functions (n + 1) := f abbrev corrRel (R : L.Relations n) : L.correspondence.Relations (n + 1) := Sum.inl R -/-- The individual-sort predicate. -/ +/-- The predicate true of individuals. -/ abbrev corrIndiv : L.correspondence.Relations 1 := Sum.inr PUnit.unit /-- The accessibility relation symbol. -/ @@ -70,8 +74,8 @@ abbrev corrWorldVar (k : ℕ) : L.correspondence.Term (Var ⊕ ℕ) := Term.var /-! ### Sorted valuations -/ -/-- The sorted valuation of an individual assignment `v` and a world - assignment `u`. `realize_st` evaluates translations at these. -/ +/-- The assignment to individual and world variables given by an assignment `v` of +individuals and an assignment `u` of worlds. -/ def stVal (v : Var → M) (u : ℕ → W) : Var ⊕ ℕ → W ⊕ M := Sum.elim (Sum.inr ∘ v) (Sum.inl ∘ u) @@ -93,18 +97,17 @@ theorem stVal_update_world [DecidableEq Var] (v : Var → M) (u : ℕ → W) (j /-! ### The translation -/ -/-- `stTerm` translates terms: a variable stays put; a function symbol - applies its world-relativized form at the current world variable. -/ +/-- The translation of terms: a variable is unchanged, and a function symbol takes the current +world as its first argument. -/ def stTerm (k : ℕ) : L.Term Var → L.correspondence.Term (Var ⊕ ℕ) | .var x => corrIndivVar x | .func f args => Term.func (corrFunc f) (Fin.cons (corrWorldVar k) fun i ↦ stTerm k (args i)) -/-- The standard translation `ST_k` of [blackburn-derijke-venema-2001]. - The current world is the free variable `Sum.inr k`; atoms - world-relativize; `box` relativizes a fresh world variable - `Sum.inr (k + 1)` along accessibility; quantifiers relativize to the - individual sort. -/ +/-- The standard translation $ST_k$ [blackburn-derijke-venema-2001], with the current world +the variable `Sum.inr k`. Atoms take the current world as their first argument, necessity +quantifies the variable `Sum.inr (k + 1)` over the worlds accessible from the current one, and +the quantifiers range over individuals. -/ def ModalFormula.st [DecidableEq Var] (k : ℕ) : ModalFormula L Var → L.correspondence.Formula (Var ⊕ ℕ) | .equal t₁ t₂ => Term.equal (stTerm k t₁) (stTerm k t₂) @@ -119,10 +122,10 @@ def ModalFormula.st [DecidableEq Var] (k : ℕ) : /-! ### Sort-guarded sentence closure -/ -/-- `stClose` closes the current-world variable `Sum.inr k` under a - sort-guarded existential, `∃z(¬IsIndiv(z) ∧ ψ)`. The guard is - load-bearing on the mixed carrier — a bare `ex₁` could be witnessed by - a junk individual-as-world, which satisfies `□⊥` vacuously. -/ +/-- The existential closure of the current-world variable `Sum.inr k` over worlds, +$\exists z \, (\neg \mathrm{Indiv}(z) \land \psi)$. Without the restriction to worlds an +individual could witness the quantifier, and an individual accesses no world, so it satisfies +$\Box \bot$. -/ def stClose [DecidableEq Var] (k : ℕ) (ψ : L.correspondence.Formula (Var ⊕ ℕ)) : L.correspondence.Formula (Var ⊕ ℕ) := Formula.ex₁ (Sum.inr k) @@ -140,11 +143,9 @@ theorem realize_stClose [DecidableEq Var] [L.correspondence.Structure (W ⊕ M)] variable [Inhabited M] (K : ModalStructure L W M) -/-- `K.correspondence` encodes a modal structure as a single mathlib - structure on `W ⊕ M` — the structure half of `Language.correspondence`: - worlds and individuals share the carrier, sorted by `corrIndiv`; - relational guards make all off-sort atoms false, and off-sort function - arguments default. -/ +/-- A Kripke model as one structure for the correspondence language on its worlds and +individuals. An atom applied to arguments of the wrong sort is false, and a function symbol +applied to them takes a default value. -/ @[instance_reducible] def ModalStructure.correspondence : L.correspondence.Structure (W ⊕ M) where funMap := fun {n} f z ↦ match n, f with @@ -207,10 +208,9 @@ private theorem realize_stTerm {k : ℕ} {v : Var → M} {u : ℕ → W} : (fun i ↦ by simpa [Fin.cons_succ] using realize_stTerm (args i))] rfl -/-- The standard translation preserves satisfaction. Kripke satisfaction at the world pinned at - index `k` is first-order realization over `K.correspondence` at the sorted valuation. Off-sort - quantifier instances are discharged by the relational guards, and `box`'s fresh world variable - `k + 1` leaves index `k` untouched. -/ +/-- The standard translation preserves satisfaction: a modal formula holds at a world exactly +when its translation holds in the model's first-order structure with the current-world variable +assigned that world. -/ theorem realize_st [DecidableEq Var] {φ : ModalFormula L Var} {k : ℕ} {v : Var → M} {u : ℕ → W} : φ.Realize K (u k) v ↔ diff --git a/Linglib/Logic/Modal/FirstOrder/Semantics.lean b/Linglib/Logic/Modal/FirstOrder/Semantics.lean index 1f326548ea..3d3027ff02 100644 --- a/Linglib/Logic/Modal/FirstOrder/Semantics.lean +++ b/Linglib/Logic/Modal/FirstOrder/Semantics.lean @@ -6,35 +6,34 @@ public import Linglib.Logic.Modal.FirstOrder.Syntax /-! # Constant-domain Kripke semantics -`[UPSTREAM]` candidates for `Mathlib/ModelTheory`, which is classical: one -structure, no accessibility. A `ModalStructure L W M` — the modal analogue -of `L.Structure` — is a `W`-indexed family of `L`-structures on a constant -domain `M` together with `Finset`-valued accessibility; `ModalFormula L α` is the quantified modal -language in `BoundedFormula`'s basis, and `ModalFormula.Realize` is -Kripke satisfaction `K, w ⊨_v φ`. +A Kripke model for quantified modal logic has a set of worlds, an accessibility relation between +them, and at each world a first-order structure. In a *constant-domain* model every world has +the same domain of individuals, and only the interpretation of the symbols varies from world to +world. A formula is satisfied at a world under an assignment of individuals to its free +variables: atomic formulas are evaluated in the world's structure, necessity quantifies over the +accessible worlds, and the quantifiers range over the common domain. Because the domain does not +vary, the [Barcan formula](##realize_barcan) $\forall x \, \Box \varphi \to \Box \forall x \, +\varphi$ and [its converse](##realize_converseBarcan) hold in every model. -## Main declarations +## Main definitions -* `ModalStructure` — accessibility plus a world-indexed family of - first-order structures on a constant domain, so that terms and plain formulas - realize at a world by `Term.realizeAt` and `Formula.RealizeAt`. -* `ModalFormula.Realize` — Kripke satisfaction for the modal language of - `Syntax.lean`, with the `realize_*` simp set and the Barcan laws. +* `FirstOrder.Language.ModalStructure`: a constant-domain Kripke model. +* `FirstOrder.Language.ModalFormula.Realize`: satisfaction of a modal formula at a world. ## Implementation notes -* Accessibility is `Finset`-valued (computability-first, matching the - team-semantics consumers); generalize to a `Prop`-valued relation when a - consumer needs infinite branching. -* `ModalFormula` quantifiers bind **named** variables with - `Function.update` semantics (the `Formula.all₁` / `ex₁` convention of - `Core/ModelTheory/Binders.lean`), not de Bruijn indices: the modal - layer's consumers carry named variables. +* `[UPSTREAM]` candidate for mathlib's `ModelTheory`, whose semantics has one structure and no + accessibility relation. +* Accessibility is `Finset`-valued, for computation, as the team-semantics consumers require; it + can be generalized to a `Prop`-valued relation when a consumer needs infinite branching. +* Quantifiers bind named variables and update the assignment with `Function.update`, as + `Formula.all₁` and `Formula.ex₁` of `Core/ModelTheory/Binders.lean` do, rather than de Bruijn + indices, since the consumers carry named variables. ## References -* [fitting-mendelsohn-2023] — constant-domain models, world-relative - interpretation, the Barcan formulas +* [fitting-mendelsohn-2023] — constant-domain models, world-relative interpretation, the Barcan + formulas -/ @[expose] public section @@ -43,13 +42,12 @@ namespace FirstOrder.Language variable {L : Language} {W M α : Type*} -/-- A structure for the quantified modal language — the model object of - constant-domain Kripke semantics: `Finset`-valued accessibility plus a - `W`-indexed family of `L`-structures on the domain `M`. -/ +/-- A constant-domain Kripke model: an accessibility relation on the worlds `W` and, at each +world, an `L`-structure on the domain `M`. -/ structure ModalStructure (L : Language) (W M : Type*) where - /-- Accessibility relation (per-world set of accessible worlds). -/ + /-- The worlds accessible from each world. -/ access : W → Finset W - /-- World-indexed interpretation of the signature. -/ + /-- The structure at each world. -/ interp : W → L.Structure M namespace ModalStructure @@ -95,8 +93,7 @@ namespace ModalFormula variable [DecidableEq α] -/-- Kripke satisfaction `K, w ⊨_v φ`, under which atoms evaluate at the world's structure, - `□` quantifies over accessible worlds, and named quantifiers update the valuation. -/ +/-- Satisfaction of a modal formula at a world under an assignment, $K, w \vDash_v \varphi$. -/ def Realize (K : ModalStructure L W M) : W → ModalFormula L α → (α → M) → Prop | w, .equal t₁ t₂, v => t₁.realizeAt K.interp w v = t₂.realizeAt K.interp w v @@ -167,8 +164,7 @@ variable (K : ModalStructure L W M) (w : W) (v : α → M) /-! ### The Barcan laws -Constant domains validate the Barcan formula and its converse: `□` and `∀` -are both world-independent universal quantifiers, so they commute. -/ +In a constant-domain model necessity and universal quantification commute. -/ theorem realize_barcan (x : α) (φ : ModalFormula L α) : (all x (box φ)).Realize K w v → (box (all x φ)).Realize K w v := diff --git a/Linglib/Logic/Modal/FirstOrder/Syntax.lean b/Linglib/Logic/Modal/FirstOrder/Syntax.lean index d57ed2adda..bfb5de9ee8 100644 --- a/Linglib/Logic/Modal/FirstOrder/Syntax.lean +++ b/Linglib/Logic/Modal/FirstOrder/Syntax.lean @@ -5,11 +5,24 @@ public import Mathlib.ModelTheory.Syntax /-! # The quantified modal language -`ModalFormula L α`: modal formulas over `L` with named free variables `α`, -in mathlib's `BoundedFormula` basis — atomic `equal`/`rel`, `falsum`, -`imp` — plus `□` and named universal quantification, with `∼`, `⊤`, `⊓`, -`⊔`, `ex`, and `diamond` derived exactly as for `BoundedFormula`. -`[UPSTREAM]` candidate for `Mathlib/ModelTheory`. +Quantified modal logic adds a necessity operator to first-order logic. Its formulas over a +signature `L`, with free variables in `α`, are built as mathlib's first-order formulas are, from +equations between terms, relation symbols applied to terms, falsity and implication, together +with necessity and universal quantification over a named variable. Negation, the other +connectives, existential quantification and possibility are defined from these exactly as for +first-order formulas. + +## Main definitions + +* `FirstOrder.Language.ModalFormula L α`: the formulas of quantified modal logic. + +## Implementation notes + +`[UPSTREAM]` candidate for mathlib's `ModelTheory`. + +## References + +* [fitting-mendelsohn-2023] -/ @[expose] public section @@ -18,10 +31,7 @@ namespace FirstOrder.Language variable {L : Language} {α : Type*} -/-- Modal formulas over `L` with named free variables `α`: mathlib's - `BoundedFormula` basis — atomic `equal`/`rel`, `falsum`, `imp` — plus - `□` and named quantification; `∼`, `⊤`, `⊓`, `⊔`, `ex`, and `diamond` are - derived exactly as for `BoundedFormula`. -/ +/-- A formula of quantified modal logic over `L` with free variables in `α`. -/ inductive ModalFormula (L : Language) (α : Type*) where /-- The proposition that two terms are equal. -/ | equal (t₁ t₂ : L.Term α) : ModalFormula L α @@ -52,12 +62,12 @@ instance : Min (ModalFormula L α) := ⟨fun φ ψ => (φ.imp ψ.not).not⟩ instance : Max (ModalFormula L α) := ⟨fun φ ψ => φ.not.imp ψ⟩ -/-- Existential quantification of a named variable, derived: `∃x := ∼∀x∼`. -/ +/-- Existential quantification of a named variable, defined as $\neg \forall x \neg$. -/ @[match_pattern] protected def ex (x : α) (φ : ModalFormula L α) : ModalFormula L α := (all x φ.not).not -/-- Possibility, derived: `◇φ := ∼□∼φ` — to `box` what `ex` is to `all`. -/ +/-- Possibility, defined as $\neg \Box \neg$. -/ @[match_pattern] def diamond (φ : ModalFormula L α) : ModalFormula L α := (box φ.not).not diff --git a/Linglib/Semantics/Modification/Classification.lean b/Linglib/Semantics/Modification/Classification.lean index 4969b88f9e..6425d6e04b 100644 --- a/Linglib/Semantics/Modification/Classification.lean +++ b/Linglib/Semantics/Modification/Classification.lean @@ -62,10 +62,8 @@ theorem isPrivative_iff_forall : /-- Intersective modifiers are extensional, since the meet with a fixed property reads the noun only through its extension at each world. -/ -theorem IsIntersective.isExtensional (h : IsIntersective adj) : ModalLogic.IsExtensional adj := by - obtain ⟨Q, hQ⟩ := h - intro w N₁ N₂ hN - simp only [hQ, Pi.inf_apply, hN] +theorem IsIntersective.isExtensional (h : IsIntersective adj) : ModalLogic.IsExtensional adj := + h.elim fun Q hQ ↦ ModalLogic.isExtensional_iff_exists_eq_piMap.2 ⟨fun w ↦ (Q w ⊓ ·), funext hQ⟩ /-- A privative modifier that holds of something is not subsective. -/ theorem IsPrivative.not_isSubsective (hp : IsPrivative adj) (hne : ∃ N w x, adj N w x) : diff --git a/Linglib/Semantics/Reference/Rigidity.lean b/Linglib/Semantics/Reference/Rigidity.lean index 696068de35..f080accadc 100644 --- a/Linglib/Semantics/Reference/Rigidity.lean +++ b/Linglib/Semantics/Reference/Rigidity.lean @@ -7,6 +7,7 @@ module public import Mathlib.Logic.Function.Basic public import Mathlib.Data.Set.Image +public import Linglib.Logic.Modal.Extensional /-! # Rigid designation @@ -21,8 +22,9 @@ of identity. An operator `O` governing the predication of `P` of a designator `f` has a large scope reading, which evaluates `f` at the index of the whole sentence, and a small scope reading, which evaluates it at each index the operator reaches. The large scope reading of `f` is the small -scope reading of the designator whose reference `f` fixes at that index, so the two readings -coincide for a rigid designator. +scope reading of the designator whose reference `f` fixes at that index. The two readings +coincide when `f` is constant on the indices on which the operator's value depends: under every +operator when `f` is rigid, and for every designator when the operator is extensional. ## Main definitions @@ -35,7 +37,11 @@ coincide for a rigid designator. * `isRigid_iff_subsingleton_range`: the mathlib face. * `IsRigid.eq_of_apply_eq`: the necessity of identity. * `largeScope_eq_smallScope_const`: the large scope reading as fixing the reference. +* `largeScope_eq_smallScope_of_dependsOn`: the scope readings coincide for a designator constant + on the indices the operator reads. * `largeScope_eq_smallScope`: the scope readings coincide for a rigid designator. +* `ModalLogic.IsExtensionalAt.largeScope_eq_smallScope`: the scope readings coincide under an + extensional operator. ## References @@ -97,6 +103,20 @@ theorem largeScope_eq_smallScope_const (O : (W → Prop) → W → Prop) (P : τ (f : W → τ) (w : W) : largeScope O P f w = smallScope O P (fun _ ↦ f w) w := rfl +/-- The two scope readings of `f` coincide at `w` when `f` is constant on a set of indices on +which the operator's value at `w` depends. -/ +theorem largeScope_eq_smallScope_of_dependsOn {O : (W → Prop) → W → Prop} {s : Set W} {w : W} + (hO : DependsOn (O · w) s) (hf : Set.EqOn f (fun _ ↦ f w) s) (P : τ → W → Prop) : + largeScope O P f w = smallScope O P f w := + hO fun v hv ↦ congrArg (P · v) (hf hv).symm + theorem largeScope_eq_smallScope (h : IsRigid f) (O : (W → Prop) → W → Prop) (P : τ → W → Prop) : largeScope O P f = smallScope O P f := - funext fun w ↦ (congrArg (smallScope O P · w) (h.eq_const w)).symm + funext fun w ↦ largeScope_eq_smallScope_of_dependsOn (dependsOn_univ _) (fun v _ ↦ h v w) P + +/-- The two scope readings of every designator coincide under an operator extensional at `w`. -/ +theorem ModalLogic.IsExtensionalAt.largeScope_eq_smallScope {O : (W → Prop) → W → Prop} {w : W} + (h : ModalLogic.IsExtensionalAt O w) (P : τ → W → Prop) (f : W → τ) : + largeScope O P f w = smallScope O P f w := + largeScope_eq_smallScope_of_dependsOn (ModalLogic.isExtensionalAt_iff_dependsOn.1 h) + (Set.eqOn_singleton.2 rfl) P diff --git a/Studies/Kamp1975.lean b/Studies/Kamp1975.lean index 63a4f04a81..c4eafa2252 100644 --- a/Studies/Kamp1975.lean +++ b/Studies/Kamp1975.lean @@ -28,6 +28,14 @@ two agree. Before this, Kamp argues that no many-valued logic handles borderline asymmetric, and the witness shows the incomparability and the forced verdict, not the paper's specific outcome. +## Errata + +* Definition (7) asks for a single function $F'$ on extensions with $F(P)(w) = F'(P(w))$ at + every world, while the gloss after it and the claim that every predicative adjective is + extensional need $F'$ to vary with the world. A predicative adjective whose property differs + between worlds, such as `grayAdj`, satisfies (4) and the gloss but not (7) as printed. The + study reads (7) by its gloss, `ModalLogic.IsExtensional`. + ## References * [kamp-1975] @@ -224,35 +232,38 @@ inductive W2 | w₁ | w₂ /-- Three entities suffice for all witness constructions. -/ inductive E3 | a | b | c --- UNVERIFIED: Kamp's definition numbers (4)–(6) below; the paper is not available to check. - -/-- *gray* is predicative, Kamp's definition (4), since it conjoins a fixed property with the -noun, so *gray cat* entails both *gray* and *cat*. -/ -def grayAdj : Modifier (W2 → E3 → Prop) := fun N w x ↦ - (match x with | .a => True | _ => False) ∧ N w x +/-- *gray* is predicative, Kamp's definition (4) (p. 124), since it conjoins a property with the +noun, so *gray cat* entails both *gray* and *cat*. Only `a` is gray, and only at `w₁`. -/ +def grayAdj : Modifier (W2 → E3 → Prop) := fun N w x ↦ (w = .w₁ ∧ x = .a) ∧ N w x -/-- Each class has a member, and extensionality is independent of subsectivity. -/ theorem gray_intersective : IsIntersective grayAdj := - Modifier.isIntersective_iff_exists_forall.mpr - ⟨fun _ x ↦ match x with | .a => True | _ => False, - fun N w x ↦ by cases x <;> simp [grayAdj]⟩ + ⟨fun w x ↦ w = .w₁ ∧ x = .a, fun _ ↦ rfl⟩ /-- *gray* is therefore also extensional and subsective. -/ example : ModalLogic.IsExtensional grayAdj := Modifier.IsIntersective.isExtensional gray_intersective example : IsSubsective grayAdj := gray_intersective.isSubsective -/-- *fake* is privative, Kamp's definition (5), so *fake gun* entails *not a gun*. Kamp doubts -that any English adjective is privative "in all of its possible uses". -/ +/-- No single function on extensions gives *gray*, so the predicative *gray* is not extensional by +(7) as printed (p. 125). -/ +theorem not_exists_forall_grayAdj_eq : + ¬ ∃ F' : (E3 → Prop) → E3 → Prop, ∀ N w, grayAdj N w = F' (N w) := by + rintro ⟨F', hF'⟩ + have h := (congrFun (hF' (fun _ _ ↦ True) .w₁) .a).trans + (congrFun (hF' (fun _ _ ↦ True) .w₂) .a).symm + simp [grayAdj] at h + +/-- *fake* is privative, Kamp's definition (5) (p. 125), so *fake gun* entails *not a gun*. Kamp +doubts that any English adjective is privative "in all of its possible uses". -/ def fakeAdj : Modifier (W2 → E3 → Prop) := fun N w x ↦ (match x with | .b => True | _ => False) ∧ ¬ N w x theorem fake_privative : IsPrivative fakeAdj := Modifier.isPrivative_iff_forall.mpr fun _ _ _ h ↦ h.2 -/-- *skillful* is affirmative, Kamp's definition (6), but not extensional. A skillful surgeon -is a surgeon, yet skill depends on the noun's intension and not just its current extension, as -in the case of cobblers and darts players that Kamp credits to Lewis. -/ +/-- *skillful* is affirmative, Kamp's definition (6) (p. 125), but not extensional (7). A +skillful surgeon is a surgeon, yet skill depends on the noun's intension and not just its current +extension, as in the case of cobblers and darts players that Kamp credits to Lewis. -/ def skillfulAdj : Modifier (W2 → E3 → Prop) := fun N w x ↦ N w x ∧ match x with | .a => N .w₁ .a -- a's skill assessment depends on N's intension @@ -269,12 +280,12 @@ theorem skillful_not_extensional : ¬ ModalLogic.IsExtensional skillfulAdj := by | _, _ => True have hagree : N₁ .w₂ = N₂ .w₂ := by funext x; cases x <;> simp [N₁, N₂] - have h := hext .w₂ N₁ N₂ hagree + have h := hext .w₂ hagree have hLHS : skillfulAdj N₁ .w₂ .a := ⟨trivial, trivial⟩ exact (congrFun h .a ▸ hLHS).2 -/-- *alleged* satisfies no meaning postulate, Kamp's opening example (1) being that *every -alleged thief is a thief* is no logical truth. -/ +/-- *alleged* satisfies no meaning postulate, Kamp's opening example (1) (p. 123) being that +*every alleged thief is a thief* is no logical truth. -/ def allegedAdj : Modifier (W2 → E3 → Prop) := fun _N _ x ↦ match x with | .a => True | _ => False diff --git a/Studies/Kripke1980.lean b/Studies/Kripke1980.lean index 219a9ab1cd..5e44ce7e6b 100644 --- a/Studies/Kripke1980.lean +++ b/Studies/Kripke1980.lean @@ -80,7 +80,7 @@ theorem forall_largeScope_box_iff_smallScope_box_iff : (∀ P, largeScope □[R] P t w ↔ smallScope □[R] P t w) ↔ Set.EqOn t (fun _ ↦ t w) {v | w ~[R] v} := ⟨fun h v hv ↦ (h fun e _ ↦ e = t w).1 (fun _ _ ↦ rfl) v hv, fun h _ ↦ - forall₂_congr fun _ hv ↦ by simp only [h hv]⟩ + iff_of_eq (largeScope_eq_smallScope_of_dependsOn (dependsOn_box_iff.2 subset_rfl) h _)⟩ theorem isRigid_iff_largeScope_eq_smallScope : IsRigid t ↔ ∀ P, largeScope □[Set.univ] P t = smallScope □[Set.univ] P t := diff --git a/Studies/Zimmermann2026.lean b/Studies/Zimmermann2026.lean index aaad522d4c..aa39e2a587 100644 --- a/Studies/Zimmermann2026.lean +++ b/Studies/Zimmermann2026.lean @@ -2,7 +2,7 @@ module public import Studies.Owusu2022 public import Studies.Zimmermann2008 -public import Linglib.Logic.Modal.Extensional +public import Linglib.Semantics.Reference.Rigidity /-! # Zimmermann (2026): African Lambdas I, The Nominal Domain @@ -57,13 +57,19 @@ theorem bi_reading_not_narrow {S E : Type*} (f : S → ChoiceFunction E) {s : S} have h' := (Owusu2022.negation_narrow_iff f ⟨a, ha⟩).mp h hab ((h' a ha).trans (h' b hb).symm) -/-- Under negation, the bound and free construals of the situation argument of *bí* coincide, as the -explanation of (15) requires. -/ -theorem bi_negation_construals_collapse {S E : Type*} - (f : S → ChoiceFunction E) (s₀ : S) (P : S → E → Prop) (VP : E → S → Prop) : - (fun p s ↦ ¬ p s) (fun s ↦ VP (f s (P s)) s) s₀ ↔ - (fun p s ↦ ¬ p s) (fun s ↦ VP (f s₀ (P s₀)) s) s₀ := - iff_of_eq <| ModalLogic.isExtensionalAt_iff_forall_diag.mp ModalLogic.IsExtensionalAt.neg - fun σ s ↦ VP (f σ (P σ)) s +/-- Under an operator that is not intensional, such as negation, the bound and free construals of +the situation argument of *bí* (16a) coincide, so that the operator cannot shift it, as the +explanation of (15) requires (p. 7). -/ +theorem bi_construals_collapse {S E : Type*} {O : (S → Prop) → S → Prop} {s₀ : S} + (hO : ModalLogic.IsExtensionalAt O s₀) (f : S → ChoiceFunction E) (P : S → E → Prop) + (VP : E → S → Prop) : + smallScope O VP (fun s ↦ f s (P s)) s₀ = largeScope O VP (fun s ↦ f s (P s)) s₀ := + (hO.largeScope_eq_smallScope VP _).symm + +example {S E : Type*} (f : S → ChoiceFunction E) (s₀ : S) (P : S → E → Prop) + (VP : E → S → Prop) : + smallScope (fun p s ↦ ¬ p s) VP (fun s ↦ f s (P s)) s₀ = + largeScope (fun p s ↦ ¬ p s) VP (fun s ↦ f s (P s)) s₀ := + bi_construals_collapse ModalLogic.isExtensionalAt_not f P VP end Zimmermann2026 diff --git a/references.bib b/references.bib index 43a2247145..d7c16cbd8c 100644 --- a/references.bib +++ b/references.bib @@ -5006,7 +5006,7 @@ @book{gallin-1975 role = {cited}, doi = {10.1016/s0304-0208(08)x7029-x}, validated = {true}, - sources = {Semantics/Intensional/Rigidity.lean;Semantics/Intensional/Algebra.lean;Semantics/Intensional/Defs.lean;Core/Logic/Temporal/Basic.lean;Core/Logic/Modal/Basic.lean} + sources = {Logic/Modal/Basic.lean;Logic/Temporal/Basic.lean;Semantics/Composition/Ty.lean;Semantics/Reference/Rigidity.lean} } @inproceedings{kagan-alexeyenko-2011, author = {Kagan, Olga and Alexeyenko, Sascha}, @@ -5033,7 +5033,7 @@ @incollection{kamp-1975 role = {cited}, doi = {10.1017/cbo9780511897696.011}, validated = {true}, - sources = {Semantics/Degree/Delineation.lean;Semantics/Modification/Basic.lean;Semantics/Modification/Classification.lean;Studies/ChatzikyriakidisLuo2020.lean;Studies/DAmbrosioHedden2024.lean;Studies/DelPinal2015.lean;Studies/Elbourne2026.lean;Studies/Fine1975.lean;Studies/Kamp1975.lean;Studies/Klein1980.lean;Studies/Partee2010.lean} + sources = {Logic/Modal/Extensional.lean;Semantics/Degree/Delineation.lean;Semantics/Modification/Basic.lean;Semantics/Modification/Classification.lean;Studies/ChatzikyriakidisLuo2020.lean;Studies/DAmbrosioHedden2024.lean;Studies/DelPinal2015.lean;Studies/Elbourne2026.lean;Studies/Fine1975.lean;Studies/Kamp1975.lean;Studies/Klein1980.lean;Studies/Partee2010.lean} } @book{huddleston-pullum-2002, author = {Huddleston, Rodney and Pullum, Geoffrey K.}, @@ -10128,7 +10128,7 @@ @book{fitting-mendelsohn-2023 subfield = {semantics/modality}, validated = {true}, role = {cited}, - sources = {Logic/Modal/FirstOrder/Semantics.lean} + sources = {Logic/Modal/FirstOrder/Semantics.lean;Logic/Modal/FirstOrder/Syntax.lean} } @book{blackburn-derijke-venema-2001, @@ -34836,7 +34836,7 @@ @article{zimmermann-2026 doi = {10.1111/lnc3.70025}, subfield = {semantics/nominal}, role = {formalized}, - sources = {Studies/Zimmermann2026.lean} + sources = {Logic/Modal/Extensional.lean;Studies/Zimmermann2026.lean} } @book{matthewson-2008, editor = {Matthewson, Lisa}, From 0139641c3e7de20bdede2c9b9fe94f49ef1f026c Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Tue, 27 Oct 2026 12:02:06 -0700 Subject: [PATCH 2/2] refactor(Semantics/Composition): move extensional operators from Modal --- Linglib.lean | 1 - Linglib/Logic/Modal/Defs.lean | 12 +++++++++- .../Composition}/Extensional.lean | 24 ++++++------------- .../Modification/Classification.lean | 6 ++--- Linglib/Semantics/Reference/Rigidity.lean | 10 ++++---- Studies/Kamp1975.lean | 10 ++++---- Studies/Zimmermann2026.lean | 4 ++-- references.bib | 4 ++-- 8 files changed, 35 insertions(+), 36 deletions(-) rename Linglib/{Logic/Modal => Semantics/Composition}/Extensional.lean (87%) diff --git a/Linglib.lean b/Linglib.lean index bb5bcded5c..e083ca850a 100644 --- a/Linglib.lean +++ b/Linglib.lean @@ -829,7 +829,6 @@ import Linglib.Semantics.Mereology import Linglib.Semantics.Modality.BranchingTime import Linglib.Semantics.Modality.Directive import Linglib.Logic.Modal.Epistemic -import Linglib.Logic.Modal.Extensional import Linglib.Semantics.Modality.EventRelativity import Linglib.Semantics.Modality.HistoricalAlternatives import Linglib.Semantics.Modality.Kernel diff --git a/Linglib/Logic/Modal/Defs.lean b/Linglib/Logic/Modal/Defs.lean index 89a734f1d2..fcb28133a2 100644 --- a/Linglib/Logic/Modal/Defs.lean +++ b/Linglib/Logic/Modal/Defs.lean @@ -2,6 +2,7 @@ module public import Linglib.Core.Relation.SetRel public import Mathlib.Order.GaloisConnection.Basic +public import Mathlib.Logic.Function.DependsOn /-! # Necessity and possibility in Kripke frames @@ -20,7 +21,8 @@ Euclidean ones. Each axiom holds along a relation Possibility along a relation is [left adjoint to necessity along the converse relation](##diamond_box_gc), which gives the monotonicity and distribution laws, and necessity along a composite relation is -[nested necessity](##box_comp). Some laws hold at a world exactly when the world has few +[nested necessity](##box_comp). Necessity at a world depends on its argument +[at exactly the worlds the world accesses](##dependsOn_box_iff). Some laws hold at a world exactly when the world has few successors. Excluded middle for necessity, $\Box p \lor \Box \neg p$ for every $p$, holds at a world [exactly when it accesses at most one world](##box_or_box_not_at_iff), and Negation Swap, $\Box \neg p \leftrightarrow \neg \Box p$, holds everywhere @@ -100,6 +102,14 @@ theorem box_iUnion {ι : Sort*} (R : ι → SetRel W' W) : □[⋃ i, R i] p w theorem box_congr_left {w'' : W'} (h : ∀ v, w ~[R] v ↔ w'' ~[R] v) : □[R] p w ↔ □[R] p w'' := forall_congr' fun v ↦ imp_congr_left (h v) +/-- Necessity at `w` depends on its argument at a set of worlds exactly when the set contains every +world `w` accesses. -/ +theorem dependsOn_box_iff {s : Set W} : DependsOn (□[R] · w) s ↔ {v | w ~[R] v} ⊆ s := by + refine ⟨fun h v hv ↦ by_contra fun hvs ↦ ?_, fun h p q hpq ↦ + propext <| forall₂_congr fun v hv ↦ iff_of_eq (hpq v (h hv))⟩ + have := @h (· ≠ v) (fun _ ↦ True) fun u hu ↦ eq_true (ne_of_mem_of_not_mem hu hvs) + exact this.mpr (fun _ _ ↦ trivial) v hv rfl + end Operators /-! ### The Galois connection and normality -/ diff --git a/Linglib/Logic/Modal/Extensional.lean b/Linglib/Semantics/Composition/Extensional.lean similarity index 87% rename from Linglib/Logic/Modal/Extensional.lean rename to Linglib/Semantics/Composition/Extensional.lean index c1ea3e6fbf..d9549fea19 100644 --- a/Linglib/Logic/Modal/Extensional.lean +++ b/Linglib/Semantics/Composition/Extensional.lean @@ -27,14 +27,14 @@ connectives are extensional, and so are composites of extensional operators. In general the value of an operator at an index depends on its argument at some set of indices, and the operator is extensional there when that set can be taken to be the index alone. Necessity in a Kripke frame depends at a world on -[exactly the worlds accessible from it](##dependsOn_box_iff), so it is +[exactly the worlds accessible from it](##ModalLogic.dependsOn_box_iff), so it is [extensional only at a world that accesses no world but itself](##isExtensionalAt_box_iff). ## Main definitions -* `ModalLogic.IsExtensionalAt O w`: the value of `O` at `w` depends only on the extension of its +* `Montague.IsExtensionalAt O w`: the value of `O` at `w` depends only on the extension of its argument at `w`. -* `ModalLogic.IsExtensional O`: `O` is extensional at every index. +* `Montague.IsExtensional O`: `O` is extensional at every index. ## Implementation notes @@ -52,7 +52,7 @@ adjective is extensional requires. @[expose] public section -namespace ModalLogic +namespace Montague open Function @@ -102,19 +102,9 @@ theorem isExtensionalAt_iff_forall_diag : IsExtensionalAt O w ↔ ∀ g : W → W → α, O (fun v ↦ g v v) w = O (g w) w := ⟨fun h _ ↦ h rfl, fun h ↦ isExtensionalAt_iff_forall_const.2 fun p ↦ h fun u _ ↦ p u⟩ -/-! ### The box -/ +/-! ### Necessity -/ -open SetRel in -/-- The value of the box along `R` at `w` depends on a set of indices exactly when the set -contains every `R`-successor of `w`. -/ -theorem dependsOn_box_iff {W' : Type*} {R : SetRel W' W} {w : W'} {s : Set W} : - DependsOn (□[R] · w) s ↔ {v | w ~[R] v} ⊆ s := by - refine ⟨fun h v hv ↦ by_contra fun hvs ↦ ?_, fun h p q hpq ↦ - propext <| forall₂_congr fun v hv ↦ iff_of_eq (hpq v (h hv))⟩ - have := @h (· ≠ v) (fun _ ↦ True) fun u hu ↦ eq_true (ne_of_mem_of_not_mem hu hvs) - exact this.mpr (fun _ _ ↦ trivial) v hv rfl - -open SetRel in +open ModalLogic SetRel in theorem isExtensionalAt_box_iff {R : SetRel W W} : IsExtensionalAt □[R] w ↔ ∀ v, w ~[R] v → v = w := by rw [isExtensionalAt_iff_dependsOn, dependsOn_box_iff, Set.subset_singleton_iff] @@ -159,4 +149,4 @@ theorem or {O O' : (W → α) → W → Prop} (h : IsExtensionalAt O w) (h' : Is end IsExtensionalAt -end ModalLogic +end Montague diff --git a/Linglib/Semantics/Modification/Classification.lean b/Linglib/Semantics/Modification/Classification.lean index 6425d6e04b..a0847a864c 100644 --- a/Linglib/Semantics/Modification/Classification.lean +++ b/Linglib/Semantics/Modification/Classification.lean @@ -5,7 +5,7 @@ public import Linglib.Semantics.Reference.Rigidity public import Mathlib.Order.PropInstances public import Mathlib.Data.Set.Basic public import Mathlib.Tactic.Common -public import Linglib.Logic.Modal.Extensional +public import Linglib.Semantics.Composition.Extensional /-! # Modifiers of intensional properties @@ -62,8 +62,8 @@ theorem isPrivative_iff_forall : /-- Intersective modifiers are extensional, since the meet with a fixed property reads the noun only through its extension at each world. -/ -theorem IsIntersective.isExtensional (h : IsIntersective adj) : ModalLogic.IsExtensional adj := - h.elim fun Q hQ ↦ ModalLogic.isExtensional_iff_exists_eq_piMap.2 ⟨fun w ↦ (Q w ⊓ ·), funext hQ⟩ +theorem IsIntersective.isExtensional (h : IsIntersective adj) : Montague.IsExtensional adj := + h.elim fun Q hQ ↦ Montague.isExtensional_iff_exists_eq_piMap.2 ⟨fun w ↦ (Q w ⊓ ·), funext hQ⟩ /-- A privative modifier that holds of something is not subsective. -/ theorem IsPrivative.not_isSubsective (hp : IsPrivative adj) (hne : ∃ N w x, adj N w x) : diff --git a/Linglib/Semantics/Reference/Rigidity.lean b/Linglib/Semantics/Reference/Rigidity.lean index f080accadc..6e43501d6f 100644 --- a/Linglib/Semantics/Reference/Rigidity.lean +++ b/Linglib/Semantics/Reference/Rigidity.lean @@ -7,7 +7,7 @@ module public import Mathlib.Logic.Function.Basic public import Mathlib.Data.Set.Image -public import Linglib.Logic.Modal.Extensional +public import Linglib.Semantics.Composition.Extensional /-! # Rigid designation @@ -40,7 +40,7 @@ operator when `f` is rigid, and for every designator when the operator is extens * `largeScope_eq_smallScope_of_dependsOn`: the scope readings coincide for a designator constant on the indices the operator reads. * `largeScope_eq_smallScope`: the scope readings coincide for a rigid designator. -* `ModalLogic.IsExtensionalAt.largeScope_eq_smallScope`: the scope readings coincide under an +* `Montague.IsExtensionalAt.largeScope_eq_smallScope`: the scope readings coincide under an extensional operator. ## References @@ -115,8 +115,8 @@ theorem largeScope_eq_smallScope (h : IsRigid f) (O : (W → Prop) → W → Pro funext fun w ↦ largeScope_eq_smallScope_of_dependsOn (dependsOn_univ _) (fun v _ ↦ h v w) P /-- The two scope readings of every designator coincide under an operator extensional at `w`. -/ -theorem ModalLogic.IsExtensionalAt.largeScope_eq_smallScope {O : (W → Prop) → W → Prop} {w : W} - (h : ModalLogic.IsExtensionalAt O w) (P : τ → W → Prop) (f : W → τ) : +theorem Montague.IsExtensionalAt.largeScope_eq_smallScope {O : (W → Prop) → W → Prop} {w : W} + (h : Montague.IsExtensionalAt O w) (P : τ → W → Prop) (f : W → τ) : largeScope O P f w = smallScope O P f w := - largeScope_eq_smallScope_of_dependsOn (ModalLogic.isExtensionalAt_iff_dependsOn.1 h) + largeScope_eq_smallScope_of_dependsOn (Montague.isExtensionalAt_iff_dependsOn.1 h) (Set.eqOn_singleton.2 rfl) P diff --git a/Studies/Kamp1975.lean b/Studies/Kamp1975.lean index c4eafa2252..d08aae1846 100644 --- a/Studies/Kamp1975.lean +++ b/Studies/Kamp1975.lean @@ -5,7 +5,7 @@ public import Linglib.Logic.Trivalent.Basic public import Mathlib.Data.Set.Basic public import Mathlib.Algebra.Order.Ring.Rat public import Mathlib.Algebra.Order.BigOperators.Group.Finset -public import Linglib.Logic.Modal.Extensional +public import Linglib.Semantics.Composition.Extensional /-! # Kamp (1975): Two theories about adjectives @@ -34,7 +34,7 @@ two agree. Before this, Kamp argues that no many-valued logic handles borderline every world, while the gloss after it and the claim that every predicative adjective is extensional need $F'$ to vary with the world. A predicative adjective whose property differs between worlds, such as `grayAdj`, satisfies (4) and the gloss but not (7) as printed. The - study reads (7) by its gloss, `ModalLogic.IsExtensional`. + study reads (7) by its gloss, `Montague.IsExtensional`. ## References @@ -240,7 +240,7 @@ theorem gray_intersective : IsIntersective grayAdj := ⟨fun w x ↦ w = .w₁ ∧ x = .a, fun _ ↦ rfl⟩ /-- *gray* is therefore also extensional and subsective. -/ -example : ModalLogic.IsExtensional grayAdj := +example : Montague.IsExtensional grayAdj := Modifier.IsIntersective.isExtensional gray_intersective example : IsSubsective grayAdj := gray_intersective.isSubsective @@ -272,7 +272,7 @@ def skillfulAdj : Modifier (W2 → E3 → Prop) := fun N w x ↦ theorem skillful_subsective : IsSubsective skillfulAdj := fun _ _ _ h ↦ h.1 -theorem skillful_not_extensional : ¬ ModalLogic.IsExtensional skillfulAdj := by +theorem skillful_not_extensional : ¬ Montague.IsExtensional skillfulAdj := by intro hext let N₁ : W2 → E3 → Prop := fun _ _ ↦ True let N₂ : W2 → E3 → Prop := fun w x ↦ match w, x with @@ -289,7 +289,7 @@ theorem skillful_not_extensional : ¬ ModalLogic.IsExtensional skillfulAdj := by def allegedAdj : Modifier (W2 → E3 → Prop) := fun _N _ x ↦ match x with | .a => True | _ => False -theorem alleged_extensional : ModalLogic.IsExtensional allegedAdj := +theorem alleged_extensional : Montague.IsExtensional allegedAdj := fun _ _ _ _ ↦ rfl /-- *alleged N* does not entail *N*. -/ diff --git a/Studies/Zimmermann2026.lean b/Studies/Zimmermann2026.lean index aa39e2a587..a3f8ce5ebb 100644 --- a/Studies/Zimmermann2026.lean +++ b/Studies/Zimmermann2026.lean @@ -61,7 +61,7 @@ theorem bi_reading_not_narrow {S E : Type*} (f : S → ChoiceFunction E) {s : S} the situation argument of *bí* (16a) coincide, so that the operator cannot shift it, as the explanation of (15) requires (p. 7). -/ theorem bi_construals_collapse {S E : Type*} {O : (S → Prop) → S → Prop} {s₀ : S} - (hO : ModalLogic.IsExtensionalAt O s₀) (f : S → ChoiceFunction E) (P : S → E → Prop) + (hO : Montague.IsExtensionalAt O s₀) (f : S → ChoiceFunction E) (P : S → E → Prop) (VP : E → S → Prop) : smallScope O VP (fun s ↦ f s (P s)) s₀ = largeScope O VP (fun s ↦ f s (P s)) s₀ := (hO.largeScope_eq_smallScope VP _).symm @@ -70,6 +70,6 @@ example {S E : Type*} (f : S → ChoiceFunction E) (s₀ : S) (P : S → E → P (VP : E → S → Prop) : smallScope (fun p s ↦ ¬ p s) VP (fun s ↦ f s (P s)) s₀ = largeScope (fun p s ↦ ¬ p s) VP (fun s ↦ f s (P s)) s₀ := - bi_construals_collapse ModalLogic.isExtensionalAt_not f P VP + bi_construals_collapse Montague.isExtensionalAt_not f P VP end Zimmermann2026 diff --git a/references.bib b/references.bib index d7c16cbd8c..f9752c7925 100644 --- a/references.bib +++ b/references.bib @@ -5033,7 +5033,7 @@ @incollection{kamp-1975 role = {cited}, doi = {10.1017/cbo9780511897696.011}, validated = {true}, - sources = {Logic/Modal/Extensional.lean;Semantics/Degree/Delineation.lean;Semantics/Modification/Basic.lean;Semantics/Modification/Classification.lean;Studies/ChatzikyriakidisLuo2020.lean;Studies/DAmbrosioHedden2024.lean;Studies/DelPinal2015.lean;Studies/Elbourne2026.lean;Studies/Fine1975.lean;Studies/Kamp1975.lean;Studies/Klein1980.lean;Studies/Partee2010.lean} + sources = {Semantics/Composition/Extensional.lean;Semantics/Degree/Delineation.lean;Semantics/Modification/Basic.lean;Semantics/Modification/Classification.lean;Studies/ChatzikyriakidisLuo2020.lean;Studies/DAmbrosioHedden2024.lean;Studies/DelPinal2015.lean;Studies/Elbourne2026.lean;Studies/Fine1975.lean;Studies/Kamp1975.lean;Studies/Klein1980.lean;Studies/Partee2010.lean} } @book{huddleston-pullum-2002, author = {Huddleston, Rodney and Pullum, Geoffrey K.}, @@ -34836,7 +34836,7 @@ @article{zimmermann-2026 doi = {10.1111/lnc3.70025}, subfield = {semantics/nominal}, role = {formalized}, - sources = {Logic/Modal/Extensional.lean;Studies/Zimmermann2026.lean} + sources = {Semantics/Composition/Extensional.lean;Studies/Zimmermann2026.lean} } @book{matthewson-2008, editor = {Matthewson, Lisa},