Documentation

Linglib.Phenomena.Modality.Studies.Kratzer1977

Kratzer (1977) — Premise semantics worked example #

@cite{kratzer-1977} @cite{kratzer-2012}

A concrete formalization of the New Zealand judgments scenario from §1.3 of @cite{kratzer-1977} (= Chapter 1 of @cite{kratzer-2012}), exercising the API of Core.Logic.Intensional.Premise.

The scenario #

@cite{kratzer-1977} 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:

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 Core.Logic.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.

worldp (murder is a crime)q (deer responsible)
w₀truetrue
w₁truefalse
w₂falsetrue
w₃falsefalse

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

Equations
Instances For

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

    Equations
    Instances For

      The premise set A of @cite{kratzer-1977} §1.3 — what the New Zealand judgments provide: the three rulings, taken together.

      Equations
      Instances For
        def Phenomena.Modality.Studies.Kratzer1977.f :
        Fin 4List (Fin 4Prop)

        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
        Instances For

          Membership lemmas: each judgment is in A. #

          §2. A is inconsistent #

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

          §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.

          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.

          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 @cite{kratzer-1977} §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 #

          Consistency of relevant sublists of A #

          Sublist enumeration #

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

          theorem Phenomena.Modality.Studies.Kratzer1977.mem_of_sublist_A {B : List (Fin 4Prop)} (hB : B A.sublists) {x : Fin 4Prop} (hx : x B) :
          x = p x = q x = negQ
          theorem Phenomena.Modality.Studies.Kratzer1977.not_q_and_negQ {B : List (Fin 4Prop)} (hCons : Core.Logic.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] #

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

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

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

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

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

          The empty list is a sublist of A.

          Witness selection for the revised must/can theorems #

          theorem Phenomena.Modality.Studies.Kratzer1977.exists_extension_with_p {B : List (Fin 4Prop)} (hBSub : B A.sublists) (hBCons : Core.Logic.Intensional.Premise.isConsistent B) :
          CA.sublists, Core.Logic.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.

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

          (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.

          (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.

          (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.

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

          (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.