Grove (2022): Presupposition Projection as a Scope Phenomenon

This file formalizes Grove's scope theory of presupposition projection, on which a presupposition trigger denotes a value of a maybe type, undefined on presupposition failure, and its presupposition projects to the constituent over which it takes scope. The maybe types are Option, whose unit and bind are the type shifts of (15); the intensional monad of section 4.1 is the reader transformer over it, as the paper's footnote says (Iₚ); the connective of (16) is the middle Kleene material conditional (materialCond); the presuppositional universal of (27) is undefined wherever its scope is; and believe is the Hintikka quantifier (28) over them. The proviso problem of section 2.1 then dissolves into a scope ambiguity. For If Theo has a brother, he'll bring his wetsuit, the trigger in situ yields the conditional presupposition of the satisfaction theory (localReading_isSome_iff), the consequent pied-piped over the conditional yields the unconditional one (globalReading_isSome_iff), and the two readings agree wherever the global one is defined. For Theo believes he lost his wetsuit, section 4.2, the clause in situ presupposes a wetsuit at every doxastic alternative and the clause scoped above the verb a wetsuit at the evaluation index, with the at-issue content reconstructing by Left Identity (believeGlobal_eq_some_true_iff).

Implementation notes

The truth-value type is Bool, so the possibly undefined truth values are Option Bool, the library's SignType in monadic form, and the predicates of the models are decidable propositions turned into truth values by decide. The universal of (27) quantifies over a whole type and is defined classically. The readings are stated for arbitrary index and entity types, the trigger his wetsuit being an Iₚ I E value, so the presupposition theorems are general rather than checked on a finite model. The monad laws of Figure 7 are Lean's lawful-monad instance for the reader transformer. The paper's judged sentences are rows of Data.Examples.Grove2022.

References

• [Gro22]
• [Hei83]
• [Hei92]
• [Cha20]
• [BK01]

TODO

The syntax of roll-up pied-piping in Figures 2 and 6 and the sketched also of (29) are not represented; the readings are the meanings the derivations deliver.

@[reducible, inline]

abbrev Grove2022.Iₚ (I α : Type) : Type

The intensional presuppositional monad I# of section 4.1, a reader over the maybe monad.

Equations

• Grove2022.Iₚ I = ReaderT I Option

theorem Grove2022.monad_laws {I α β γ : Type} (v : α) (m : Iₚ I α) (k : α → Iₚ I β) (n : β → Iₚ I γ) : pure v >>= k = k v ∧ m >>= pure = m ∧ m >>= k >>= n = m >>= fun (x : α) => k x >>= n

The monad laws of Figure 7 hold for I#. Left Identity is semantic reconstruction, and Associativity is what licenses cyclic scope.

def Grove2022.materialCond : Option Bool → Option Bool → Option Bool

The material conditional of (16) has middle Kleene semantics, in which an undefined antecedent absorbs and a false one makes the conditional true whatever the consequent.

Equations

• Grove2022.materialCond none x✝ = none
• Grove2022.materialCond (some false) x✝ = some true
• Grove2022.materialCond (some true) x✝ = x✝

theorem Grove2022.materialCond_decide (P : Prop) [Decidable P] (ψ : Option Bool) : materialCond (some (decide P)) ψ = if P then ψ else some true

noncomputable def Grove2022.forallP {α : Type u_1} (φ : α → Option Bool) : Option Bool

The presuppositional universal of (27) is true if its scope is true everywhere, undefined if its scope is undefined somewhere, and false otherwise.

Equations

• Grove2022.forallP φ = if ∃ (x : α), φ x = none then none else if ∀ (x : α), φ x = some true then some true else some false

theorem Grove2022.forallP_eq_none_iff {α : Type u_1} (φ : α → Option Bool) : forallP φ = none ↔ ∃ (x : α), φ x = none

theorem Grove2022.forallP_eq_some_true_iff {α : Type u_1} (φ : α → Option Bool) : forallP φ = some true ↔ ∀ (x : α), φ x = some true

theorem Grove2022.forallP_isSome_iff {α : Type u_1} (φ : α → Option Bool) : (forallP φ).isSome = true ↔ ∀ (x : α), (φ x).isSome = true

def Grove2022.evalI {I : Type} (φ : Iₚ I (I → Bool)) : Iₚ I Bool

The evaluation of (20) identifies the index an I# (i → t) value reads with the index of the intension it returns.

Equations

• Grove2022.evalI φ i = Option.map (fun (x : I → Bool) => x i) (φ i)

noncomputable def Grove2022.believe {I E : Type} (dox : E → I → I → Prop) [(x : E) → (i j : I) → Decidable (dox x i j)] (φ : Iₚ I Bool) (x : E) : Iₚ I Bool

The believe of (28) is the Hintikka quantifier over doxastic alternatives, the conditional filtering the inaccessible indices.

Equations

• Grove2022.believe dox φ x i = Grove2022.forallP fun (j : I) => Grove2022.materialCond (some (decide (dox x i j))) (φ j)

