Free Choice Configuration

To derive free choice, we need:

• φ = ◇(a ∨ b) (the prejacent)
• ALT = {◇(a ∨ b), ◇a, ◇b, ◇(a ∧ b)} (the alternatives)

Key observation: This ALT is NOT closed under conjunction!

• ◇a ∧ ◇b is NOT in ALT (it's not equivalent to any member)

This non-closure is what allows II to derive free choice.

inductive NeoGricean.FreeChoice.FCWorld : Type

Possible worlds for free choice (whether each disjunct is permitted).

The separatelyAB world is crucial: it represents an epistemic state where a and b are each individually permitted but not jointly — i.e., some accessible world has a (not b) and some has b (not a), but no single accessible world has both. This distinguishes ◇a ∧ ◇b from ◇(a ∧ b) and is what makes free choice derivable via II.

• neither : FCWorld
• onlyA : FCWorld
• onlyB : FCWorld
• both : FCWorld
• separatelyAB : FCWorld

instance NeoGricean.FreeChoice.instDecidableEqFCWorld : DecidableEq FCWorld

Equations

• NeoGricean.FreeChoice.instDecidableEqFCWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def NeoGricean.FreeChoice.instBEqFCWorld.beq : FCWorld → FCWorld → Bool

Equations

• NeoGricean.FreeChoice.instBEqFCWorld.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance NeoGricean.FreeChoice.instBEqFCWorld : BEq FCWorld

Equations

• NeoGricean.FreeChoice.instBEqFCWorld = { beq := NeoGricean.FreeChoice.instBEqFCWorld.beq }

instance NeoGricean.FreeChoice.instReprFCWorld : Repr FCWorld

Equations

• NeoGricean.FreeChoice.instReprFCWorld = { reprPrec := NeoGricean.FreeChoice.instReprFCWorld.repr }

def NeoGricean.FreeChoice.instReprFCWorld.repr : FCWorld → ℕ → Std.Format

Equations

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

instance NeoGricean.FreeChoice.instInhabitedFCWorld : Inhabited FCWorld

Equations

• NeoGricean.FreeChoice.instInhabitedFCWorld = { default := NeoGricean.FreeChoice.instInhabitedFCWorld.default }

def NeoGricean.FreeChoice.instInhabitedFCWorld.default : FCWorld

Equations

• NeoGricean.FreeChoice.instInhabitedFCWorld.default = NeoGricean.FreeChoice.FCWorld.neither

def NeoGricean.FreeChoice.permA : Prop' FCWorld

Proposition: a is permitted

Equations

• NeoGricean.FreeChoice.permA NeoGricean.FreeChoice.FCWorld.neither = False
• NeoGricean.FreeChoice.permA NeoGricean.FreeChoice.FCWorld.onlyA = True
• NeoGricean.FreeChoice.permA NeoGricean.FreeChoice.FCWorld.onlyB = False
• NeoGricean.FreeChoice.permA NeoGricean.FreeChoice.FCWorld.both = True
• NeoGricean.FreeChoice.permA NeoGricean.FreeChoice.FCWorld.separatelyAB = True

def NeoGricean.FreeChoice.permB : Prop' FCWorld

Proposition: b is permitted

Equations

• NeoGricean.FreeChoice.permB NeoGricean.FreeChoice.FCWorld.neither = False
• NeoGricean.FreeChoice.permB NeoGricean.FreeChoice.FCWorld.onlyA = False
• NeoGricean.FreeChoice.permB NeoGricean.FreeChoice.FCWorld.onlyB = True
• NeoGricean.FreeChoice.permB NeoGricean.FreeChoice.FCWorld.both = True
• NeoGricean.FreeChoice.permB NeoGricean.FreeChoice.FCWorld.separatelyAB = True

def NeoGricean.FreeChoice.permAorB : Prop' FCWorld

Proposition: a ∨ b is permitted (◇(a ∨ b))

Equations

• NeoGricean.FreeChoice.permAorB NeoGricean.FreeChoice.FCWorld.neither = False
• NeoGricean.FreeChoice.permAorB NeoGricean.FreeChoice.FCWorld.onlyA = True
• NeoGricean.FreeChoice.permAorB NeoGricean.FreeChoice.FCWorld.onlyB = True
• NeoGricean.FreeChoice.permAorB NeoGricean.FreeChoice.FCWorld.both = True
• NeoGricean.FreeChoice.permAorB NeoGricean.FreeChoice.FCWorld.separatelyAB = True

def NeoGricean.FreeChoice.permAandB : Prop' FCWorld

Proposition: a ∧ b is permitted (◇(a ∧ b))

Equations

• NeoGricean.FreeChoice.permAandB NeoGricean.FreeChoice.FCWorld.neither = False
• NeoGricean.FreeChoice.permAandB NeoGricean.FreeChoice.FCWorld.onlyA = False
• NeoGricean.FreeChoice.permAandB NeoGricean.FreeChoice.FCWorld.onlyB = False
• NeoGricean.FreeChoice.permAandB NeoGricean.FreeChoice.FCWorld.both = True
• NeoGricean.FreeChoice.permAandB NeoGricean.FreeChoice.FCWorld.separatelyAB = False

def NeoGricean.FreeChoice.fcALT : Set (Prop' FCWorld)

The free choice alternative set: {◇(a ∨ b), ◇a, ◇b, ◇(a ∧ b)}

Equations

• NeoGricean.FreeChoice.fcALT = {NeoGricean.FreeChoice.permAorB, NeoGricean.FreeChoice.permA, NeoGricean.FreeChoice.permB, NeoGricean.FreeChoice.permAandB}

def NeoGricean.FreeChoice.fcPrejacent : Prop' FCWorld

The prejacent: ◇(a ∨ b)

Equations

• NeoGricean.FreeChoice.fcPrejacent = NeoGricean.FreeChoice.permAorB

The Key Structural Property

Theorem (Non-closure): fcALT is NOT closed under conjunction.

Specifically: permA ∧ permB (= ◇a ∧ ◇b) is not in fcALT.

This is the structural property that distinguishes FC alternatives from simple disjunction alternatives and enables the free choice inference.

For simple disjunction:

• ALT = {a ∨ b, a, b, a ∧ b}
• a ∧ b IS in ALT
• Closed under conjunction

For FC disjunction:

• ALT = {◇(a ∨ b), ◇a, ◇b, ◇(a ∧ b)}
• ◇a ∧ ◇b is NOT in ALT (it's different from ◇(a ∧ b)!)
• NOT closed under conjunction

theorem NeoGricean.FreeChoice.fc_not_closed_general : ¬∀ X ⊆ fcALT, ⋀ X ∈ fcALT

The free choice alternatives are NOT closed under conjunction in the relevant sense: the conjunction of two alternatives is not equivalent to any single alternative in the general case.

In modal logic: ◇a ∧ ◇b ⊭ ◇(a ∧ b) (there are worlds where both are individually possible but their conjunction is not).

IE Computation for Free Choice

For φ = ◇(a ∨ b) and ALT = {◇(a ∨ b), ◇a, ◇b, ◇(a ∧ b)}:

IE Analysis:

• ◇(a ∧ b) is innocently excludable (can be consistently negated)
• ◇a is NOT innocently excludable (negating it contradicts φ at some worlds)
• ◇b is NOT innocently excludable (negating it contradicts φ at some worlds)

Result: IE = {◇(a ∧ b)}

This is where standard exhaustivity stops: Exh^{IE}(◇(a ∨ b)) = ◇(a ∨ b) ∧ ¬◇(a ∧ b) which does NOT entail ◇a ∧ ◇b.

II Computation for Free Choice

After IE excludes ◇(a ∧ b), II considers which remaining alternatives can be consistently assigned TRUE.

II Analysis: Given φ = ◇(a ∨ b) and IE = {◇(a ∧ b)}:

Consider the constraint set: {◇(a ∨ b), ¬◇(a ∧ b)}

• This is consistent with ◇a (witness: onlyA world)
• This is consistent with ◇b (witness: onlyB world)
• Both ◇a and ◇b appear in EVERY maximal II-compatible set

Therefore: II = {◇a, ◇b}

Result: Exh^{IE+II}(◇(a ∨ b)) = ◇(a ∨ b) ∧ ¬◇(a ∧ b) ∧ ◇a ∧ ◇b

This is FREE CHOICE!

Main Result: Free Choice Derivation

Theorem: Exh^{IE+II}(◇(a ∨ b)) ⊢ ◇a ∧ ◇b

The exhaustified meaning of "you may have a or b" entails "you may have a AND you may have b".

theorem NeoGricean.FreeChoice.fc_entails_permA (w : FCWorld) : Exhaustivity.exhIEII fcALT fcPrejacent w → permA w

The free choice inference: exhaustified ◇(a ∨ b) entails ◇a

theorem NeoGricean.FreeChoice.fc_entails_permB (w : FCWorld) : Exhaustivity.exhIEII fcALT fcPrejacent w → permB w

The free choice inference: exhaustified ◇(a ∨ b) entails ◇b

theorem NeoGricean.FreeChoice.free_choice (w : FCWorld) : Exhaustivity.exhIEII fcALT fcPrejacent w → permA w ∧ permB w

Main Free Choice Theorem: Exh^{IE+II}(◇(a ∨ b)) ⊢ ◇a ∧ ◇b

Why Simple Disjunction Doesn't Get Free Choice

For comparison, simple disjunction:

• φ = a ∨ b
• ALT = {a ∨ b, a, b, a ∧ b}

This ALT IS closed under conjunction (a ∧ b is already there).

IE Analysis: IE = {a, b, a ∧ b} (all proper alternatives excludable) II Analysis: II = ∅ (nothing can be consistently included after IE)

Result: Exh^{IE+II}(a ∨ b) = (a ∨ b) ∧ ¬a ∧ ¬b ∧ ¬(a ∧ b) = ⊥

This is inconsistent! So Exh cannot apply to simple disjunction (motivating embedded exhaustification in complex sentences).

The contrast:

• ◇(a ∨ b): FC alternatives not closed → free choice
• a ∨ b: Alternatives closed → exclusive-or (or inconsistency)

inductive NeoGricean.FreeChoice.DisjWorld : Type

Simple disjunction worlds

• neither : DisjWorld
• onlyA : DisjWorld
• onlyB : DisjWorld
• both : DisjWorld

instance NeoGricean.FreeChoice.instDecidableEqDisjWorld : DecidableEq DisjWorld

Equations

• NeoGricean.FreeChoice.instDecidableEqDisjWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def NeoGricean.FreeChoice.instBEqDisjWorld.beq : DisjWorld → DisjWorld → Bool

Equations

• NeoGricean.FreeChoice.instBEqDisjWorld.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance NeoGricean.FreeChoice.instBEqDisjWorld : BEq DisjWorld

Equations

• NeoGricean.FreeChoice.instBEqDisjWorld = { beq := NeoGricean.FreeChoice.instBEqDisjWorld.beq }

instance NeoGricean.FreeChoice.instReprDisjWorld : Repr DisjWorld

Equations

• NeoGricean.FreeChoice.instReprDisjWorld = { reprPrec := NeoGricean.FreeChoice.instReprDisjWorld.repr }

def NeoGricean.FreeChoice.instReprDisjWorld.repr : DisjWorld → ℕ → Std.Format

Equations

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

def NeoGricean.FreeChoice.instInhabitedDisjWorld.default : DisjWorld

Equations

• NeoGricean.FreeChoice.instInhabitedDisjWorld.default = NeoGricean.FreeChoice.DisjWorld.neither

instance NeoGricean.FreeChoice.instInhabitedDisjWorld : Inhabited DisjWorld

Equations

• NeoGricean.FreeChoice.instInhabitedDisjWorld = { default := NeoGricean.FreeChoice.instInhabitedDisjWorld.default }

def NeoGricean.FreeChoice.propA : Prop' DisjWorld

Proposition a

Equations

• NeoGricean.FreeChoice.propA NeoGricean.FreeChoice.DisjWorld.neither = False
• NeoGricean.FreeChoice.propA NeoGricean.FreeChoice.DisjWorld.onlyA = True
• NeoGricean.FreeChoice.propA NeoGricean.FreeChoice.DisjWorld.onlyB = False
• NeoGricean.FreeChoice.propA NeoGricean.FreeChoice.DisjWorld.both = True

def NeoGricean.FreeChoice.propB : Prop' DisjWorld

Proposition b

Equations

• NeoGricean.FreeChoice.propB NeoGricean.FreeChoice.DisjWorld.neither = False
• NeoGricean.FreeChoice.propB NeoGricean.FreeChoice.DisjWorld.onlyA = False
• NeoGricean.FreeChoice.propB NeoGricean.FreeChoice.DisjWorld.onlyB = True
• NeoGricean.FreeChoice.propB NeoGricean.FreeChoice.DisjWorld.both = True

def NeoGricean.FreeChoice.propAorB : Prop' DisjWorld

Proposition a ∨ b

Equations

• NeoGricean.FreeChoice.propAorB NeoGricean.FreeChoice.DisjWorld.neither = False
• NeoGricean.FreeChoice.propAorB NeoGricean.FreeChoice.DisjWorld.onlyA = True
• NeoGricean.FreeChoice.propAorB NeoGricean.FreeChoice.DisjWorld.onlyB = True
• NeoGricean.FreeChoice.propAorB NeoGricean.FreeChoice.DisjWorld.both = True

def NeoGricean.FreeChoice.propAandB : Prop' DisjWorld

Proposition a ∧ b

Equations

• NeoGricean.FreeChoice.propAandB NeoGricean.FreeChoice.DisjWorld.neither = False
• NeoGricean.FreeChoice.propAandB NeoGricean.FreeChoice.DisjWorld.onlyA = False
• NeoGricean.FreeChoice.propAandB NeoGricean.FreeChoice.DisjWorld.onlyB = False
• NeoGricean.FreeChoice.propAandB NeoGricean.FreeChoice.DisjWorld.both = True

def NeoGricean.FreeChoice.simpleALT : Set (Prop' DisjWorld)

Simple disjunction alternatives: {a ∨ b, a, b, a ∧ b}

Equations

• NeoGricean.FreeChoice.simpleALT = {NeoGricean.FreeChoice.propAorB, NeoGricean.FreeChoice.propA, NeoGricean.FreeChoice.propB, NeoGricean.FreeChoice.propAandB}

theorem NeoGricean.FreeChoice.simple_has_conjunction : propAandB ∈ simpleALT

Simple disjunction IS closed under conjunction (a ∧ b ∈ ALT)

theorem NeoGricean.FreeChoice.simple_exclusive_or (w : DisjWorld) : Exhaustivity.exhIE simpleALT propAorB w → propA w ∧ ¬propB w ∨ propB w ∧ ¬propA w ∨ propA w ∧ propB w

For simple disjunction, exhaustification yields exclusive-or (or inconsistency without embedded Exh)

Summary

Definitions

• II: Innocently Includable alternatives (those in every MI-set)
• exhIEII: Combined exhaustivity operator Exh^{IE+II}
• isInnocentlyIncludable: Predicate for II membership

Results

• free_choice: Exh^{IE+II}(◇(a ∨ b)) ⊢ ◇a ∧ ◇b
• fc_not_closed_general: FC alternatives not closed under ∧
• simple_has_conjunction: Simple disjunction alternatives ARE closed

Theoretical Insight

The structural difference between FC and simple disjunction is closure under conjunction:

• Closed → exclusive-or (standard scalar implicature)
• Not closed → free choice (via Innocent Inclusion)