Disjunction Ignorance @cite{chierchia-2013}

Empirical patterns for ignorance inferences from disjunction, organized around @cite{chierchia-2013}'s positional-asymmetry account.

"Harry is in Antwerp or Brussels" implicates:

1. Speaker doesn't know Harry is in Antwerp
2. Speaker doesn't know Harry is in Brussels

This is different from scalar implicature:

• Scalar: "some" → speaker knows not all
• Ignorance: "A or B" → speaker doesn't know which

The file provides a predictReading function over ContextPolarity (from Core.NaturalLogic) that derives the preferred inclusive/exclusive reading from structural position.

structure Phenomena.Polarity.Studies.Chierchia2013.DisjunctionIgnoranceDatum : Type

Empirical pattern: Disjunction and speaker ignorance.

"Harry is in Antwerp or Brussels" implicates:

1. Speaker doesn't know Harry is in Antwerp
2. Speaker doesn't know Harry is in Brussels

Source: @cite{gazdar-1979}, @cite{geurts-2010} Ch. 3.3

• disjunction : String

  The disjunctive statement

• disjunctA : String

  First disjunct

• disjunctB : String

  Second disjunct

• inferenceA : String

  Ignorance inference about A

• inferenceB : String

  Ignorance inference about B

@[implicit_reducible]

instance Phenomena.Polarity.Studies.Chierchia2013.instReprDisjunctionIgnoranceDatum : Repr DisjunctionIgnoranceDatum

Equations

• Phenomena.Polarity.Studies.Chierchia2013.instReprDisjunctionIgnoranceDatum = { reprPrec := Phenomena.Polarity.Studies.Chierchia2013.instReprDisjunctionIgnoranceDatum.repr }

def Phenomena.Polarity.Studies.Chierchia2013.instReprDisjunctionIgnoranceDatum.repr : DisjunctionIgnoranceDatum → ℕ → Std.Format

Equations

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

def Phenomena.Polarity.Studies.Chierchia2013.harryLocation : DisjunctionIgnoranceDatum

Classic example: Harry's location. Source: @cite{geurts-2010} p.61

Equations

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

def Phenomena.Polarity.Studies.Chierchia2013.maryLocation : DisjunctionIgnoranceDatum

Location example with Mary.

Equations

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

def Phenomena.Polarity.Studies.Chierchia2013.johnActivity : DisjunctionIgnoranceDatum

Activity example.

Equations

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

def Phenomena.Polarity.Studies.Chierchia2013.disjunctionIgnoranceExamples : List DisjunctionIgnoranceDatum

All basic ignorance examples.

Equations

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

structure Phenomena.Polarity.Studies.Chierchia2013.IgnoranceVsScalarDatum : Type

Comparison between ignorance and scalar implicatures.

Scalar implicatures and ignorance inferences differ:

• Scalar: speaker knows the stronger alternative is false
• Ignorance: speaker doesn't know which disjunct is true

• utterance : String

  The utterance

• inferenceType : String

  Type of inference

• inference : String

  The inference

• speakerClaimsKnowledge : Bool

  Is speaker claiming knowledge?

@[implicit_reducible]

instance Phenomena.Polarity.Studies.Chierchia2013.instReprIgnoranceVsScalarDatum : Repr IgnoranceVsScalarDatum

Equations

• Phenomena.Polarity.Studies.Chierchia2013.instReprIgnoranceVsScalarDatum = { reprPrec := Phenomena.Polarity.Studies.Chierchia2013.instReprIgnoranceVsScalarDatum.repr }

def Phenomena.Polarity.Studies.Chierchia2013.instReprIgnoranceVsScalarDatum.repr : IgnoranceVsScalarDatum → ℕ → Std.Format

Equations

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

def Phenomena.Polarity.Studies.Chierchia2013.someScalar : IgnoranceVsScalarDatum

"Some" triggers scalar implicature (speaker knows).

Equations

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

def Phenomena.Polarity.Studies.Chierchia2013.orIgnorance : IgnoranceVsScalarDatum

