Kratzer (1977) — Premise semantics worked example

[Kra77] [Kra12]

A concrete formalization of the New Zealand judgments scenario from §1.3 of [Kra77] (= Chapter 1 of [Kra12]), exercising the API of Intensional.Premise.

The scenario

[Kra77] imagines a country whose entire common law consists of three judgments:

1. Murder is a crime. — call this proposition p.
2. Deer are personally responsible for damage they inflict on young trees. — call this proposition q.
3. Deer are not personally responsible for damage they inflict on young trees. — proposition ¬q.

The premise set A = [p, q, ¬q] is inconsistent (its intersection is empty: no world makes q and ¬q both true). Yet our intuitions about modal claims relativized to what the New Zealand judgments provide are crisp:

• (7) "Murder must be a crime." — TRUE
• (8) "It must be that murder is not a crime." — FALSE
• (9) "It is possible that deer are responsible." — TRUE
• (10) "It is possible that deer are not responsible." — TRUE
• (14) "It is possible that murder is not a crime." — FALSE

Kratzer's original Defs 5–6 (necessity = consequence, possibility = compatibility) collapse on inconsistent A: by ex falso quodlibet, everything follows from A, so must p and must ¬p are both true, and nothing is compatible with A, so can q and can ¬q are both false. Defs 7–8 — quantifying over the consistent subsets of A and asking for an extension that supports the conclusion — recover the intuitive predictions.

What this study is

A Phenomenon-layer integration test for Intensional.Premise: it picks the worked example Kratzer uses to motivate the revision from Defs 5–6 to Defs 7–8 and verifies, by structural proofs over the four-world frame, that the formalization gets each prediction right and that the unrevised definitions fail in exactly the way Kratzer says they do.

§1. The model

A four-world frame, indexed by Fin 4, that distinguishes the two contingent dimensions of the scenario: whether murder is a crime (p) and whether deer are responsible (q). All four combinations are represented so that every singleton premise — p, q, ¬q, ¬p — is individually consistent.

world	p (murder is a crime)	q (deer responsible)
w₀	true	true
w₁	true	false
w₂	false	true
w₃	false	false

def Kratzer1977.p : Fin 4 → Prop

"Murder is a crime." True at w₀ and w₁.

Equations

• Kratzer1977.p 0 = True
• Kratzer1977.p 1 = True
• Kratzer1977.p 2 = False
• Kratzer1977.p 3 = False

def Kratzer1977.q : Fin 4 → Prop

"Deer are personally responsible for damage they inflict on young trees." True at w₀ and w₂.

Equations

• Kratzer1977.q 0 = True
• Kratzer1977.q 1 = False
• Kratzer1977.q 2 = True
• Kratzer1977.q 3 = False

def Kratzer1977.negQ : Fin 4 → Prop

"Deer are not personally responsible…" — the negation of q.

Equations

• Kratzer1977.negQ w = ¬Kratzer1977.q w

def Kratzer1977.negP : Fin 4 → Prop

"Murder is not a crime." The negation of p.

Equations

• Kratzer1977.negP w = ¬Kratzer1977.p w

def Kratzer1977.A : List (Fin 4 → Prop)

The premise set A of [Kra77] §1.3 — what the New Zealand judgments provide: the three rulings, taken together.

Equations

• Kratzer1977.A = [Kratzer1977.p, Kratzer1977.q, Kratzer1977.negQ]

def Kratzer1977.f : Fin 4 → List (Fin 4 → Prop)

The constant modal restriction: at every world, the premise set is A. The scenario abstracts away from world-to-world variation in the judgments.

Equations

• Kratzer1977.f x✝ = Kratzer1977.A

Membership lemmas: each judgment is in A.

theorem Kratzer1977.p_mem_A : p ∈ A

theorem Kratzer1977.q_mem_A : q ∈ A

theorem Kratzer1977.negQ_mem_A : negQ ∈ A

§2. A is inconsistent

The premise set contains both q and its negation, so its intersection is empty.

theorem Kratzer1977.A_inconsistent : ¬Intensional.Premise.isConsistent A

§3. Unrevised Defs 5–6 give paradoxical predictions

These two theorems are the formal counterpart of Kratzer's diagnosis of the original definitions: they trivialize over an inconsistent A.

theorem Kratzer1977.must_negP_under_def5 : Intensional.Premise.mustInView f negP 0

Under the original Def 5 (mustInView), the inconsistent A entails every proposition — including ¬p. This is the paradox of ex falso quodlibet that motivates the revision to Def 7.

theorem Kratzer1977.can_q_under_def6 : ¬Intensional.Premise.canInView f q 0

Under the original Def 6 (canInView), nothing is compatible with the inconsistent A — including q, which intuitively is possible in view of the judgments.

§4. Revised Defs 7–8 give the intuitive predictions

Each theorem corresponds to a sentence number from [Kra77] §1.3, with the predicted truth value Kratzer argues for.

The proofs proceed by enumerating the consistent sublists of A and, for each one, exhibiting an extension that witnesses (or refutes) the target consequence.

Membership helpers for the four worlds

@[simp]

theorem Kratzer1977.p_zero : p 0

@[simp]

theorem Kratzer1977.p_one : p 1

@[simp]

theorem Kratzer1977.not_p_two : ¬p 2

@[simp]

theorem Kratzer1977.not_p_three : ¬p 3

