Klinedinst and Rothschild (2012): Connectives without Truth Tables

This file formalizes Klinedinst and Rothschild's parameter treatment of the dynamic effects of and and or. Truth is relative to a world and to an information parameter, the set of worlds that epistemic modals quantify over, (46) and (47), the domain semantics of Yalcin (Yalcin2007.Sentence), and the connectives shift that parameter for their second clause: a and b evaluates b against the parameter updated with a, (49), and a or b against the parameter updated with the negation of a, (50) (conj, disj). This is what lets an epistemic modal sit in a disjunct: the dog is in the backyard or it must be in the kitchen, (36), says that the dog is in the backyard or that the information, given that it is not, puts it in the kitchen (disj_must_iff), disjunctive syllogism fails for it, (38)–(40) (not_disjunctive_syllogism), and so does commutation, (104) (disj_not_comm). The non-truth-tabular uses of §1 are the assertion forms of (60) that keep only the dynamic effect: and with its first clause shifting the parameter alone is the conditional of (52), (61) and (62), and or with both clauses entailed asserts its first disjunct and the second under the negation of the first, (66) and (67) (Use.interpret); the other two forms collapse into the normal connectives (doubleEntailment_and, shift_disj). A normal conjunction whose second conjunct needs worlds where the first fails is a contradiction, (68) (not_conj_might_compl).

Implementation notes

• The context parameter and the presuppositional definedness of (48) are omitted, as is the inner and outer sphere refinement of §4.2 for counterfactual morphology; a sentence is a function of the information parameter and the world.

References

• [KR12b]
• [Yal07]

def KlinedinstRothschild2012.update {W : Type u_1} (a : Yalcin2007.Sentence W) (s : Set W) : Set W

The information parameter updated with a, the sᵃ of §4.

Equations

