structure Phenomena.FreeChoice.FreeChoiceDatum : Type

Empirical pattern: Free choice permission.

"You may have coffee or tea" pragmatically implies: "You may have coffee AND you may have tea"

This is not a semantic entailment:

• Semantically: ◇(C∨T) ↔ ◇C ∨ ◇T
• Pragmatically: ◇(C∨T) → ◇C ∧ ◇T

• permission : String

  The permission statement

• disjunctA : String

  The disjuncts

• disjunctB : String
• inference : String

  The inferred free choice reading

• isSemanticEntailment : Bool

  Is this a semantic entailment?

• isPragmaticInference : Bool

  Is this a pragmatic inference?

def Phenomena.FreeChoice.instReprFreeChoiceDatum.repr : FreeChoiceDatum → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.FreeChoice.instReprFreeChoiceDatum : Repr FreeChoiceDatum

Equations

• Phenomena.FreeChoice.instReprFreeChoiceDatum = { reprPrec := Phenomena.FreeChoice.instReprFreeChoiceDatum.repr }

def Phenomena.FreeChoice.coffeeOrTea : FreeChoiceDatum

Classic free choice example. Source: @cite{ross-1944}, @cite{kamp-1973}

Equations

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

def Phenomena.FreeChoice.readOrSleep : FreeChoiceDatum

Free choice with activities. Source: @cite{kamp-1973}

Equations

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

def Phenomena.FreeChoice.parkOrBeach : FreeChoiceDatum

Free choice with locations.

Equations

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

def Phenomena.FreeChoice.freeChoiceExamples : List FreeChoiceDatum

All basic free choice examples.

Equations

• Phenomena.FreeChoice.freeChoiceExamples = [Phenomena.FreeChoice.coffeeOrTea, Phenomena.FreeChoice.readOrSleep, Phenomena.FreeChoice.parkOrBeach]

structure Phenomena.FreeChoice.RossParadoxDatum : Type

Ross's Paradox: The puzzle that motivated free choice research.

From "Post the letter" we can infer "Post the letter or burn it" (by or-introduction). But intuitively, permission to post doesn't give permission to burn!

Source: @cite{ross-1944}

• original : String

  The original imperative/permission

• derived : String

  The derived statement (by or-intro)

• semanticallyValid : Bool

  Is the derivation semantically valid?

• pragmaticallyFelicitous : Bool

  Is the derivation pragmatically felicitous?

def Phenomena.FreeChoice.instReprRossParadoxDatum.repr : RossParadoxDatum → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.FreeChoice.instReprRossParadoxDatum : Repr RossParadoxDatum

Equations

• Phenomena.FreeChoice.instReprRossParadoxDatum = { reprPrec := Phenomena.FreeChoice.instReprRossParadoxDatum.repr }

def Phenomena.FreeChoice.postOrBurn : RossParadoxDatum

Classic Ross's paradox example. Source: @cite{ross-1944}

Equations

• Phenomena.FreeChoice.postOrBurn = { original := "Post the letter", derived := "Post the letter or burn it", semanticallyValid := true, pragmaticallyFelicitous := false }

def Phenomena.FreeChoice.mayPostOrBurn : RossParadoxDatum

Ross's paradox with permission.

Equations

• Phenomena.FreeChoice.mayPostOrBurn = { original := "You may post the letter", derived := "You may post the letter or burn it", semanticallyValid := true, pragmaticallyFelicitous := false }

def Phenomena.FreeChoice.rossParadoxExamples : List RossParadoxDatum

All Ross's paradox examples.

Equations

• Phenomena.FreeChoice.rossParadoxExamples = [Phenomena.FreeChoice.postOrBurn, Phenomena.FreeChoice.mayPostOrBurn]

structure Phenomena.FreeChoice.ModalFreeChoiceDatum : Type

Free choice occurs with various modal flavors.

• modalType : String

  The modal type

• sentence : String

  Example sentence

• inference : String

  Free choice inference

• freeChoiceArises : Bool

  Does free choice arise?

@[implicit_reducible]

instance Phenomena.FreeChoice.instReprModalFreeChoiceDatum : Repr ModalFreeChoiceDatum

Equations

• Phenomena.FreeChoice.instReprModalFreeChoiceDatum = { reprPrec := Phenomena.FreeChoice.instReprModalFreeChoiceDatum.repr }

def Phenomena.FreeChoice.instReprModalFreeChoiceDatum.repr : ModalFreeChoiceDatum → Nat → Std.Format

Equations

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

def Phenomena.FreeChoice.deonticFC : ModalFreeChoiceDatum

Deontic permission (classic case). Source: @cite{kamp-1973}

Equations

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

