Katzir and Singh (2015): Economy of Structure and Information

Katzir and Singh account for the oddness of assertions such as Some Italians come from a warm country and John has one wife with two felicity conditions. The question condition (8) asks that an assertion address a question the participants are known to want settled; the answer condition (15) asks that it be a true, relevant answer not needlessly worse than another true relevant one, an alternative being better (16) when it is at most as complex, in Katzir's structural sense, and at least as strong. A Scenario collects the meanings and complexities of the alternatives, the context and the question, and Felicitous conjoins the two conditions.

Main results

• Scenario.better_trans: being better is a strict order.
• Scenario.not_goodAnswer_of_stronger: a true relevant alternative of no greater complexity that is strictly stronger makes an answer needlessly weak, behind the some/all cases (17) and (18) and Heim's Maximize Presupposition (21).
• Scenario.not_goodAnswer_disj, Scenario.not_goodAnswer_conj: disjoining a stronger or conjoining a weaker constituent makes an answer needlessly complex, Hurford's constraint (22).
• some_all_odd_of_settled, all_felicitous_some_odd, some_felicitous_all_odd: the one-answer question of (1) makes some and all alike odd, the open question of (17) leaves all good and some odd where all holds, and the downward-entailing (18) reverses the verdict.

Implementation notes

A question is a family of answers, the alternatives of the assertion when no question is explicit, and it is settled in a context when its live answers there coincide, the use the paper makes of the good question of (7); an assertion is relevant when it does not split a cell of the partition the answers induce (the paper's footnote 8). Complexity enters as a rank, the structural order not being rebuilt on trees. Meanings are sets of worlds, with presupposition folded into truth for (21). The embedded cases of Section 4, which the paper leaves open, are not represented.

References

• [KS15]
• [Mag09]
• [Spe14]
• [Hei91]
• [Hur74]
• [Kat07]

structure KatzirSingh2015.Scenario (W : Type u_1) (U : Type u_2) (A : Type u_3) : Type (max (max u_1 u_2) u_3)

A discourse situation records the meanings of the alternatives and their structural complexity, the context, and the question, a family of answers.

• meaning : U → Set W
• complexity : U → ℕ
• context : Set W
• question : A → Set W

def KatzirSingh2015.Scenario.Settled {W : Type u_1} {U : Type u_2} {A : Type u_3} (s : Scenario W U A) : Prop

The question is settled in the context when its live answers there coincide.

Equations

• s.Settled = ∀ (a b : A), (∃ w ∈ s.context, w ∈ s.question a) → (∃ w ∈ s.context, w ∈ s.question b) → ∀ w ∈ s.context, w ∈ s.question a ↔ w ∈ s.question b

def KatzirSingh2015.Scenario.Relevant {W : Type u_1} {U : Type u_2} {A : Type u_3} (s : Scenario W U A) (u : U) : Prop

An assertion is relevant to the question when, within the context, it does not split a cell of the partition the answers induce.

Equations

• s.Relevant u = ∀ w ∈ s.context, ∀ v ∈ s.context, (∀ (a : A), w ∈ s.question a ↔ v ∈ s.question a) → (w ∈ s.meaning u ↔ v ∈ s.meaning u)

def KatzirSingh2015.Scenario.AtLeastAsGood {W : Type u_1} {U : Type u_2} {A : Type u_3} (s : Scenario W U A) (u v : U) : Prop

An alternative is at least as good (16a) when it is at most as complex and at least as strong.

Equations

• s.AtLeastAsGood u v = (s.complexity u ≤ s.complexity v ∧ s.meaning u ⊆ s.meaning v)

def KatzirSingh2015.Scenario.Better {W : Type u_1} {U : Type u_2} {A : Type u_3} (s : Scenario W U A) (u v : U) : Prop

An alternative is better (16b) when it is at least as good and not conversely.

Equations

• s.Better u v = (s.AtLeastAsGood u v ∧ ¬s.AtLeastAsGood v u)

def KatzirSingh2015.Scenario.GoodAnswer {W : Type u_1} {U : Type u_2} {A : Type u_3} (s : Scenario W U A) (u : U) (w : W) : Prop

A good answer at w (15) is true, relevant, and not needlessly worse than a true relevant alternative.

Equations

• s.GoodAnswer u w = (w ∈ s.meaning u ∧ s.Relevant u ∧ ¬∃ (v : U), s.Better v u ∧ w ∈ s.meaning v ∧ s.Relevant v)

def KatzirSingh2015.Scenario.Felicitous {W : Type u_1} {U : Type u_2} {A : Type u_3} (s : Scenario W U A) (u : U) (w : W) : Prop

An assertion is felicitous at w when the question is not settled (8) and the assertion is a good answer (15).

Equations

• s.Felicitous u w = (¬s.Settled ∧ s.GoodAnswer u w)

@[instance_reducible]

instance KatzirSingh2015.Scenario.instDecidableSettled {W : Type u_1} {U : Type u_2} {A : Type u_3} (s : Scenario W U A) [Fintype W] [Fintype A] [DecidablePred fun (x : W) => x ∈ s.context] [(a : A) → DecidablePred fun (x : W) => x ∈ s.question a] : Decidable s.Settled

Equations

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

@[instance_reducible]

instance KatzirSingh2015.Scenario.instDecidableRelevant {W : Type u_1} {U : Type u_2} {A : Type u_3} (s : Scenario W U A) [Fintype W] [Fintype A] [(u : U) → DecidablePred fun (x : W) => x ∈ s.meaning u] [DecidablePred fun (x : W) => x ∈ s.context] [(a : A) → DecidablePred fun (x : W) => x ∈ s.question a] (u : U) : Decidable (s.Relevant u)

Equations

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

@[instance_reducible]

instance KatzirSingh2015.Scenario.instDecidableAtLeastAsGood {W : Type u_1} {U : Type u_2} {A : Type u_3} (s : Scenario W U A) [Fintype W] [(u : U) → DecidablePred fun (x : W) => x ∈ s.meaning u] (u v : U) : Decidable (s.AtLeastAsGood u v)

Equations

• s.instDecidableAtLeastAsGood u v = { decide := decide (s.complexity u ≤ s.complexity v) && decide (∀ x ∈ s.meaning u, x ∈ s.meaning v), reflects_decide := ⋯ }

@[instance_reducible]

instance KatzirSingh2015.Scenario.instDecidableBetter {W : Type u_1} {U : Type u_2} {A : Type u_3} (s : Scenario W U A) [Fintype W] [(u : U) → DecidablePred fun (x : W) => x ∈ s.meaning u] (u v : U) : Decidable (s.Better u v)

Equations

• s.instDecidableBetter u v = { decide := decide (s.AtLeastAsGood u v) && decide ¬s.AtLeastAsGood v u, reflects_decide := ⋯ }

@[instance_reducible]

instance KatzirSingh2015.Scenario.instDecidableGoodAnswer {W : Type u_1} {U : Type u_2} {A : Type u_3} (s : Scenario W U A) [Fintype W] [Fintype U] [Fintype A] [(u : U) → DecidablePred fun (x : W) => x ∈ s.meaning u] [DecidablePred fun (x : W) => x ∈ s.context] [(a : A) → DecidablePred fun (x : W) => x ∈ s.question a] (u : U) (w : W) : Decidable (s.GoodAnswer u w)

Equations

• s.instDecidableGoodAnswer u w = { decide := decide (w ∈ s.meaning u) && decide (s.Relevant u ∧ ¬∃ (x : U), s.Better x u ∧ w ∈ s.meaning x ∧ s.Relevant x), reflects_decide := ⋯ }

@[instance_reducible]

instance KatzirSingh2015.Scenario.instDecidableFelicitous {W : Type u_1} {U : Type u_2} {A : Type u_3} (s : Scenario W U A) [Fintype W] [Fintype U] [Fintype A] [(u : U) → DecidablePred fun (x : W) => x ∈ s.meaning u] [DecidablePred fun (x : W) => x ∈ s.context] [(a : A) → DecidablePred fun (x : W) => x ∈ s.question a] (u : U) (w : W) : Decidable (s.Felicitous u w)

Equations

• s.instDecidableFelicitous u w = { decide := decide ¬s.Settled && decide (s.GoodAnswer u w), reflects_decide := ⋯ }

theorem KatzirSingh2015.Scenario.atLeastAsGood_refl {W : Type u_1} {U : Type u_2} {A : Type u_3} (s : Scenario W U A) (u : U) : s.AtLeastAsGood u u

theorem KatzirSingh2015.Scenario.atLeastAsGood_trans {W : Type u_1} {U : Type u_2} {A : Type u_3} (s : Scenario W U A) {u v x : U} (h : s.AtLeastAsGood u v) (h' : s.AtLeastAsGood v x) : s.AtLeastAsGood u x

theorem KatzirSingh2015.Scenario.better_irrefl {W : Type u_1} {U : Type u_2} {A : Type u_3} (s : Scenario W U A) (u : U) : ¬s.Better u u

theorem KatzirSingh2015.Scenario.better_asymm {W : Type u_1} {U : Type u_2} {A : Type u_3} (s : Scenario W U A) {u v : U} (h : s.Better u v) : ¬s.Better v u

theorem KatzirSingh2015.Scenario.better_trans {W : Type u_1} {U : Type u_2} {A : Type u_3} (s : Scenario W U A) {u v x : U} (h : s.Better u v) (h' : s.Better v x) : s.Better u x

Better-than is a strict order, the irreflexive part of the at-least-as-good preorder.

theorem KatzirSingh2015.Scenario.not_goodAnswer_of_stronger {W : Type u_1} {U : Type u_2} {A : Type u_3} (s : Scenario W U A) {u v : U} {w : W} (hc : s.complexity v ≤ s.complexity u) (hs : s.meaning v ⊂ s.meaning u) (hw : w ∈ s.meaning v) (hr : s.Relevant v) : ¬s.GoodAnswer u w

An answer is needlessly weak, and so not good, when a true relevant alternative of no greater complexity is strictly stronger.

theorem KatzirSingh2015.Scenario.not_goodAnswer_disj {W : Type u_1} {U : Type u_2} {A : Type u_3} (s : Scenario W U A) {d φ ψ : U} {w : W} (hd : s.meaning d = s.meaning φ ∪ s.meaning ψ) (hψ : s.meaning ψ ⊆ s.meaning φ) (hc : s.complexity φ < s.complexity d) (hw : w ∈ s.meaning φ) (hr : s.Relevant φ) : ¬s.GoodAnswer d w

A disjunction whose second disjunct entails the first says what the first does at greater complexity, so it is a needlessly complex answer (22) where the first disjunct is a true relevant one.

theorem KatzirSingh2015.Scenario.not_goodAnswer_conj {W : Type u_1} {U : Type u_2} {A : Type u_3} (s : Scenario W U A) {c φ ψ : U} {w : W} (hc' : s.meaning c = s.meaning φ ∩ s.meaning ψ) (hψ : s.meaning φ ⊆ s.meaning ψ) (hc : s.complexity φ < s.complexity c) (hw : w ∈ s.meaning φ) (hr : s.Relevant φ) : ¬s.GoodAnswer c w

Likewise a conjunction whose second conjunct is entailed by the first, (23).

Some and all (Sections 1 and 3.2)

The some and all alternatives over the three ways a set of grades, names or origins can fall, the vertices of the triangle of opposition (Aristotelian.Triangle): to none (E), to some but not all (IO), or to all (A).

inductive KatzirSingh2015.Scalar : Type

The scalar alternatives.

• some_ : Scalar
• all_ : Scalar

@[instance_reducible]

instance KatzirSingh2015.instDecidableEqScalar : DecidableEq Scalar

Equations

• KatzirSingh2015.instDecidableEqScalar x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def KatzirSingh2015.instReprScalar.repr : Scalar → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance KatzirSingh2015.instReprScalar : Repr Scalar

Equations

• KatzirSingh2015.instReprScalar = { reprPrec := KatzirSingh2015.instReprScalar.repr }

@[instance_reducible]

instance KatzirSingh2015.instFintypeScalar : Fintype Scalar

Equations

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

def KatzirSingh2015.scalarDenotes : Scalar → Aristotelian.Triangle → Prop

Some is true above the bottom vertex, all only at the top one.

Equations

• KatzirSingh2015.scalarDenotes KatzirSingh2015.Scalar.some_ x✝ = (⊥ < x✝)
• KatzirSingh2015.scalarDenotes KatzirSingh2015.Scalar.all_ x✝ = (x✝ = ⊤)

@[instance_reducible]

instance KatzirSingh2015.instDecidableScalarDenotes (u : Scalar) (w : Aristotelian.Triangle) : Decidable (scalarDenotes u w)

Equations

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

@[reducible, inline]

abbrev KatzirSingh2015.scalar (context : Set Aristotelian.Triangle) : Scenario Aristotelian.Triangle Scalar Scalar

In the scalar scenario the alternatives form the question and have the same complexity, the context being a parameter.

Equations

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

theorem KatzirSingh2015.some_all_odd_of_settled : (scalar {w : Aristotelian.Triangle | w ≠ Aristotelian.Triangle.IO}).Settled ∧ ∀ (u : Scalar) (w : Aristotelian.Triangle), ¬(scalar {w : Aristotelian.Triangle | w ≠ Aristotelian.Triangle.IO}).Felicitous u w

Where the context makes some and all equivalent, as common knowledge that Italy is warm or that every father names all his children alike does in (1) and (19), the question they form has one live answer and both are odd.

theorem KatzirSingh2015.all_felicitous_some_odd : (scalar Set.univ).Felicitous Scalar.all_ Aristotelian.Triangle.A ∧ ¬(scalar Set.univ).Felicitous Scalar.some_ Aristotelian.Triangle.A

Where the equivalence is the speaker's belief rather than common knowledge (17), the question is open, and where the property holds of all all is a good answer while some is needlessly weak.

@[reducible, inline]

abbrev KatzirSingh2015.explicit : Scenario Aristotelian.Triangle Scalar Aristotelian.Triangle

The explicit question to how many? of (20) is not settled by the common knowledge of (19), and all becomes a good answer while some stays needlessly weak.

Equations

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

theorem KatzirSingh2015.explicit_question_rescues_all : ¬explicit.Settled ∧ explicit.Felicitous Scalar.all_ Aristotelian.Triangle.A ∧ ¬explicit.Felicitous Scalar.some_ Aristotelian.Triangle.A

def KatzirSingh2015.restrictorDenotes : Scalar → Aristotelian.Triangle → Prop

Under a downward-entailing operator (18) the entailment reverses, some being the stronger, and it is all that is needlessly weak.

Equations

• KatzirSingh2015.restrictorDenotes KatzirSingh2015.Scalar.some_ x✝ = (x✝ = ⊤)
• KatzirSingh2015.restrictorDenotes KatzirSingh2015.Scalar.all_ x✝ = (⊥ < x✝)

@[instance_reducible]

instance KatzirSingh2015.instDecidableRestrictorDenotes (u : Scalar) (w : Aristotelian.Triangle) : Decidable (restrictorDenotes u w)

Equations

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

@[reducible, inline]

abbrev KatzirSingh2015.restrictor : Scenario Aristotelian.Triangle Scalar Scalar

The scenario of (18) asserts that every professor who assigned an A to some or all of his students got a raise, over how many of the A-givers got one.

Equations

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

theorem KatzirSingh2015.some_felicitous_all_odd : restrictor.Felicitous Scalar.some_ Aristotelian.Triangle.A ∧ ¬restrictor.Felicitous Scalar.all_ Aristotelian.Triangle.A

Maximize Presupposition (Section 3.2.3)

inductive KatzirSingh2015.Sky : Type

How many suns there are and whether one shines.

• oneShining : Sky
• oneDark : Sky
• many : Sky

@[instance_reducible]

instance KatzirSingh2015.instDecidableEqSky : DecidableEq Sky

Equations

• KatzirSingh2015.instDecidableEqSky x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance KatzirSingh2015.instReprSky : Repr Sky

Equations

• KatzirSingh2015.instReprSky = { reprPrec := KatzirSingh2015.instReprSky.repr }

def KatzirSingh2015.instReprSky.repr : Sky → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• KatzirSingh2015.instReprSky.repr KatzirSingh2015.Sky.many prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "KatzirSingh2015.Sky.many")).group prec✝

@[instance_reducible]

instance KatzirSingh2015.instFintypeSky : Fintype Sky

Equations

• KatzirSingh2015.instFintypeSky = { elems := { val := ↑KatzirSingh2015.Sky.enumList, nodup := KatzirSingh2015.Sky.enumList_nodup }, complete := KatzirSingh2015.instFintypeSky._proof_1 }

inductive KatzirSingh2015.Article : Type

A sun is shining and the sun is shining.

• a : Article
• the : Article

@[instance_reducible]

instance KatzirSingh2015.instDecidableEqArticle : DecidableEq Article

Equations

• KatzirSingh2015.instDecidableEqArticle x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def KatzirSingh2015.instReprArticle.repr : Article → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance KatzirSingh2015.instReprArticle : Repr Article

Equations

• KatzirSingh2015.instReprArticle = { reprPrec := KatzirSingh2015.instReprArticle.repr }

@[instance_reducible]

instance KatzirSingh2015.instFintypeArticle : Fintype Article

Equations

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

def KatzirSingh2015.articleDenotes : Article → Sky → Prop

The definite carries the uniqueness presupposition into its truth conditions.

Equations

• KatzirSingh2015.articleDenotes KatzirSingh2015.Article.a x✝ = (x✝ ≠ KatzirSingh2015.Sky.oneDark)
• KatzirSingh2015.articleDenotes KatzirSingh2015.Article.the x✝ = (x✝ = KatzirSingh2015.Sky.oneShining)

@[instance_reducible]

instance KatzirSingh2015.instDecidableArticleDenotes (u : Article) (w : Sky) : Decidable (articleDenotes u w)

Equations

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

@[reducible, inline]

abbrev KatzirSingh2015.sun : Scenario Sky Article Bool

(21) with common knowledge of one sun, the question being whether it shines.

Equations

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

theorem KatzirSingh2015.the_felicitous_a_odd : sun.Felicitous Article.the Sky.oneShining ∧ ¬sun.Felicitous Article.a Sky.oneShining

Maximize Presupposition is an instance of the answer condition, the definite being the better answer and the indefinite needlessly weak.

Hurford disjunctions (Section 3.3)

inductive KatzirSingh2015.Trip : Type

Where John went.

• paris : Trip
• franceNotParis : Trip
• elsewhere : Trip

@[instance_reducible]

instance KatzirSingh2015.instDecidableEqTrip : DecidableEq Trip

Equations

• KatzirSingh2015.instDecidableEqTrip x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def KatzirSingh2015.instReprTrip.repr : Trip → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance KatzirSingh2015.instReprTrip : Repr Trip

Equations

• KatzirSingh2015.instReprTrip = { reprPrec := KatzirSingh2015.instReprTrip.repr }

@[instance_reducible]

instance KatzirSingh2015.instFintypeTrip : Fintype Trip

Equations

• KatzirSingh2015.instFintypeTrip = { elems := { val := ↑KatzirSingh2015.Trip.enumList, nodup := KatzirSingh2015.Trip.enumList_nodup }, complete := KatzirSingh2015.instFintypeTrip._proof_1 }

inductive KatzirSingh2015.Visit : Type

John visited France, and the disjunction (22) with Paris.

• france : Visit
• franceOrParis : Visit

@[instance_reducible]

instance KatzirSingh2015.instDecidableEqVisit : DecidableEq Visit

Equations

• KatzirSingh2015.instDecidableEqVisit x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def KatzirSingh2015.instReprVisit.repr : Visit → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance KatzirSingh2015.instReprVisit : Repr Visit

Equations

• KatzirSingh2015.instReprVisit = { reprPrec := KatzirSingh2015.instReprVisit.repr }

@[instance_reducible]

instance KatzirSingh2015.instFintypeVisit : Fintype Visit

Equations

• KatzirSingh2015.instFintypeVisit = { elems := { val := ↑KatzirSingh2015.Visit.enumList, nodup := KatzirSingh2015.Visit.enumList_nodup }, complete := KatzirSingh2015.instFintypeVisit._proof_1 }

def KatzirSingh2015.visitDenotes : Visit → Trip → Prop

Equations

• KatzirSingh2015.visitDenotes KatzirSingh2015.Visit.france x✝ = (x✝ ≠ KatzirSingh2015.Trip.elsewhere)
• KatzirSingh2015.visitDenotes KatzirSingh2015.Visit.franceOrParis x✝ = (x✝ ≠ KatzirSingh2015.Trip.elsewhere)

@[instance_reducible]

instance KatzirSingh2015.instDecidableVisitDenotes (u : Visit) (w : Trip) : Decidable (visitDenotes u w)

Equations

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

@[reducible, inline]

abbrev KatzirSingh2015.hurford : Scenario Trip Visit Trip

In (22) the disjunction is more complex than its first disjunct, and the question is where John went.

Equations

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

theorem KatzirSingh2015.hurford_odd (w : Trip) : ¬hurford.Felicitous Visit.franceOrParis w

France or Paris is a needlessly complex answer wherever France is true.

theorem KatzirSingh2015.france_felicitous : hurford.Felicitous Visit.france Trip.paris

France is a good answer where true.