The conditional, section 3

If Theo has a brother, he'll bring his wetsuit, (1): bro is the antecedent, wetsuit the trigger his wetsuit, Theo's unique wetsuit at an index if he has one, and bring the predicate.

def Grove2022.consequent {I E : Type} (wetsuit : Iₚ I E) (bring : E → I → Prop) [(x : E) → (i : I) → Decidable (bring x i)] : Iₚ I Bool

The consequent with the trigger scoped to its edge, as in Figure 5, is the lifted trigger over the abstracted clause, of type t#.

Equations

• Grove2022.consequent wetsuit bring i = do let x ← wetsuit i pure (decide (bring x i))

def Grove2022.localReading {I E : Type} (bro : I → Prop) [DecidablePred bro] (wetsuit : Iₚ I E) (bring : E → I → Prop) [(x : E) → (i : I) → Decidable (bring x i)] : Iₚ I Bool

The local reading of (1), in Figure 5, applies the conditional to the consequent.

Equations

• Grove2022.localReading bro wetsuit bring i = Grove2022.materialCond (some (decide (bro i))) (Grove2022.consequent wetsuit bring i)

def Grove2022.globalReading {I E : Type} (bro : I → Prop) [DecidablePred bro] (wetsuit : Iₚ I E) (bring : E → I → Prop) [(x : E) → (i : I) → Decidable (bring x i)] : Iₚ I Bool

In the global reading of (1), Figure 6, the consequent, of type t## after two units in the trigger's scope, takes scope over the conditional.

Equations

• Grove2022.globalReading bro wetsuit bring i = do let ψ ← do let x ← wetsuit i pure (pure (decide (bring x i))) Grove2022.materialCond (some (decide (bro i))) ψ

theorem Grove2022.localReading_eq_none_iff {I E : Type} (bro : I → Prop) [DecidablePred bro] (wetsuit : Iₚ I E) (bring : E → I → Prop) [(x : E) → (i : I) → Decidable (bring x i)] (i : I) : localReading bro wetsuit bring i = none ↔ bro i ∧ wetsuit i = none

The local reading is undefined exactly when Theo has a brother but no wetsuit, the conditional presupposition of the satisfaction theory in Figure 3.

theorem Grove2022.localReading_eq_some_true_iff {I E : Type} (bro : I → Prop) [DecidablePred bro] (wetsuit : Iₚ I E) (bring : E → I → Prop) [(x : E) → (i : I) → Decidable (bring x i)] (i : I) : localReading bro wetsuit bring i = some true ↔ bro i → ∃ (x : E), wetsuit i = some x ∧ bring x i

theorem Grove2022.localReading_isSome_iff {I E : Type} (bro : I → Prop) [DecidablePred bro] (wetsuit : Iₚ I E) (bring : E → I → Prop) [(x : E) → (i : I) → Decidable (bring x i)] (i : I) : (localReading bro wetsuit bring i).isSome = true ↔ bro i → (wetsuit i).isSome = true

theorem Grove2022.globalReading_eq_none_iff {I E : Type} (bro : I → Prop) [DecidablePred bro] (wetsuit : Iₚ I E) (bring : E → I → Prop) [(x : E) → (i : I) → Decidable (bring x i)] (i : I) : globalReading bro wetsuit bring i = none ↔ wetsuit i = none

The global reading is undefined exactly when Theo has no wetsuit, the unconditional presupposition of Figure 4, available without pragmatic strengthening.

theorem Grove2022.globalReading_eq_some_true_iff {I E : Type} (bro : I → Prop) [DecidablePred bro] (wetsuit : Iₚ I E) (bring : E → I → Prop) [(x : E) → (i : I) → Decidable (bring x i)] (i : I) : globalReading bro wetsuit bring i = some true ↔ ∃ (x : E), wetsuit i = some x ∧ (bro i → bring x i)

theorem Grove2022.globalReading_isSome_iff {I E : Type} (bro : I → Prop) [DecidablePred bro] (wetsuit : Iₚ I E) (bring : E → I → Prop) [(x : E) → (i : I) → Decidable (bring x i)] (i : I) : (globalReading bro wetsuit bring i).isSome = true ↔ (wetsuit i).isSome = true

theorem Grove2022.globalReading_eq_localReading_of_isSome {I E : Type} (bro : I → Prop) [DecidablePred bro] (wetsuit : Iₚ I E) (bring : E → I → Prop) [(x : E) → (i : I) → Decidable (bring x i)] (i : I) (h : (wetsuit i).isSome = true) : globalReading bro wetsuit bring i = localReading bro wetsuit bring i

The two readings differ only in their presuppositions, since wherever the global reading is defined, so is the local one, with the same value.