@[simp]

theorem Kratzer1977.q_zero : q 0

@[simp]

theorem Kratzer1977.not_q_one : ¬q 1

@[simp]

theorem Kratzer1977.q_two : q 2

@[simp]

theorem Kratzer1977.not_q_three : ¬q 3

@[simp]

theorem Kratzer1977.negQ_one : negQ 1

@[simp]

theorem Kratzer1977.negQ_three : negQ 3

Consistency of relevant sublists of A

theorem Kratzer1977.cons_singleton_p : Intensional.Premise.isConsistent [p]

theorem Kratzer1977.cons_singleton_q : Intensional.Premise.isConsistent [q]

theorem Kratzer1977.cons_singleton_negQ : Intensional.Premise.isConsistent [negQ]

theorem Kratzer1977.cons_pair_pq : Intensional.Premise.isConsistent [p, q]

theorem Kratzer1977.cons_pair_pnegQ : Intensional.Premise.isConsistent [p, negQ]

Sublist enumeration

Every sublist of A = [p, q, negQ] has every element drawn from {p, q, negQ}.

theorem Kratzer1977.mem_of_sublist_A {B : List (Fin 4 → Prop)} (hB : B ∈ A.sublists) {x : Fin 4 → Prop} (hx : x ∈ B) : x = p ∨ x = q ∨ x = negQ

theorem Kratzer1977.not_q_and_negQ {B : List (Fin 4 → Prop)} (hCons : Intensional.Premise.isConsistent B) (hq : q ∈ B) (hnq : negQ ∈ B) : False

A consistent sublist of A cannot contain both q and negQ.

Sublist relations against A = [p, q, negQ]

theorem Kratzer1977.pq_sublist_A : [p, q] ∈ A.sublists

[p, q] is a sublist of [p, q, negQ] (drop negQ).

theorem Kratzer1977.pnegQ_sublist_A : [p, negQ] ∈ A.sublists

[p, negQ] is a sublist of [p, q, negQ] (drop q).

theorem Kratzer1977.p_sublist_A : [p] ∈ A.sublists

[p] is a sublist of [p, q, negQ].

theorem Kratzer1977.q_sublist_A : [q] ∈ A.sublists

[q] is a sublist of [p, q, negQ].

theorem Kratzer1977.negQ_sublist_A : [negQ] ∈ A.sublists

[negQ] is a sublist of [p, q, negQ].

theorem Kratzer1977.nil_sublist_A : [] ∈ A.sublists

The empty list is a sublist of A.

Witness selection for the revised must/can theorems

theorem Kratzer1977.exists_extension_with_p {B : List (Fin 4 → Prop)} (hBSub : B ∈ A.sublists) (hBCons : Intensional.Premise.isConsistent B) : ∃ C ∈ A.sublists, Intensional.Premise.isConsistent C ∧ B ⊆ C ∧ p ∈ C

For any consistent sublist B of A, exhibit a consistent sublist C of A with B ⊆ C and p ∈ C. We use [p, q] if B does not contain negQ, and [p, negQ] otherwise.

theorem Kratzer1977.followsFrom_p_of_mem {C : List (Fin 4 → Prop)} (hp : p ∈ C) : Intensional.Premise.followsFrom p C

Any list containing p entails p: ⋂ C ⊆ propExtension p.

theorem Kratzer1977.sentence_7_must_p : Intensional.Premise.mustInView' f p 0

(7) "Murder must be a crime" — TRUE under Def 7. The extension [p, q] (or [p, ¬q]) of any consistent subset of A entails p.

theorem Kratzer1977.sentence_8_not_must_negP : ¬Intensional.Premise.mustInView' f negP 0

(8) "It must be that murder is not a crime" — FALSE under Def 7. Apply Def 7 at B = [p]; any consistent extension C ⊇ [p] of A contains p, but negP cannot follow from C because C admits a witness world (0 if q ∈ C, else 1) where p holds, hence negP fails.

theorem Kratzer1977.sentence_9_can_q : Intensional.Premise.canInView' f q 0

(9) "It is possible that deer are responsible" — TRUE under Def 8. Witness: take B = [q]; every consistent extension already contains q, so adding q preserves consistency.

theorem Kratzer1977.sentence_10_can_negQ : Intensional.Premise.canInView' f negQ 0

(10) "It is possible that deer are not responsible" — TRUE under Def 8. Symmetric to (9), with witness B = [¬q].

theorem Kratzer1977.sentence_14_not_can_negP : ¬Intensional.Premise.canInView' f negP 0

(14) "It is possible that murder is not a crime" — FALSE under Def 8. Every consistent subset of A extends to one containing p, and adding ¬p to such a set is never consistent.

§5. The contrast in one place

Two theorems pinning the bug-vs-fix asymmetry: the revised definitions agree with intuition exactly where the original definitions trivialize.

theorem Kratzer1977.def5_vs_def7_negP : Intensional.Premise.mustInView f negP 0 ∧ ¬Intensional.Premise.mustInView' f negP 0

Def 5 wrongly accepts must ¬p; Def 7 correctly rejects it.

theorem Kratzer1977.def6_vs_def8_q : ¬Intensional.Premise.canInView f q 0 ∧ Intensional.Premise.canInView' f q 0

Def 6 wrongly rejects can q; Def 8 correctly accepts it.