|
| 1 | +import Linglib.Theories.Semantics.Attitudes.ContextQuantification |
| 2 | +import Linglib.Theories.Semantics.Reference.ShiftedIndexicals |
| 3 | +import Linglib.Theories.Semantics.Reference.Kaplan |
| 4 | +import Linglib.Theories.Semantics.Reference.Monsters |
| 5 | +import Linglib.Theories.Semantics.Reference.PersonFeatures |
| 6 | + |
| 7 | +/-! |
| 8 | +# Schlenker (2003): A Plea for Monsters |
| 9 | +@cite{schlenker-2003} |
| 10 | +
|
| 11 | +End-to-end verification of @cite{schlenker-2003}'s core argument: |
| 12 | +
|
| 13 | +1. Kaplan's thesis (no monsters) holds for English: "I" always refers |
| 14 | + to the actual speaker, even under attitude verbs |
| 15 | +2. Amharic violates the thesis: "I" shifts to the attitude holder |
| 16 | +3. Context quantification (`ctxBox`) captures both patterns: |
| 17 | + - With world-only meaning → reduces to standard `boxAt` (Fixity holds) |
| 18 | + - With agent-reading meaning → strictly more expressive (Fixity fails) |
| 19 | +4. Person features as presuppositions derive logophoric pronouns |
| 20 | +
|
| 21 | +## Derivation Chain |
| 22 | +
|
| 23 | +``` |
| 24 | +Core.Context.Tower (ContextTower, push, origin, innermost) |
| 25 | + ↓ |
| 26 | +Core.Context.Shifts (attitudeShift) |
| 27 | + ↓ |
| 28 | +Theories.Semantics.Reference.Kaplan (pronI_access, origin-reading) |
| 29 | + ↓ |
| 30 | +Theories.Semantics.Reference.ShiftedIndexicals (amharic_pronI, local-reading) |
| 31 | + ↓ |
| 32 | +Theories.Semantics.Attitudes.ContextQuantification (ctxBox, Fixity) |
| 33 | + ↓ |
| 34 | +Theories.Semantics.Reference.PersonFeatures (logophoric pronouns) |
| 35 | + ↓ |
| 36 | +This file: concrete end-to-end verification |
| 37 | +``` |
| 38 | +-/ |
| 39 | + |
| 40 | +namespace Phenomena.Reference.Studies.Schlenker2003 |
| 41 | + |
| 42 | +open Core.Context |
| 43 | +open Semantics.Attitudes.ContextQuantification |
| 44 | +open Semantics.Attitudes.Doxastic (AccessRel boxAt) |
| 45 | +open Semantics.Reference.ShiftedIndexicals (amharic_pronI) |
| 46 | +open Semantics.Reference.Kaplan (pronI_access) |
| 47 | + |
| 48 | +-- ════════════════════════════════════════════════════════════════ |
| 49 | +-- § Concrete Setup |
| 50 | +-- ════════════════════════════════════════════════════════════════ |
| 51 | + |
| 52 | +inductive Person | alice | bob |
| 53 | + deriving DecidableEq, BEq, Repr |
| 54 | + |
| 55 | +inductive World | w0 | w1 |
| 56 | + deriving DecidableEq, BEq, Repr |
| 57 | + |
| 58 | +abbrev Ctx := KContext World Person Unit Unit |
| 59 | + |
| 60 | +/-- Speech-act context: Alice speaking to Bob at world w0. -/ |
| 61 | +def speechCtx : Ctx := |
| 62 | + { agent := .alice, addressee := .bob, world := .w0, |
| 63 | + time := (), position := () } |
| 64 | + |
| 65 | +def rootT : ContextTower Ctx := ContextTower.root speechCtx |
| 66 | + |
| 67 | +/-- Bob's doxastic accessibility: both worlds are compatible with |
| 68 | + what Bob believes. -/ |
| 69 | +def bobBel : AccessRel World Person |
| 70 | + | .bob, _, _ => true |
| 71 | + | .alice, _, w' => w' == .w0 |
| 72 | + |
| 73 | +/-- Tower after attitude shift: "Bob said that ..." pushes Bob as |
| 74 | + agent and w1 as the attitude world. -/ |
| 75 | +def shiftedT : ContextTower Ctx := |
| 76 | + rootT.push (attitudeShift .bob .w1) |
| 77 | + |
| 78 | +-- ════════════════════════════════════════════════════════════════ |
| 79 | +-- § English vs Amharic "I" Under Attitude Shift |
| 80 | +-- ════════════════════════════════════════════════════════════════ |
| 81 | + |
| 82 | +/-- English "I" = Alice (actual speaker), even under Bob's attitude verb. -/ |
| 83 | +theorem english_I_is_speaker : |
| 84 | + pronI_access.resolve shiftedT = .alice := rfl |
| 85 | + |
| 86 | +/-- Amharic "I" = Bob (attitude holder), shifted by the attitude verb. -/ |
| 87 | +theorem amharic_I_is_holder : |
| 88 | + amharic_pronI.resolve shiftedT = .bob := rfl |
| 89 | + |
| 90 | +/-- English and Amharic "I" diverge under the same attitude shift. -/ |
| 91 | +theorem indexicals_diverge : |
| 92 | + pronI_access.resolve shiftedT ≠ amharic_pronI.resolve shiftedT := by |
| 93 | + decide |
| 94 | + |
| 95 | +-- ════════════════════════════════════════════════════════════════ |
| 96 | +-- § Context Quantification: English vs Amharic Truth Conditions |
| 97 | +-- ════════════════════════════════════════════════════════════════ |
| 98 | + |
| 99 | +/-- Happiness predicate: Alice is happy in w0 only; Bob is happy in both. -/ |
| 100 | +def isHappy : Person → World → Bool |
| 101 | + | .alice, .w0 => true |
| 102 | + | .alice, .w1 => false |
| 103 | + | .bob, _ => true |
| 104 | + |
| 105 | +/-- English: "Bob said that I am happy" = "Bob said that Alice is happy." |
| 106 | + The meaning is world-only (Alice is fixed by origin-reading "I"), |
| 107 | + so context quantification reduces to standard world quantification. -/ |
| 108 | +theorem english_reduces_to_boxAt : |
| 109 | + ctxBox bobBel .bob (fun c => isHappy .alice c.world) rootT .w0 [.w0, .w1] = |
| 110 | + boxAt bobBel .bob .w0 [.w0, .w1] (isHappy .alice) := by |
| 111 | + simp only [ctxBox_world_only] |
| 112 | + |
| 113 | +/-- English version is false: Alice is NOT happy in all of Bob's |
| 114 | + belief worlds (she's unhappy in w1). -/ |
| 115 | +theorem english_result : |
| 116 | + ctxBox bobBel .bob (fun c => isHappy .alice c.world) |
| 117 | + rootT .w0 [.w0, .w1] = false := by |
| 118 | + native_decide |
| 119 | + |
| 120 | +/-- Amharic: "Bob said that I am happy" = "Bob said that Bob is happy." |
| 121 | + The meaning reads the agent from the shifted context (Bob), |
| 122 | + so ctxBox does NOT reduce to boxAt. -/ |
| 123 | +theorem amharic_result : |
| 124 | + ctxBox bobBel .bob (fun c => isHappy c.agent c.world) |
| 125 | + rootT .w0 [.w0, .w1] = true := by |
| 126 | + native_decide |
| 127 | + |
| 128 | +/-- The English and Amharic versions have different truth values: |
| 129 | + English is false, Amharic is true. This is the formal content of |
| 130 | + @cite{schlenker-2003}'s argument that context quantification is |
| 131 | + strictly more expressive than world quantification. -/ |
| 132 | +theorem english_amharic_differ : |
| 133 | + ctxBox bobBel .bob (fun c => isHappy .alice c.world) |
| 134 | + rootT .w0 [.w0, .w1] ≠ |
| 135 | + ctxBox bobBel .bob (fun c => isHappy c.agent c.world) |
| 136 | + rootT .w0 [.w0, .w1] := by |
| 137 | + native_decide |
| 138 | + |
| 139 | +-- ════════════════════════════════════════════════════════════════ |
| 140 | +-- § Fixity Thesis |
| 141 | +-- ════════════════════════════════════════════════════════════════ |
| 142 | + |
| 143 | +/-- World-only meanings satisfy Fixity (Claim 2): the truth value of |
| 144 | + "Alice is happy" is tower-independent. -/ |
| 145 | +theorem fixity_english : |
| 146 | + SatisfiesFixity (W := World) (E := Person) (P := Unit) (T := Unit) |
| 147 | + (fun _ w => isHappy .alice w) := |
| 148 | + fixity_world_only (isHappy .alice) |
| 149 | + |
| 150 | +-- ════════════════════════════════════════════════════════════════ |
| 151 | +-- § Context Quantification ↔ Shifted Indexicals Bridge |
| 152 | +-- ════════════════════════════════════════════════════════════════ |
| 153 | + |
| 154 | +/-- The agent of the accessible context (from `ctxFromShift`) is exactly |
| 155 | + what Amharic "I" (`amharic_pronI`) resolves to. -/ |
| 156 | +theorem bridge_ctxFromShift_amharic : |
| 157 | + (ctxFromShift rootT .bob .w1).agent = |
| 158 | + amharic_pronI.resolve shiftedT := by |
| 159 | + native_decide |
| 160 | + |
| 161 | +/-- English "I" gives the same result with or without the shift: |
| 162 | + both return Alice (the origin agent). -/ |
| 163 | +theorem bridge_english_invariant : |
| 164 | + pronI_access.resolve shiftedT = |
| 165 | + pronI_access.resolve rootT := |
| 166 | + english_I_invariant rootT .bob .w1 |
| 167 | + |
| 168 | +-- ════════════════════════════════════════════════════════════════ |
| 169 | +-- § Person Features: Logophoric Pronouns |
| 170 | +-- ════════════════════════════════════════════════════════════════ |
| 171 | + |
| 172 | +open Semantics.Reference.PersonFeatures |
| 173 | + |
| 174 | +/-- Bob is logophoric under the attitude shift: he is +author(local) |
| 175 | + (agent of the embedded context) but −author* (not the actual |
| 176 | + speaker Alice). -/ |
| 177 | +theorem bob_is_logophoric : |
| 178 | + isLogophoric .bob shiftedT .local = true := by |
| 179 | + native_decide |
| 180 | + |
| 181 | +/-- Alice (the speaker) is never logophoric: +author* blocks it. -/ |
| 182 | +theorem alice_not_logophoric : |
| 183 | + isLogophoric .alice shiftedT .local = false := by |
| 184 | + native_decide |
| 185 | + |
| 186 | +end Phenomena.Reference.Studies.Schlenker2003 |
0 commit comments