Question-based desire semantics

a wants p relative to a contextual question Q: the answers compatible with a's beliefs are ordered by the desires they entail, and the ascription holds iff every best such answer entails p — [PB25]'s semantics. Its definedness conditions are the paper's metasemantic constraints — IsConsidered (every answer settles p), IsDiverse (both p- and ¬p-answers), IsAntiDeckstacking (a salient proposition some answer entails is itself settled; [Con02]), IsBelSensitive (the beliefs discriminate among the answers; [Yal18]) — bundled as Defined and as the presupposition of toPartialProp, under which the ascription is Strawson upward monotone (toPartialProp_strawsonEntails). On the finest question the semantics is the best-worlds one (want_finest_iff).

def Desire.QuestionBased.le {W : Type u_1} (G : List (Finset W)) (a a' : Finset W) : Prop

le G a a': every desire in G entailed by a' is entailed by a — the criteria-derived order with entailment as satisfaction.

Equations

• Desire.QuestionBased.le G a a' = (a ⊆ a')

theorem Desire.QuestionBased.le_iff {W : Type u_1} (G : List (Finset W)) (a a' : Finset W) : le G a a' ↔ ∀ s ∈ G, a' ⊆ s → a ⊆ s

def Desire.QuestionBased.Live {W : Type u_1} (bel : Set W) (a : Finset W) : Prop

An answer compatible with the beliefs.

Equations

• Desire.QuestionBased.Live bel a = ∃ w ∈ a, w ∈ bel

def Desire.QuestionBased.Want {W : Type u_1} (G Q : List (Finset W)) (bel p : Set W) : Prop

a wants p: every best live answer of Q entails p.

Equations

• One or more equations did not get rendered due to their size.

def Desire.QuestionBased.IsConsidered {W : Type u_1} (Q : List (Finset W)) (p : Set W) : Prop

Every answer settles p.

Equations

• Desire.QuestionBased.IsConsidered Q p = ∀ a ∈ Q, (∀ w ∈ a, w ∈ p) ∨ ∀ w ∈ a, w ∉ p

def Desire.QuestionBased.IsDiverse {W : Type u_1} (Q : List (Finset W)) (p : Set W) : Prop

Some answer entails p and some entails ¬p.

Equations

• Desire.QuestionBased.IsDiverse Q p = ((∃ a ∈ Q, ∀ w ∈ a, w ∈ p) ∧ ∃ a ∈ Q, ∀ w ∈ a, w ∉ p)

def Desire.QuestionBased.IsAntiDeckstacking {W : Type u_1} (N Q : List (Finset W)) : Prop

Every salient proposition in N that some answer entails is itself settled.

Equations

• Desire.QuestionBased.IsAntiDeckstacking N Q = ∀ q ∈ N, (∃ a ∈ Q, a ⊆ q) → Desire.QuestionBased.IsConsidered Q ↑q

def Desire.QuestionBased.IsBelSensitive {W : Type u_1} (Q : List (Finset W)) (bel : Set W) : Prop

The beliefs discriminate among the answers: some answer is live and some is not.

Equations

• Desire.QuestionBased.IsBelSensitive Q bel = ((∃ a ∈ Q, Desire.QuestionBased.Live bel a) ∧ ∃ a ∈ Q, ¬Desire.QuestionBased.Live bel a)

def Desire.QuestionBased.Defined {W : Type u_1} (N Q : List (Finset W)) (bel p : Set W) : Prop

The four metasemantic constraints jointly.

Equations

• One or more equations did not get rendered due to their size.

def Desire.QuestionBased.toPartialProp {W : Type u_1} (G N Q : List (Finset W)) (bel p : Set W) : Semantics.Presupposition.PartialProp W

Question-based want with its definedness conditions as presupposition.

Equations

• Desire.QuestionBased.toPartialProp G N Q bel p = { presup := fun (x : W) => Desire.QuestionBased.Defined N Q bel p, assertion := fun (x : W) => Desire.QuestionBased.Want G Q bel p }

@[instance_reducible]

instance Desire.QuestionBased.instDecidableLeOfDecidableEq {W : Type u_1} (G : List (Finset W)) [DecidableEq W] (a a' : Finset W) : Decidable (le G a a')

Equations

• Desire.QuestionBased.instDecidableLeOfDecidableEq G a a' = Desire.QuestionBased.instDecidableLeOfDecidableEq._aux_1 G a a'

@[instance_reducible]

instance Desire.QuestionBased.instDecidableLiveOfDecidablePredMemSet {W : Type u_1} (bel : Set W) [DecidablePred fun (x : W) => x ∈ bel] (a : Finset W) : Decidable (Live bel a)

Equations

• Desire.QuestionBased.instDecidableLiveOfDecidablePredMemSet bel a = Desire.QuestionBased.instDecidableLiveOfDecidablePredMemSet._aux_1 bel a

@[instance_reducible]

instance Desire.QuestionBased.instDecidableWantOfDecidableEqOfDecidablePredMemSet {W : Type u_1} (G Q : List (Finset W)) (bel p : Set W) [DecidableEq W] [DecidablePred fun (x : W) => x ∈ bel] [DecidablePred fun (x : W) => x ∈ p] : Decidable (Want G Q bel p)

Equations

• Desire.QuestionBased.instDecidableWantOfDecidableEqOfDecidablePredMemSet G Q bel p = Desire.QuestionBased.instDecidableWantOfDecidableEqOfDecidablePredMemSet._aux_1 G Q bel p

@[instance_reducible]

instance Desire.QuestionBased.instDecidableIsConsideredOfDecidablePredMemSet {W : Type u_1} (Q : List (Finset W)) (p : Set W) [DecidablePred fun (x : W) => x ∈ p] : Decidable (IsConsidered Q p)

Equations

• Desire.QuestionBased.instDecidableIsConsideredOfDecidablePredMemSet Q p = Desire.QuestionBased.instDecidableIsConsideredOfDecidablePredMemSet._aux_1 Q p

@[instance_reducible]

instance Desire.QuestionBased.instDecidableIsDiverseOfDecidablePredMemSet {W : Type u_1} (Q : List (Finset W)) (p : Set W) [DecidablePred fun (x : W) => x ∈ p] : Decidable (IsDiverse Q p)

Equations

• Desire.QuestionBased.instDecidableIsDiverseOfDecidablePredMemSet Q p = Desire.QuestionBased.instDecidableIsDiverseOfDecidablePredMemSet._aux_1 Q p

@[instance_reducible]

instance Desire.QuestionBased.instDecidableIsAntiDeckstackingOfDecidableEq {W : Type u_1} (N Q : List (Finset W)) [DecidableEq W] : Decidable (IsAntiDeckstacking N Q)

Equations

• Desire.QuestionBased.instDecidableIsAntiDeckstackingOfDecidableEq N Q = Desire.QuestionBased.instDecidableIsAntiDeckstackingOfDecidableEq._aux_1 N Q

@[instance_reducible]

instance Desire.QuestionBased.instDecidableIsBelSensitiveOfDecidablePredMemSet {W : Type u_1} (Q : List (Finset W)) (bel : Set W) [DecidablePred fun (x : W) => x ∈ bel] : Decidable (IsBelSensitive Q bel)

Equations

• Desire.QuestionBased.instDecidableIsBelSensitiveOfDecidablePredMemSet Q bel = Desire.QuestionBased.instDecidableIsBelSensitiveOfDecidablePredMemSet._aux_1 Q bel

@[instance_reducible]

instance Desire.QuestionBased.instDecidableDefinedOfDecidableEqOfDecidablePredMemSet {W : Type u_1} (N Q : List (Finset W)) (bel p : Set W) [DecidableEq W] [DecidablePred fun (x : W) => x ∈ bel] [DecidablePred fun (x : W) => x ∈ p] : Decidable (Defined N Q bel p)

Equations

• Desire.QuestionBased.instDecidableDefinedOfDecidableEqOfDecidablePredMemSet N Q bel p = Desire.QuestionBased.instDecidableDefinedOfDecidableEqOfDecidablePredMemSet._aux_1 N Q bel p

theorem Desire.QuestionBased.Want.mono {W : Type u_1} {G Q : List (Finset W)} {bel p q : Set W} (hpq : p ⊆ q) (h : Want G Q bel p) : Want G Q bel q

theorem Desire.QuestionBased.toPartialProp_strawsonEntails {W : Type u_1} {G N Q : List (Finset W)} {bel p q : Set W} (hpq : p ⊆ q) : (toPartialProp G N Q bel p).strawsonEntails (toPartialProp G N Q bel q)

Strawson upward monotonicity: where both ascriptions are defined, want p entails want q for p ⊆ q.

The finest question

def Desire.QuestionBased.finest {W : Type u_1} (worlds : List W) : List (Finset W)

The finest question over a world list: one singleton answer per world.

Equations

• Desire.QuestionBased.finest worlds = List.map (fun (x : W) => {x}) worlds

theorem Desire.QuestionBased.le_singleton_iff {W : Type u_1} (G : List (Finset W)) (w z : W) : le G {w} {z} ↔ BestWorlds.le G w z

theorem Desire.QuestionBased.want_finest_iff {W : Type u_1} {G : List (Finset W)} {bel p : Set W} {worlds : List W} (h : ∀ (w : W), w ∈ worlds) : Want G (finest worlds) bel p ↔ BestWorlds.Want G bel p

On the finest question over an exhaustive world list, question-based want is best-worlds want.