def Phenomena.FreeChoice.epistemicFC : ModalFreeChoiceDatum

Epistemic possibility. Source: @cite{zimmermann-2000}

Equations

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

def Phenomena.FreeChoice.abilityFC : ModalFreeChoiceDatum

Ability modal.

Equations

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

def Phenomena.FreeChoice.modalFreeChoiceExamples : List ModalFreeChoiceDatum

All modal free choice examples.

Equations

• Phenomena.FreeChoice.modalFreeChoiceExamples = [Phenomena.FreeChoice.deonticFC, Phenomena.FreeChoice.epistemicFC, Phenomena.FreeChoice.abilityFC]

structure Phenomena.FreeChoice.FCCancellationDatum : Type

Free choice can be cancelled, showing it's pragmatic not semantic.

• original : String

  Original sentence with free choice

• cancellation : String

  Cancellation phrase

• combined : String

  Combined result

• felicitous : Bool

  Is the result felicitous?

def Phenomena.FreeChoice.instReprFCCancellationDatum.repr : FCCancellationDatum → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.FreeChoice.instReprFCCancellationDatum : Repr FCCancellationDatum

Equations

• Phenomena.FreeChoice.instReprFCCancellationDatum = { reprPrec := Phenomena.FreeChoice.instReprFCCancellationDatum.repr }

def Phenomena.FreeChoice.explicitCancellation : FCCancellationDatum

Explicit cancellation of free choice.

Equations

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

def Phenomena.FreeChoice.contextualCancellation : FCCancellationDatum

Cancellation by context.

Equations

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

def Phenomena.FreeChoice.cancellationExamples : List FCCancellationDatum

All cancellation examples.

Equations

• Phenomena.FreeChoice.cancellationExamples = [Phenomena.FreeChoice.explicitCancellation, Phenomena.FreeChoice.contextualCancellation]

Free Choice Any

Universal free choice items (FCIs) like any exhibit similar inference patterns to disjunctive free choice but involve universal quantification.

"You may take any class" pragmatically implies:

• You may take Syntax (specifically)
• You may take Phonology (specifically)
• You may take Semantics (specifically) -... (for all classes)

This is the exclusiveness inference: permission applies to each individual alternative, not just to "some class or other".

Key difference from disjunction:

• Disjunction: ◇(a ∨ b) → ◇a ∧ ◇b
• Universal FCI: ◇(∃x.class(x)) → ∀x.class(x) → ◇take(x)

structure Phenomena.FreeChoice.FCIAnyDatum : Type

Empirical pattern: Free choice any (universal FCI).

"You may take any class" pragmatically implies permission for each specific class. This is the exclusiveness inference, distinct from simple existential permission.

• sentence : String

  The sentence with any

• domain : String

  The domain of quantification

• domainElements : List String

  Example domain elements

• inference : String

  The inferred reading

• exclusivenessArises : Bool

  Does exclusiveness inference arise?

• robustToPriors : Bool

  Is this inference robust to prior manipulation?

def Phenomena.FreeChoice.instReprFCIAnyDatum.repr : FCIAnyDatum → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.FreeChoice.instReprFCIAnyDatum : Repr FCIAnyDatum

Equations

• Phenomena.FreeChoice.instReprFCIAnyDatum = { reprPrec := Phenomena.FreeChoice.instReprFCIAnyDatum.repr }

def Phenomena.FreeChoice.anyClass : FCIAnyDatum

Free choice any with classes. Source: @cite{alsop-2024}

Equations

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

def Phenomena.FreeChoice.anyFruit : FCIAnyDatum

Free choice any with fruits (simplified domain). Source: Based on @cite{kadmon-landman-1993}

Equations

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

def Phenomena.FreeChoice.anyRoom : FCIAnyDatum

Free choice any with locations.

Equations

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

def Phenomena.FreeChoice.fciAnyExamples : List FCIAnyDatum

All FCI any examples.

Equations

• Phenomena.FreeChoice.fciAnyExamples = [Phenomena.FreeChoice.anyClass, Phenomena.FreeChoice.anyFruit, Phenomena.FreeChoice.anyRoom]

structure Phenomena.FreeChoice.FCComparisonDatum : Type

Comparison between disjunctive FC and universal any FC.

• aspect : String

  Description of the contrast

• disjunctionFC : String

  Disjunctive FC behavior

• universalFC : String

  Universal any FC behavior

• analogous : Bool

  Are they analogous?

def Phenomena.FreeChoice.instReprFCComparisonDatum.repr : FCComparisonDatum → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.FreeChoice.instReprFCComparisonDatum : Repr FCComparisonDatum

Equations

• Phenomena.FreeChoice.instReprFCComparisonDatum = { reprPrec := Phenomena.FreeChoice.instReprFCComparisonDatum.repr }