"Or" triggers ignorance (speaker doesn't know).

Equations

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

def Phenomena.Polarity.Studies.Chierchia2013.comparisonExamples : List IgnoranceVsScalarDatum

All comparison examples.

Equations

• Phenomena.Polarity.Studies.Chierchia2013.comparisonExamples = [Phenomena.Polarity.Studies.Chierchia2013.someScalar, Phenomena.Polarity.Studies.Chierchia2013.orIgnorance]

structure Phenomena.Polarity.Studies.Chierchia2013.LongDisjunctionIgnoranceDatum : Type

Ignorance extends to long disjunctions (n > 2).

For "A or B or C", we get ignorance about each disjunct:

• Speaker doesn't know A
• Speaker doesn't know B
• Speaker doesn't know C

Source: @cite{geurts-2010} p.61-64

• disjunction : String

  The disjunctive statement

• disjuncts : List String

  List of disjuncts

• ignoranceInferences : List String

  Ignorance inferences (one per disjunct)

@[implicit_reducible]

instance Phenomena.Polarity.Studies.Chierchia2013.instReprLongDisjunctionIgnoranceDatum : Repr LongDisjunctionIgnoranceDatum

Equations

• Phenomena.Polarity.Studies.Chierchia2013.instReprLongDisjunctionIgnoranceDatum = { reprPrec := Phenomena.Polarity.Studies.Chierchia2013.instReprLongDisjunctionIgnoranceDatum.repr }

def Phenomena.Polarity.Studies.Chierchia2013.instReprLongDisjunctionIgnoranceDatum.repr : LongDisjunctionIgnoranceDatum → ℕ → Std.Format

Equations

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

def Phenomena.Polarity.Studies.Chierchia2013.threeWayLocation : LongDisjunctionIgnoranceDatum

Three-way disjunction example. Source: @cite{geurts-2010} p.61

Equations

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

def Phenomena.Polarity.Studies.Chierchia2013.fourWayActivity : LongDisjunctionIgnoranceDatum

Four-way disjunction example.

Equations

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

def Phenomena.Polarity.Studies.Chierchia2013.longDisjunctionExamples : List LongDisjunctionIgnoranceDatum

All long disjunction examples.

Equations

• Phenomena.Polarity.Studies.Chierchia2013.longDisjunctionExamples = [Phenomena.Polarity.Studies.Chierchia2013.threeWayLocation, Phenomena.Polarity.Studies.Chierchia2013.fourWayActivity]

structure Phenomena.Polarity.Studies.Chierchia2013.IgnoranceBlockingDatum : Type

Cases where ignorance inference is blocked or cancelled.

• context : String

  The context or construction

• sentence : String

  Example sentence

• ignoranceBlocked : Bool

  Is ignorance blocked?

• explanation : String

  Explanation

@[implicit_reducible]

instance Phenomena.Polarity.Studies.Chierchia2013.instReprIgnoranceBlockingDatum : Repr IgnoranceBlockingDatum

Equations

• Phenomena.Polarity.Studies.Chierchia2013.instReprIgnoranceBlockingDatum = { reprPrec := Phenomena.Polarity.Studies.Chierchia2013.instReprIgnoranceBlockingDatum.repr }

def Phenomena.Polarity.Studies.Chierchia2013.instReprIgnoranceBlockingDatum.repr : IgnoranceBlockingDatum → ℕ → Std.Format

Equations

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

def Phenomena.Polarity.Studies.Chierchia2013.explicitKnowledge : IgnoranceBlockingDatum

Explicit knowledge blocks ignorance.

Equations

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

def Phenomena.Polarity.Studies.Chierchia2013.rhetoricalQuestion : IgnoranceBlockingDatum

Rhetorical questions don't trigger ignorance.

Equations

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

def Phenomena.Polarity.Studies.Chierchia2013.embeddedBelief : IgnoranceBlockingDatum

Embedded disjunction under belief.

Equations

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

def Phenomena.Polarity.Studies.Chierchia2013.blockingExamples : List IgnoranceBlockingDatum

All blocking examples.

Equations

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

structure Phenomena.Polarity.Studies.Chierchia2013.QuantifiedIgnoranceDatum : Type

Interaction between disjunction ignorance and quantifiers.

• sentence : String

  The sentence

• quantifierScope : String

  Quantifier scope

• inference : String

  Ignorance inference

• notes : String

  Notes on the reading

@[implicit_reducible]

instance Phenomena.Polarity.Studies.Chierchia2013.instReprQuantifiedIgnoranceDatum : Repr QuantifiedIgnoranceDatum

Equations

• Phenomena.Polarity.Studies.Chierchia2013.instReprQuantifiedIgnoranceDatum = { reprPrec := Phenomena.Polarity.Studies.Chierchia2013.instReprQuantifiedIgnoranceDatum.repr }

def Phenomena.Polarity.Studies.Chierchia2013.instReprQuantifiedIgnoranceDatum.repr : QuantifiedIgnoranceDatum → ℕ → Std.Format

Equations

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

def Phenomena.Polarity.Studies.Chierchia2013.universalScopeDisj : QuantifiedIgnoranceDatum

Disjunction in scope of universal.

Equations

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

def Phenomena.Polarity.Studies.Chierchia2013.disjScopeUniversal : QuantifiedIgnoranceDatum

Disjunction scoping over universal.

Equations

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

def Phenomena.Polarity.Studies.Chierchia2013.quantifiedIgnoranceExamples : List QuantifiedIgnoranceDatum

All quantified ignorance examples.

Equations

• Phenomena.Polarity.Studies.Chierchia2013.quantifiedIgnoranceExamples = [Phenomena.Polarity.Studies.Chierchia2013.universalScopeDisj, Phenomena.Polarity.Studies.Chierchia2013.disjScopeUniversal]

Positional Asymmetry in Disjunction Interpretation

@cite{chierchia-2013} "Logic in Grammar" Ch.1 observes that the same lexical material yields different preferred readings based on structural position:

Position	Polarity	Preferred Reading
Consequent of conditional	UE	Exclusive
Antecedent of conditional	DE	Inclusive
Scope of "every"	UE	Exclusive
Restrictor of "every"	DE	Inclusive
Positive sentence	UE	Exclusive
Negative sentence	DE	Inclusive

The Core Pattern

UE contexts: exclusive reading preferred

• "If everything goes well, we'll hire Mary or Sue"
• Default: we'll hire exactly one of them

DE contexts: inclusive reading preferred

• "If we hire Mary or Sue, everything will go well"
• Default: hiring either or both leads to success

Explanation via Maximize Strength

The asymmetry follows from the Maximize Strength principle:

• In UE: adding "not both" strengthens → compute SI
• In DE: adding "not both" would weaken → don't compute SI

When the exclusive SI is not computed, the inclusive reading emerges.

inductive Phenomena.Polarity.Studies.Chierchia2013.DisjunctionReading : Type

Type of disjunction interpretation.

• inclusive : DisjunctionReading
• exclusive : DisjunctionReading

@[implicit_reducible]

instance Phenomena.Polarity.Studies.Chierchia2013.instDecidableEqDisjunctionReading : DecidableEq DisjunctionReading

Equations

• Phenomena.Polarity.Studies.Chierchia2013.instDecidableEqDisjunctionReading x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Polarity.Studies.Chierchia2013.instReprDisjunctionReading.repr : DisjunctionReading → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Polarity.Studies.Chierchia2013.instReprDisjunctionReading : Repr DisjunctionReading

Equations

• Phenomena.Polarity.Studies.Chierchia2013.instReprDisjunctionReading = { reprPrec := Phenomena.Polarity.Studies.Chierchia2013.instReprDisjunctionReading.repr }

inductive Phenomena.Polarity.Studies.Chierchia2013.DisjunctionPosition : Type

Structural position of the disjunction.

• matrix : DisjunctionPosition
• conditional_cons : DisjunctionPosition
• conditionalAntecedent : DisjunctionPosition
• every_scope : DisjunctionPosition
• every_restrictor : DisjunctionPosition
• negation_scope : DisjunctionPosition

@[implicit_reducible]

instance Phenomena.Polarity.Studies.Chierchia2013.instDecidableEqDisjunctionPosition : DecidableEq DisjunctionPosition

Equations

• Phenomena.Polarity.Studies.Chierchia2013.instDecidableEqDisjunctionPosition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Polarity.Studies.Chierchia2013.instReprDisjunctionPosition.repr : DisjunctionPosition → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Polarity.Studies.Chierchia2013.instReprDisjunctionPosition : Repr DisjunctionPosition

Equations

• Phenomena.Polarity.Studies.Chierchia2013.instReprDisjunctionPosition = { reprPrec := Phenomena.Polarity.Studies.Chierchia2013.instReprDisjunctionPosition.repr }

def Phenomena.Polarity.Studies.Chierchia2013.positionPolarity : DisjunctionPosition → Core.NaturalLogic.ContextPolarity

Determine context polarity from position.

Equations

• Phenomena.Polarity.Studies.Chierchia2013.positionPolarity Phenomena.Polarity.Studies.Chierchia2013.DisjunctionPosition.matrix = Core.NaturalLogic.ContextPolarity.upward
• Phenomena.Polarity.Studies.Chierchia2013.positionPolarity Phenomena.Polarity.Studies.Chierchia2013.DisjunctionPosition.conditional_cons = Core.NaturalLogic.ContextPolarity.upward
• Phenomena.Polarity.Studies.Chierchia2013.positionPolarity Phenomena.Polarity.Studies.Chierchia2013.DisjunctionPosition.conditionalAntecedent = Core.NaturalLogic.ContextPolarity.downward
• Phenomena.Polarity.Studies.Chierchia2013.positionPolarity Phenomena.Polarity.Studies.Chierchia2013.DisjunctionPosition.every_scope = Core.NaturalLogic.ContextPolarity.upward
• Phenomena.Polarity.Studies.Chierchia2013.positionPolarity Phenomena.Polarity.Studies.Chierchia2013.DisjunctionPosition.every_restrictor = Core.NaturalLogic.ContextPolarity.downward
• Phenomena.Polarity.Studies.Chierchia2013.positionPolarity Phenomena.Polarity.Studies.Chierchia2013.DisjunctionPosition.negation_scope = Core.NaturalLogic.ContextPolarity.downward

def Phenomena.Polarity.Studies.Chierchia2013.predictReading : Core.NaturalLogic.ContextPolarity → DisjunctionReading

Predict preferred reading from polarity. UE → exclusive (SI computed), DE → inclusive (SI not computed). NM → inclusive (no clear strength ordering, so no exclusive SI).

Equations

• Phenomena.Polarity.Studies.Chierchia2013.predictReading Core.NaturalLogic.ContextPolarity.upward = Phenomena.Polarity.Studies.Chierchia2013.DisjunctionReading.exclusive
• Phenomena.Polarity.Studies.Chierchia2013.predictReading Core.NaturalLogic.ContextPolarity.downward = Phenomena.Polarity.Studies.Chierchia2013.DisjunctionReading.inclusive
• Phenomena.Polarity.Studies.Chierchia2013.predictReading Core.NaturalLogic.ContextPolarity.nonMonotonic = Phenomena.Polarity.Studies.Chierchia2013.DisjunctionReading.inclusive

structure Phenomena.Polarity.Studies.Chierchia2013.ExclusiveInclusiveExample : Type

Example showing exclusive/inclusive asymmetry.

• sentence : String

  The sentence

• position : DisjunctionPosition

  Position of disjunction

• polarity : Core.NaturalLogic.ContextPolarity

  Polarity of that position

• preferredReading : DisjunctionReading

  Preferred reading

• canForceOther : Bool

  Can the other reading be forced with context?

• source : String

  Source

def Phenomena.Polarity.Studies.Chierchia2013.instReprExclusiveInclusiveExample.repr : ExclusiveInclusiveExample → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Polarity.Studies.Chierchia2013.instReprExclusiveInclusiveExample : Repr ExclusiveInclusiveExample

Equations

• Phenomena.Polarity.Studies.Chierchia2013.instReprExclusiveInclusiveExample = { reprPrec := Phenomena.Polarity.Studies.Chierchia2013.instReprExclusiveInclusiveExample.repr }

def Phenomena.Polarity.Studies.Chierchia2013.hiring_consequent : ExclusiveInclusiveExample

Equations

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

def Phenomena.Polarity.Studies.Chierchia2013.hiring_antecedent : ExclusiveInclusiveExample

Equations

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

def Phenomena.Polarity.Studies.Chierchia2013.matrix_exclusive : ExclusiveInclusiveExample

Equations

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

def Phenomena.Polarity.Studies.Chierchia2013.every_scope : ExclusiveInclusiveExample

Equations

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

def Phenomena.Polarity.Studies.Chierchia2013.every_restrictor : ExclusiveInclusiveExample

Equations

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

def Phenomena.Polarity.Studies.Chierchia2013.negation_scope : ExclusiveInclusiveExample

Equations

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

def Phenomena.Polarity.Studies.Chierchia2013.exclusiveInclusiveExamples : List ExclusiveInclusiveExample

All exclusive/inclusive examples.

Equations

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

Forcing Non-Preferred Readings

While polarity determines the default reading, context can force the non-preferred interpretation:

Forcing Inclusive in UE (harder)

"If everything goes well, we'll hire Mary or Sue, or both."

• Explicit "or both" forces inclusive

Forcing Exclusive in DE (harder)

"If we hire Mary or Sue but not both, everything will go well."

• Explicit "but not both" forces exclusive

The observation: forcing requires explicit marking. The unmarked reading follows from Maximize Strength.

structure Phenomena.Polarity.Studies.Chierchia2013.ForcedReadingExample : Type

Example of forcing a non-preferred reading.

• baseSentence : String

  The base sentence

• position : DisjunctionPosition

  Position (determines default)

• defaultReading : DisjunctionReading

  Default reading

• forcingPhrase : String

  Forcing phrase

• forcedReading : DisjunctionReading

  Resulting reading

• notes : String

  Notes

@[implicit_reducible]

instance Phenomena.Polarity.Studies.Chierchia2013.instReprForcedReadingExample : Repr ForcedReadingExample

Equations

• Phenomena.Polarity.Studies.Chierchia2013.instReprForcedReadingExample = { reprPrec := Phenomena.Polarity.Studies.Chierchia2013.instReprForcedReadingExample.repr }

def Phenomena.Polarity.Studies.Chierchia2013.instReprForcedReadingExample.repr : ForcedReadingExample → ℕ → Std.Format

Equations

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

def Phenomena.Polarity.Studies.Chierchia2013.force_inclusive_ue : ForcedReadingExample

Equations

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

def Phenomena.Polarity.Studies.Chierchia2013.force_exclusive_de : ForcedReadingExample

Equations

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

def Phenomena.Polarity.Studies.Chierchia2013.forcedReadingExamples : List ForcedReadingExample

All forced reading examples.

Equations

• Phenomena.Polarity.Studies.Chierchia2013.forcedReadingExamples = [Phenomena.Polarity.Studies.Chierchia2013.force_inclusive_ue, Phenomena.Polarity.Studies.Chierchia2013.force_exclusive_de]

Universal Free Choice Items

Universal FCIs like English "any" and Italian "qualunque" contrast with existential FCIs (irgendein, yek-i, vreun) handled in @cite{alonso-ovalle-moghiseh-2025}:

FCI Type	Base Force	Examples	Morphological Hints
Existential	∃	irgendein, yek-i, vreun	Often contains "one"
Universal	∀	any, qualunque, whatever	Often wh-based

Chierchia's analysis

Both FCI types have the same underlying existential semantics. The universal force of "any" emerges from obligatory exhaustification of domain alternatives.

• "any" = ∃ + obligatory domain alternatives (always active)
• "some" = ∃ + optional domain alternatives (relevance-gated)

The "any" Distribution

1. NPI use (DE contexts): "I didn't see any students"

   • In DE, exhaustification is vacuous (domain alts are entailed)
   • Result: plain existential reading

2. FC use (modal contexts): "You may read any book"

   • Under modal, domain alts yield free choice
   • Result: universal-like permission

3. Generic use: "Any owl hunts mice" (subtrigging)

   • Generic contexts license FC reading
   • Result: universal generalization

Why "any" Fails in Positive Episodic Contexts

"*There are any cookies"

Exhaustifying domain alternatives in UE episodic contexts yields contradiction:

• ∃d∈D. P(d) (assertion)
• ∀d∈D. ¬[P(d) ∧ ∀y≠d.¬P(y)] (domain alt negation)

With two witnesses d₁, d₂: the second clause requires that for any d satisfying P, some other y also satisfies P. Combined with the first clause, this leads to infinite regress/contradiction for finite domains.

Contrast with "some"

"Some" has the same alternatives as "any", but they are optional. When not activated (low relevance), "some" = plain existential. "Any" must activate alternatives, hence the restricted distribution.

structure Phenomena.Polarity.Studies.Chierchia2013.UniversalFCI : Type

Universal FCI: existential with obligatorily active domain alternatives.

• baseIsExistential : Bool

  Base meaning is existential

• obligatoryDomainAlts : Bool

  Domain alternatives are always active (not relevance-gated)

• modalRescue : Bool

  Can be rescued via modal insertion

• genericRescue : Bool

  Can be rescued via generic/subtrigging

def Phenomena.Polarity.Studies.Chierchia2013.any_FCI : UniversalFCI

English "any" as a Universal FCI

Equations

• Phenomena.Polarity.Studies.Chierchia2013.any_FCI = { }

def Phenomena.Polarity.Studies.Chierchia2013.qualunque_FCI : UniversalFCI

Italian "qualunque" as a Universal FCI

Equations

• Phenomena.Polarity.Studies.Chierchia2013.qualunque_FCI = { }

inductive Phenomena.Polarity.Studies.Chierchia2013.UFCIContext : Type

Context type for determining Universal FCI distribution.

• positiveEpisodic : UFCIContext
• negation : UFCIContext
• conditionalAntecedent : UFCIContext
• deonticModal : UFCIContext
• epistemicModal : UFCIContext
• generic : UFCIContext
• question : UFCIContext

@[implicit_reducible]

instance Phenomena.Polarity.Studies.Chierchia2013.instDecidableEqUFCIContext : DecidableEq UFCIContext

Equations

• Phenomena.Polarity.Studies.Chierchia2013.instDecidableEqUFCIContext x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Polarity.Studies.Chierchia2013.instReprUFCIContext.repr : UFCIContext → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Polarity.Studies.Chierchia2013.instReprUFCIContext : Repr UFCIContext

Equations

• Phenomena.Polarity.Studies.Chierchia2013.instReprUFCIContext = { reprPrec := Phenomena.Polarity.Studies.Chierchia2013.instReprUFCIContext.repr }

inductive Phenomena.Polarity.Studies.Chierchia2013.UFCIReading : Type

Surface reading available to a Universal FCI.

Subset of the broader EFCI reading taxonomy: UFCIs only ever yield plain existential (NPI use, no exhaustification effect) or free choice (via modal/generic rescue). Uniqueness, modal variation, and epistemic ignorance are existential-FCI-specific readings.

• plainExistential : UFCIReading

  Plain existential (NPI use in DE contexts)

• freeChoice : UFCIReading

  Free choice (modal/generic rescue)

@[implicit_reducible]

instance Phenomena.Polarity.Studies.Chierchia2013.instDecidableEqUFCIReading : DecidableEq UFCIReading

Equations

• Phenomena.Polarity.Studies.Chierchia2013.instDecidableEqUFCIReading x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Polarity.Studies.Chierchia2013.instReprUFCIReading.repr : UFCIReading → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Polarity.Studies.Chierchia2013.instReprUFCIReading : Repr UFCIReading

Equations

• Phenomena.Polarity.Studies.Chierchia2013.instReprUFCIReading = { reprPrec := Phenomena.Polarity.Studies.Chierchia2013.instReprUFCIReading.repr }

def Phenomena.Polarity.Studies.Chierchia2013.ufciGrammatical (ctx : UFCIContext) : Bool

Universal FCI grammaticality prediction.

Ungrammatical only in positive episodic (UE without rescue).

Equations

• Phenomena.Polarity.Studies.Chierchia2013.ufciGrammatical Phenomena.Polarity.Studies.Chierchia2013.UFCIContext.positiveEpisodic = false
• Phenomena.Polarity.Studies.Chierchia2013.ufciGrammatical Phenomena.Polarity.Studies.Chierchia2013.UFCIContext.negation = true
• Phenomena.Polarity.Studies.Chierchia2013.ufciGrammatical Phenomena.Polarity.Studies.Chierchia2013.UFCIContext.conditionalAntecedent = true
• Phenomena.Polarity.Studies.Chierchia2013.ufciGrammatical Phenomena.Polarity.Studies.Chierchia2013.UFCIContext.deonticModal = true
• Phenomena.Polarity.Studies.Chierchia2013.ufciGrammatical Phenomena.Polarity.Studies.Chierchia2013.UFCIContext.epistemicModal = true
• Phenomena.Polarity.Studies.Chierchia2013.ufciGrammatical Phenomena.Polarity.Studies.Chierchia2013.UFCIContext.generic = true
• Phenomena.Polarity.Studies.Chierchia2013.ufciGrammatical Phenomena.Polarity.Studies.Chierchia2013.UFCIContext.question = true

def Phenomena.Polarity.Studies.Chierchia2013.ufciReading (ctx : UFCIContext) : Option UFCIReading

Reading obtained by Universal FCI in context.

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Polarity.Studies.Chierchia2013.ufciReading Phenomena.Polarity.Studies.Chierchia2013.UFCIContext.positiveEpisodic = none
• Phenomena.Polarity.Studies.Chierchia2013.ufciReading Phenomena.Polarity.Studies.Chierchia2013.UFCIContext.negation = some Phenomena.Polarity.Studies.Chierchia2013.UFCIReading.plainExistential
• Phenomena.Polarity.Studies.Chierchia2013.ufciReading Phenomena.Polarity.Studies.Chierchia2013.UFCIContext.deonticModal = some Phenomena.Polarity.Studies.Chierchia2013.UFCIReading.freeChoice
• Phenomena.Polarity.Studies.Chierchia2013.ufciReading Phenomena.Polarity.Studies.Chierchia2013.UFCIContext.epistemicModal = some Phenomena.Polarity.Studies.Chierchia2013.UFCIReading.freeChoice
• Phenomena.Polarity.Studies.Chierchia2013.ufciReading Phenomena.Polarity.Studies.Chierchia2013.UFCIContext.generic = some Phenomena.Polarity.Studies.Chierchia2013.UFCIReading.freeChoice
• Phenomena.Polarity.Studies.Chierchia2013.ufciReading Phenomena.Polarity.Studies.Chierchia2013.UFCIContext.question = some Phenomena.Polarity.Studies.Chierchia2013.UFCIReading.plainExistential

theorem Phenomena.Polarity.Studies.Chierchia2013.any_in_de_is_existential : ufciReading UFCIContext.negation = some UFCIReading.plainExistential

In DE contexts, exhaustifying "any"'s alternatives yields entailments, so the exhaustification is vacuous and "any" = plain existential.

This explains the NPI distribution of "any".

theorem Phenomena.Polarity.Studies.Chierchia2013.any_negation_plain : ufciReading UFCIContext.negation = some UFCIReading.plainExistential

"I didn't see any students" ≡ "I didn't see a student"

The "any" contributes no special meaning in DE contexts.

theorem Phenomena.Polarity.Studies.Chierchia2013.any_modal_fc : ufciReading UFCIContext.deonticModal = some UFCIReading.freeChoice

Under modals, "any" yields free choice via exhaustification.

"You may read any book" = For each book x, you may read x

theorem Phenomena.Polarity.Studies.Chierchia2013.any_rescued_by_modal : ufciGrammatical UFCIContext.deonticModal = true

Modal insertion is the rescue mechanism for Universal FCIs.

theorem Phenomena.Polarity.Studies.Chierchia2013.any_positive_episodic_bad : ufciGrammatical UFCIContext.positiveEpisodic = false

"*There are any cookies" is ungrammatical.

Domain alternative exhaustification in UE episodic context yields contradiction.

theorem Phenomena.Polarity.Studies.Chierchia2013.any_positive_contradiction : ufciReading UFCIContext.positiveEpisodic = none

The failure mechanism: exhaustification is G-contradictory. (See Core.Analyticity for G-triviality/L-analyticity)

structure Phenomena.Polarity.Studies.Chierchia2013.AnyExample : Type

An "any" distribution example.

• sentence : String
• context : UFCIContext
• grammatical : Bool
• reading : Option String
• notes : String

@[implicit_reducible]

instance Phenomena.Polarity.Studies.Chierchia2013.instReprAnyExample : Repr AnyExample

Equations

• Phenomena.Polarity.Studies.Chierchia2013.instReprAnyExample = { reprPrec := Phenomena.Polarity.Studies.Chierchia2013.instReprAnyExample.repr }

def Phenomena.Polarity.Studies.Chierchia2013.instReprAnyExample.repr : AnyExample → ℕ → Std.Format

Equations

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

def Phenomena.Polarity.Studies.Chierchia2013.any_positive_bad : AnyExample

Equations

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

def Phenomena.Polarity.Studies.Chierchia2013.any_negation_ok : AnyExample

Equations

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

def Phenomena.Polarity.Studies.Chierchia2013.any_deontic_ok : AnyExample

Equations

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

def Phenomena.Polarity.Studies.Chierchia2013.any_generic_ok : AnyExample

Equations

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

def Phenomena.Polarity.Studies.Chierchia2013.any_question_ok : AnyExample

Equations

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

def Phenomena.Polarity.Studies.Chierchia2013.any_conditional_ok : AnyExample

Equations

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

def Phenomena.Polarity.Studies.Chierchia2013.anyExamples : List AnyExample

Equations

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