• KlinedinstRothschild2012.update a s = {w' : W | w' ∈ s ∧ a s w'}

def KlinedinstRothschild2012.conj {W : Type u_1} (a b : Yalcin2007.Sentence W) : Yalcin2007.Sentence W

Conjunction, (49), evaluates the second conjunct against the parameter updated with the first.

Equations

• KlinedinstRothschild2012.conj a b s w = (a s w ∧ b (KlinedinstRothschild2012.update a s) w)

def KlinedinstRothschild2012.disj {W : Type u_1} (a b : Yalcin2007.Sentence W) : Yalcin2007.Sentence W

Disjunction, (50), evaluates the second disjunct against the parameter updated with the negation of the first.

Equations

• KlinedinstRothschild2012.disj a b s w = (a s w ∨ b (KlinedinstRothschild2012.update aᶜ s) w)

def KlinedinstRothschild2012.ifThen {W : Type u_1} (a b : Yalcin2007.Sentence W) : Yalcin2007.Sentence W

In the conditional, (52), the antecedent shifts the parameter, and a modal in the consequent quantifies over the result.

Equations

• KlinedinstRothschild2012.ifThen a b s w = b (KlinedinstRothschild2012.update a s) w

Epistemic modals under or, §3.2

theorem KlinedinstRothschild2012.disj_must_iff {W : Type u_1} (p q s : Set W) (w : W) : disj (Yalcin2007.Sentence.ofProp p) (Yalcin2007.Sentence.ofProp q).must s w ↔ w ∈ p ∨ ∀ w' ∈ s, w' ∉ p → w' ∈ q

(36): the dog is in the backyard or it must be in the kitchen is a disjunction of the first disjunct with the report that the information, given that the dog is not in the backyard, puts it in the kitchen.

theorem KlinedinstRothschild2012.disjunctive_syllogism {W : Type u_1} (p q : Set W) : Yalcin2007.StandardConsequence [disj (Yalcin2007.Sentence.ofProp p) (Yalcin2007.Sentence.ofProp q), (Yalcin2007.Sentence.ofProp q)ᶜ] (Yalcin2007.Sentence.ofProp p)

Disjunctive syllogism holds for factual disjuncts.

theorem KlinedinstRothschild2012.not_disjunctive_syllogism : ¬Yalcin2007.StandardConsequence [disj (Yalcin2007.Sentence.ofProp {true}) (Yalcin2007.Sentence.ofProp {false}).must, (Yalcin2007.Sentence.ofProp {false}).mustᶜ] (Yalcin2007.Sentence.ofProp {true})

(38)–(40): disjunctive syllogism fails with the modal disjunct. On the two-world model, the dog inside in one world and outside in the other, the disjunction the dog is inside or it must be outside and it's not the case that it must be outside both hold at the outside world, where the dog is not inside.

theorem KlinedinstRothschild2012.disj_not_comm : ¬∀ (a b : Yalcin2007.Sentence Bool) (s : Set Bool) (w : Bool), disj a b s w ↔ disj b a s w

(104): the dynamic effect is asymmetric, so the disjuncts do not commute: with the modal disjunct first, the same model falsifies the disjunction.

The assertion forms of (60), §5

inductive KlinedinstRothschild2012.Connective : Type

The connective whose dynamic effect is kept.

• and : Connective
• or : Connective

@[instance_reducible]

instance KlinedinstRothschild2012.instDecidableEqConnective : DecidableEq Connective

Equations

• KlinedinstRothschild2012.instDecidableEqConnective x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def KlinedinstRothschild2012.instReprConnective.repr : Connective → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance KlinedinstRothschild2012.instReprConnective : Repr Connective

Equations

• KlinedinstRothschild2012.instReprConnective = { reprPrec := KlinedinstRothschild2012.instReprConnective.repr }

inductive KlinedinstRothschild2012.Use : Type

The three assertion forms of a ∗ b, (60), are the normal connective, both clauses entailed with the second under the shifted parameter, or the first clause used only to shift the parameter of the second.

• normal : Use
• doubleEntailment : Use
• shift : Use

@[instance_reducible]

instance KlinedinstRothschild2012.instDecidableEqUse : DecidableEq Use

Equations

• KlinedinstRothschild2012.instDecidableEqUse x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def KlinedinstRothschild2012.instReprUse.repr : Use → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance KlinedinstRothschild2012.instReprUse : Repr Use

Equations

• KlinedinstRothschild2012.instReprUse = { reprPrec := KlinedinstRothschild2012.instReprUse.repr }

def KlinedinstRothschild2012.Connective.shift {W : Type u_1} : Connective → Yalcin2007.Sentence W → Set W → Set W

The parameter the second clause is evaluated under, (49) and (50).

Equations

• KlinedinstRothschild2012.Connective.and.shift x✝¹ x✝ = KlinedinstRothschild2012.update x✝¹ x✝
• KlinedinstRothschild2012.Connective.or.shift x✝¹ x✝ = KlinedinstRothschild2012.update x✝¹ᶜ x✝

def KlinedinstRothschild2012.Use.interpret {W : Type u_1} : Use → Connective → Yalcin2007.Sentence W → Yalcin2007.Sentence W → Yalcin2007.Sentence W

The content of a ∗ b on each assertion form, the table of (60).

Equations

• KlinedinstRothschild2012.Use.normal.interpret KlinedinstRothschild2012.Connective.and x✝¹ x✝ = KlinedinstRothschild2012.conj x✝¹ x✝
• KlinedinstRothschild2012.Use.normal.interpret KlinedinstRothschild2012.Connective.or x✝¹ x✝ = KlinedinstRothschild2012.disj x✝¹ x✝
• KlinedinstRothschild2012.Use.doubleEntailment.interpret x✝² x✝¹ x✝ = fun (s : Set W) (w : W) => x✝¹ s w ∧ x✝ (x✝².shift x✝¹ s) w
• KlinedinstRothschild2012.Use.shift.interpret x✝² x✝¹ x✝ = fun (s : Set W) (w : W) => x✝ (x✝².shift x✝¹ s) w

theorem KlinedinstRothschild2012.doubleEntailment_and {W : Type u_1} (a b : Yalcin2007.Sentence W) : Use.doubleEntailment.interpret Connective.and a b = conj a b

Double entailment of and reproduces the normal conjunction.

theorem KlinedinstRothschild2012.shift_disj {W : Type u_1} (a b : Yalcin2007.Sentence W) : Use.shift.interpret Connective.or a b = ifThen aᶜ b

The parameter-shifting or is the conditional on the negation of its first disjunct.

theorem KlinedinstRothschild2012.shift_and {W : Type u_1} (a b : Yalcin2007.Sentence W) : Use.shift.interpret Connective.and a b = ifThen a b

The non-truth-tabular and, (1): the first conjunct only shifts the parameter, which is the conditional of (52).

theorem KlinedinstRothschild2012.doubleEntailment_disj {W : Type u_1} (a b : Yalcin2007.Sentence W) : Use.doubleEntailment.interpret Connective.or a b = fun (s : Set W) (w : W) => a s w ∧ b (update aᶜ s) w

The non-truth-tabular or, (2) and (66): the first disjunct is asserted, and the second under the parameter updated with its negation, (67).

theorem KlinedinstRothschild2012.cond_might_iff {W : Type u_1} (p t s : Set W) (w : W) : ifThen (Yalcin2007.Sentence.ofProp p) (Yalcin2007.Sentence.ofProp t).might s w ↔ ∃ w' ∈ s, w' ∈ p ∧ w' ∈ t

(61) and (62): the police show up, and there might be trouble is true when some world of the parameter in which the police show up is one with trouble.

theorem KlinedinstRothschild2012.not_conj_might_compl {W : Type u_1} (p s : Set W) (w : W) : ¬conj (Yalcin2007.Sentence.ofProp p) (Yalcin2007.Sentence.ofProp p)ᶜ.might s w

(68): John is here and he might not be is a contradiction, the second conjunct needing a parameter with worlds in which the first fails.