Fox 2007: Free Choice via Recursive Exhaustification [Fox07]

The original grammatical account of free-choice permission. Recursive application of the covert exhaustivity operator exh (Innocent Exclusion) over the Sauerland alternatives {◇(p∨q), ◇p, ◇q, ◇(p∧q)} derives the FC inference without Innocent Inclusion.

• Layer 1: Exh(◇(p∨q)) = ◇(p∨q) ∧ ¬◇(p∧q) (only ◇(p∧q) is innocently excludable)
• Layer 2: Exh²(◇(p∨q)) = ◇p ∧ ◇q ∧ ¬◇(p∧q) — free choice

The five-world model below (ModalW) makes each ◇-formula correspond to which propositional situations are accessible from the evaluation world, so that the four Sauerland alternatives have non-trivial truth values and the IE algorithm has something to compute over.

inductive Fox2007.ModalW : Type

Modal worlds named by which ◇-propositions they make true.

• seesP : ModalW
• seesQ : ModalW
• seesPQ : ModalW
• seesBoth : ModalW
• seesNothing : ModalW

@[implicit_reducible]

instance Fox2007.instReprModalW : Repr ModalW

Equations

• Fox2007.instReprModalW = { reprPrec := Fox2007.instReprModalW.repr }

def Fox2007.instReprModalW.repr : ModalW → ℕ → Std.Format

Equations

• Fox2007.instReprModalW.repr Fox2007.ModalW.seesP prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Fox2007.ModalW.seesP")).group prec✝
• Fox2007.instReprModalW.repr Fox2007.ModalW.seesQ prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Fox2007.ModalW.seesQ")).group prec✝
• Fox2007.instReprModalW.repr Fox2007.ModalW.seesPQ prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Fox2007.ModalW.seesPQ")).group prec✝
• Fox2007.instReprModalW.repr Fox2007.ModalW.seesBoth prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Fox2007.ModalW.seesBoth")).group prec✝
• Fox2007.instReprModalW.repr Fox2007.ModalW.seesNothing prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Fox2007.ModalW.seesNothing")).group prec✝

@[implicit_reducible]

instance Fox2007.instDecidableEqModalW : DecidableEq ModalW

Equations

• Fox2007.instDecidableEqModalW x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Fox2007.instFintypeModalW : Fintype ModalW

Equations

• Fox2007.instFintypeModalW = { elems := { val := ↑Fox2007.ModalW.enumList, nodup := Fox2007.ModalW.enumList_nodup }, complete := Fox2007.instFintypeModalW._proof_1 }

def Fox2007.diamP : ModalW → Bool

Equations

• Fox2007.diamP Fox2007.ModalW.seesP = true
• Fox2007.diamP Fox2007.ModalW.seesPQ = true
• Fox2007.diamP Fox2007.ModalW.seesBoth = true
• Fox2007.diamP x✝ = false

def Fox2007.diamQ : ModalW → Bool

Equations

• Fox2007.diamQ Fox2007.ModalW.seesQ = true
• Fox2007.diamQ Fox2007.ModalW.seesPQ = true
• Fox2007.diamQ Fox2007.ModalW.seesBoth = true
• Fox2007.diamQ x✝ = false

def Fox2007.diamPorQ : ModalW → Bool

Equations

• Fox2007.diamPorQ Fox2007.ModalW.seesNothing = false
• Fox2007.diamPorQ x✝ = true

def Fox2007.diamPandQ : ModalW → Bool

Equations

• Fox2007.diamPandQ Fox2007.ModalW.seesBoth = true
• Fox2007.diamPandQ x✝ = false

@[reducible, inline]

abbrev Fox2007.modalAltsF : Finset (Finset ModalW)

Sauerland alternatives under ◇: {◇(p∨q), ◇p, ◇q, ◇(p∧q)}.

Equations

• Fox2007.modalAltsF = Exhaustification.altsFromPreds [Fox2007.diamPorQ, Fox2007.diamP, Fox2007.diamQ, Fox2007.diamPandQ]

@[reducible, inline]

abbrev Fox2007.diamPorQF : Finset ModalW

Equations

• Fox2007.diamPorQF = Exhaustification.predToFinset Fox2007.diamPorQ

@[reducible, inline]

abbrev Fox2007.diamPF : Finset ModalW

Equations

• Fox2007.diamPF = Exhaustification.predToFinset Fox2007.diamP

@[reducible, inline]

abbrev Fox2007.diamQF : Finset ModalW

Equations

• Fox2007.diamQF = Exhaustification.predToFinset Fox2007.diamQ

@[reducible, inline]

abbrev Fox2007.diamPandQF : Finset ModalW

Equations

• Fox2007.diamPandQF = Exhaustification.predToFinset Fox2007.diamPandQ

theorem Fox2007.exhDiamPorQ_eq : Exhaustification.innocent.exh modalAltsF diamPorQF = Exhaustification.predToFinset fun (w : ModalW) => diamPorQ w && !diamPandQ w

Layer 1: Exh(◇(p∨q)) = ◇(p∨q) ∧ ¬◇(p∧q). Only ◇(p∧q) is innocently excludable; ◇p and ◇q cannot be IE-excluded because excluding ◇p while keeping ◇(p∨q) forces ◇q, and conversely.

theorem Fox2007.exhDiamP_eq : Exhaustification.innocent.exh modalAltsF diamPF = Exhaustification.predToFinset fun (w : ModalW) => diamP w && !diamQ w

Exhaustifying ◇p (relative to the same alternatives) excludes ◇q.

theorem Fox2007.exhDiamQ_eq : Exhaustification.innocent.exh modalAltsF diamQF = Exhaustification.predToFinset fun (w : ModalW) => diamQ w && !diamP w

Exhaustifying ◇q excludes ◇p (symmetric).

theorem Fox2007.exhDiamPandQ_eq : Exhaustification.innocent.exh modalAltsF diamPandQF = diamPandQF

Exhaustifying ◇(p∧q) is vacuous: it entails every other alternative, so nothing is non-weaker.

@[reducible, inline]

abbrev Fox2007.layer2AltsF : Finset (Finset ModalW)

Layer-2 alternatives: {Exh(φ) : φ ∈ C} — the exhaustified versions of the original Sauerland alternatives.

Equations

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

@[reducible, inline]

abbrev Fox2007.layer1ResultF : Finset ModalW

Layer-1 result, used as the prejacent for layer 2.

Equations

• Fox2007.layer1ResultF = Exhaustification.innocent.exh Fox2007.modalAltsF Fox2007.diamPorQF

theorem Fox2007.free_choice : Exhaustification.innocent.exh layer2AltsF layer1ResultF = Exhaustification.predToFinset fun (w : ModalW) => diamP w && diamQ w && !diamPandQ w

Free Choice: double exhaustification yields ◇p ∧ ◇q ∧ ¬◇(p∧q).

Exh(C')[Exh(C)(◇(p∨q))] excludes the layer-2 alternatives Exh(◇p) = ◇p ∧ ¬◇q and Exh(◇q) = ◇q ∧ ¬◇p. Negating both (given the layer-1 prejacent ◇(p∨q) ∧ ¬◇(p∧q)) forces both ◇p and ◇q to hold.

theorem Fox2007.fc_entails_both_disjuncts (w : ModalW) (h : w ∈ Exhaustification.innocent.exh layer2AltsF layer1ResultF) : diamP w = true ∧ diamQ w = true

FC entails both disjuncts hold: the speaker has permission for each disjunct individually.