theorem Grove2022.reconstruct {I E : Type} (bro : I → Prop) [DecidablePred bro] (wetsuit : Iₚ I E) (bring : E → I → Prop) [(x : E) → (i : I) → Decidable (bring x i)] (i : I) : (do let ψ ← pure (consequent wetsuit bring i) materialCond (some (decide (bro i))) ψ) = localReading bro wetsuit bring i

By Left Identity, a unit applied outside the trigger's scope reconstructs, giving the local reading again rather than the global one, as the paper's footnote on Figure 6 observes.

Propositional attitudes, section 4.2

Theo believes he lost his wetsuit, (22): the complement is derived with intensions, Figure 8, and either evaluated in situ under the verb, Figure 9, or scoped above it, Figure 10.

def Grove2022.lostClause {I E : Type} (wetsuit : Iₚ I E) (lose : E → I → Prop) [(x : E) → (i : I) → Decidable (lose x i)] : Iₚ I (I → Bool)

he lost his wetsuit with the trigger scoped over the clause, an I# (i → t) value.

Equations

• Grove2022.lostClause wetsuit lose j = do let x ← wetsuit j pure fun (i : I) => decide (lose x i)

noncomputable def Grove2022.believeLocal {I E : Type} (dox : E → I → I → Prop) [(x : E) → (i j : I) → Decidable (dox x i j)] (wetsuit : Iₚ I E) (lose : E → I → Prop) [(x : E) → (i : I) → Decidable (lose x i)] (theo : E) : Iₚ I Bool

The local reading of (22), in Figure 9, evaluates the complement under believe.

Equations

• Grove2022.believeLocal dox wetsuit lose theo = Grove2022.believe dox (Grove2022.evalI (Grove2022.lostClause wetsuit lose)) theo

noncomputable def Grove2022.believeGlobal {I E : Type} (dox : E → I → I → Prop) [(x : E) → (i j : I) → Decidable (dox x i j)] (wetsuit : Iₚ I E) (lose : E → I → Prop) [(x : E) → (i : I) → Decidable (lose x i)] (theo : E) : Iₚ I Bool

In the global reading of (22), Figure 10, the clause scopes above the verb through the reader bind, its trigger read at the evaluation index.

Equations

• Grove2022.believeGlobal dox wetsuit lose theo = do let φ ← Grove2022.lostClause wetsuit lose Grove2022.believe dox (fun (j : I) => pure (φ j)) theo

theorem Grove2022.evalI_lostClause {I E : Type} (wetsuit : Iₚ I E) (lose : E → I → Prop) [(x : E) → (i : I) → Decidable (lose x i)] (j : I) : evalI (lostClause wetsuit lose) j = do let x ← wetsuit j pure (decide (lose x j))

Evaluating the clause as in (21) makes the trigger and the predicate read the same index.

theorem Grove2022.believeLocal_isSome_iff {I E : Type} (dox : E → I → I → Prop) [(x : E) → (i j : I) → Decidable (dox x i j)] (wetsuit : Iₚ I E) (lose : E → I → Prop) [(x : E) → (i : I) → Decidable (lose x i)] (theo : E) (i : I) : (believeLocal dox wetsuit lose theo i).isSome = true ↔ ∀ (j : I), dox theo i j → (wetsuit j).isSome = true

In situ, the presupposition is that Theo has a wetsuit at every doxastic alternative, the prediction of [Hei92] for (22).

theorem Grove2022.believeLocal_eq_some_true_iff {I E : Type} (dox : E → I → I → Prop) [(x : E) → (i j : I) → Decidable (dox x i j)] (wetsuit : Iₚ I E) (lose : E → I → Prop) [(x : E) → (i : I) → Decidable (lose x i)] (theo : E) (i : I) : believeLocal dox wetsuit lose theo i = some true ↔ ∀ (j : I), dox theo i j → ∃ (x : E), wetsuit j = some x ∧ lose x j

theorem Grove2022.believeGlobal_isSome_iff {I E : Type} (dox : E → I → I → Prop) [(x : E) → (i j : I) → Decidable (dox x i j)] (wetsuit : Iₚ I E) (lose : E → I → Prop) [(x : E) → (i : I) → Decidable (lose x i)] (theo : E) (i : I) : (believeGlobal dox wetsuit lose theo i).isSome = true ↔ (wetsuit i).isSome = true

Scoped above the verb, the presupposition is that Theo has a wetsuit at the evaluation index, so it projects past believe and his wetsuit is read de re.

theorem Grove2022.believeGlobal_eq_some_true_iff {I E : Type} (dox : E → I → I → Prop) [(x : E) → (i j : I) → Decidable (dox x i j)] (wetsuit : Iₚ I E) (lose : E → I → Prop) [(x : E) → (i : I) → Decidable (lose x i)] (theo : E) (i : I) : believeGlobal dox wetsuit lose theo i = some true ↔ ∃ (x : E), wetsuit i = some x ∧ ∀ (j : I), dox theo i j → lose x j

The at-issue content reconstructs, so the global reading is true exactly when Theo has a wetsuit that he lost at all his doxastic alternatives.