def Phenomena.FreeChoice.bothDeriveFC : FCComparisonDatum

Both derive free choice/exclusiveness inferences.

Equations

• Phenomena.FreeChoice.bothDeriveFC = { aspect := "Core inference", disjunctionFC := "◇(a ∨ b) → ◇a ∧ ◇b", universalFC := "◇(∃x.P(x)) → ∀x.P(x) → ◇x", analogous := true }

def Phenomena.FreeChoice.bothRobust : FCComparisonDatum

Both are robust to prior manipulation.

Equations

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

def Phenomena.FreeChoice.differentStructure : FCComparisonDatum

Different quantificational structure.

Equations

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

def Phenomena.FreeChoice.fcComparisonData : List FCComparisonDatum

All FC comparison data.

Equations

• Phenomena.FreeChoice.fcComparisonData = [Phenomena.FreeChoice.bothDeriveFC, Phenomena.FreeChoice.bothRobust, Phenomena.FreeChoice.differentStructure]

FC with Anaphora: Bathroom Disjunctions

@cite{elliott-sudo-2025} identify a novel FC pattern where cross-disjunct anaphora interacts with Free Choice:

"Either there's no bathroom or it's in a funny place"

Inference:

1. ◇(there's no bathroom)
2. ◇(there's a bathroom ∧ it's in a funny place)

The pronoun "it" in the second disjunct is bound by the existential in the negated first disjunct. This is puzzling because negation should block binding, yet the inference requires x to be accessible.

structure Phenomena.FreeChoice.BathroomDisjunctionDatum : Type

Bathroom disjunction: FC with cross-disjunct anaphora.

• sentence : String

  The sentence

• disjunct1 : String

  First disjunct (typically negated existential)

• disjunct2 : String

  Second disjunct (with anaphoric element)

• anaphor : String

  The anaphoric element

• antecedent : String

  The antecedent (under negation)

• inference1 : String

  First FC inference

• inference2 : String

  Second FC inference (with anaphora resolved)

• hasCrossDisjunctAnaphora : Bool

  Does cross-disjunct anaphora occur?

• source : String

  Source

@[implicit_reducible]

instance Phenomena.FreeChoice.instReprBathroomDisjunctionDatum : Repr BathroomDisjunctionDatum

Equations

• Phenomena.FreeChoice.instReprBathroomDisjunctionDatum = { reprPrec := Phenomena.FreeChoice.instReprBathroomDisjunctionDatum.repr }

def Phenomena.FreeChoice.instReprBathroomDisjunctionDatum.repr : BathroomDisjunctionDatum → Nat → Std.Format

Equations

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

def Phenomena.FreeChoice.bathroomClassic : BathroomDisjunctionDatum

Classic bathroom disjunction. Source: @cite{elliott-sudo-2025}

Equations

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

def Phenomena.FreeChoice.bathroomDefinite : BathroomDisjunctionDatum

Bathroom variant with "the bathroom".

Equations

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

def Phenomena.FreeChoice.keyExample : BathroomDisjunctionDatum

Similar pattern with different content.

Equations

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

def Phenomena.FreeChoice.nobodyExample : BathroomDisjunctionDatum

Negated universal variant.

Equations

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

def Phenomena.FreeChoice.bathroomDisjunctionExamples : List BathroomDisjunctionDatum

All bathroom disjunction examples.

Equations

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

structure Phenomena.FreeChoice.StandardFCDatum : Type

Standard FC without cross-disjunct anaphora (for comparison).

• sentence : String

  The sentence

• disjuncts : List String

  The disjuncts

• inferences : List String

  FC inferences

• hasAnaphora : Bool

  Any anaphora?

@[implicit_reducible]

instance Phenomena.FreeChoice.instReprStandardFCDatum : Repr StandardFCDatum

Equations

• Phenomena.FreeChoice.instReprStandardFCDatum = { reprPrec := Phenomena.FreeChoice.instReprStandardFCDatum.repr }

def Phenomena.FreeChoice.instReprStandardFCDatum.repr : StandardFCDatum → Nat → Std.Format

Equations

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

def Phenomena.FreeChoice.coffeeTeaStandard : StandardFCDatum

Standard FC: no anaphora.

Equations

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

def Phenomena.FreeChoice.parisLondonStandard : StandardFCDatum

Standard FC with independent disjuncts.

Equations

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

def Phenomena.FreeChoice.standardFCExamples : List StandardFCDatum

All standard FC examples (contrast with bathroom).

Equations

• Phenomena.FreeChoice.standardFCExamples = [Phenomena.FreeChoice.coffeeTeaStandard, Phenomena.FreeChoice.parisLondonStandard]