@cite{meyer-feiman-2021} — Composing Alternatives

@cite{bar-lev-fox-2017} @cite{chierchia-2004} @cite{fox-2007}

Structural priming evidence that scalar and free choice implicatures decompose into independently parameterizable sub-computations.

Citation

Meyer, M.-C. & Feiman, R. (2021). Composing alternatives: The structural source of scalar and free choice implicatures. Journal of Memory and Language, 121, 104279.

Core Contribution

Implicature computation factors into two sub-operations:

1. ALT-GEN (alternative generation): Computing what the speaker could have said
2. ALT-NEG (alternative negation): Strengthening by negating the un-uttered alternatives

Each sub-operation can independently be online (computed during processing) or offline (pre-stored with the lexical entry). This gives a spectrum of processing architectures:

Item	ALT-GEN	ALT-NEG	Category
some	online	online	Quantifier
three	offline	online	Numeral
FC or	—	different mech	FC disjunction

Experimental Evidence (6 experiments)

Structural priming paradigm: if two expressions share a sub-computation, processing one facilitates processing the other.

• Exp 1–2: some → numerals (bidirectional priming)
• Exp 3–4: numerals → some (bidirectional priming)
• Exp 5: FC or → some (NO priming)
• Exp 6: FC or → numerals (NO priming)

The pattern falsifies any uniform account: shared ALT-NEG between some and numerals, but FC uses an entirely different mechanism (assertion-based per @cite{bar-lev-fox-2017}, not negation-based).

Processing Architecture Types

inductive MeyerFeiman2021.AltGenSource : Type

How alternatives are made available during processing.

Meyer & Feiman's key theoretical distinction (§1.2, §5):

• online: alternatives computed from the Horn scale at processing time (e.g., some → {most, all} derived from ⟨some, most, all⟩)
• offline: alternatives stored with the lexical entry (e.g., three → {one, two, four,...} stored in the numeral system)

• online : AltGenSource

  Computed from Horn scale at processing time

• offline : AltGenSource

  Pre-stored with lexical entry

@[implicit_reducible]

instance MeyerFeiman2021.instDecidableEqAltGenSource : DecidableEq AltGenSource

Equations

• MeyerFeiman2021.instDecidableEqAltGenSource x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def MeyerFeiman2021.instReprAltGenSource.repr : AltGenSource → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance MeyerFeiman2021.instReprAltGenSource : Repr AltGenSource

Equations

• MeyerFeiman2021.instReprAltGenSource = { reprPrec := MeyerFeiman2021.instReprAltGenSource.repr }

@[implicit_reducible]

instance MeyerFeiman2021.instInhabitedAltGenSource : Inhabited AltGenSource

Equations

• MeyerFeiman2021.instInhabitedAltGenSource = { default := MeyerFeiman2021.instInhabitedAltGenSource.default }

def MeyerFeiman2021.instInhabitedAltGenSource.default : AltGenSource

Equations

• MeyerFeiman2021.instInhabitedAltGenSource.default = MeyerFeiman2021.AltGenSource.online

inductive MeyerFeiman2021.AltNegMechanism : Type

What is done with alternatives once generated.

The mechanism by which un-uttered alternatives contribute to meaning:

• exhaustification: negate alternatives (standard SI: "not all")
• innocentInclusion: assert alternatives (FC: "may A ∧ may B")
• none: no strengthening operation applies

• exhaustification : AltNegMechanism

  IE: negate alternatives (standard scalar implicature)

• innocentInclusion : AltNegMechanism

  II: assert alternatives (free choice inference)

• none : AltNegMechanism

  No strengthening

@[implicit_reducible]

instance MeyerFeiman2021.instDecidableEqAltNegMechanism : DecidableEq AltNegMechanism

Equations

• MeyerFeiman2021.instDecidableEqAltNegMechanism x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance MeyerFeiman2021.instReprAltNegMechanism : Repr AltNegMechanism

Equations

• MeyerFeiman2021.instReprAltNegMechanism = { reprPrec := MeyerFeiman2021.instReprAltNegMechanism.repr }

def MeyerFeiman2021.instReprAltNegMechanism.repr : AltNegMechanism → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance MeyerFeiman2021.instInhabitedAltNegMechanism : Inhabited AltNegMechanism

Equations

• MeyerFeiman2021.instInhabitedAltNegMechanism = { default := MeyerFeiman2021.instInhabitedAltNegMechanism.default }

def MeyerFeiman2021.instInhabitedAltNegMechanism.default : AltNegMechanism

Equations

• MeyerFeiman2021.instInhabitedAltNegMechanism.default = MeyerFeiman2021.AltNegMechanism.exhaustification

structure MeyerFeiman2021.ProcessProfile : Type

A scalar item's implicature processing profile.

Combines ALT-GEN source and ALT-NEG mechanism to classify how a given scalar item's implicature is computed. Meyer & Feiman argue that these two dimensions are independently parameterizable (§5).

• altGen : AltGenSource

  How alternatives are generated

• altNeg : AltNegMechanism

  What is done with alternatives

def MeyerFeiman2021.instDecidableEqProcessProfile.decEq (x✝ x✝¹ : ProcessProfile) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance MeyerFeiman2021.instDecidableEqProcessProfile : DecidableEq ProcessProfile

Equations

• MeyerFeiman2021.instDecidableEqProcessProfile = MeyerFeiman2021.instDecidableEqProcessProfile.decEq

def MeyerFeiman2021.instReprProcessProfile.repr : ProcessProfile → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance MeyerFeiman2021.instReprProcessProfile : Repr ProcessProfile

Equations

• MeyerFeiman2021.instReprProcessProfile = { reprPrec := MeyerFeiman2021.instReprProcessProfile.repr }

@[implicit_reducible]

instance MeyerFeiman2021.instInhabitedProcessProfile : Inhabited ProcessProfile

Equations

• MeyerFeiman2021.instInhabitedProcessProfile = { default := { altGen := MeyerFeiman2021.AltGenSource.online, altNeg := MeyerFeiman2021.AltNegMechanism.exhaustification } }

Scalar Item Classification

inductive MeyerFeiman2021.ScalarItemClass : Type

The three classes of scalar item distinguished by Meyer & Feiman.

The paper argues these are not merely taxonomic labels but reflect genuine processing differences, as demonstrated by the priming pattern.

• quantifier : ScalarItemClass

  Quantifiers: ALT-GEN online, ALT-NEG online (§2.1)

• numeral : ScalarItemClass

  Numerals: ALT-GEN offline, ALT-NEG online (§2.2)

• freeChoiceDisjunction : ScalarItemClass

  Free choice disjunction: different mechanism entirely (§2.3)

@[implicit_reducible]

instance MeyerFeiman2021.instDecidableEqScalarItemClass : DecidableEq ScalarItemClass

Equations

• MeyerFeiman2021.instDecidableEqScalarItemClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def MeyerFeiman2021.instReprScalarItemClass.repr : ScalarItemClass → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance MeyerFeiman2021.instReprScalarItemClass : Repr ScalarItemClass

Equations

• MeyerFeiman2021.instReprScalarItemClass = { reprPrec := MeyerFeiman2021.instReprScalarItemClass.repr }

def MeyerFeiman2021.instInhabitedScalarItemClass.default : ScalarItemClass

Equations

• MeyerFeiman2021.instInhabitedScalarItemClass.default = MeyerFeiman2021.ScalarItemClass.quantifier

@[implicit_reducible]

instance MeyerFeiman2021.instInhabitedScalarItemClass : Inhabited ScalarItemClass

Equations

• MeyerFeiman2021.instInhabitedScalarItemClass = { default := MeyerFeiman2021.instInhabitedScalarItemClass.default }

def MeyerFeiman2021.classProfile : ScalarItemClass → ProcessProfile

The process profile for each scalar item class.

This is the paper's central theoretical claim (Table 1, §5).

Equations

• MeyerFeiman2021.classProfile MeyerFeiman2021.ScalarItemClass.quantifier = { altGen := MeyerFeiman2021.AltGenSource.online, altNeg := MeyerFeiman2021.AltNegMechanism.exhaustification }
• MeyerFeiman2021.classProfile MeyerFeiman2021.ScalarItemClass.numeral = { altGen := MeyerFeiman2021.AltGenSource.offline, altNeg := MeyerFeiman2021.AltNegMechanism.exhaustification }
• MeyerFeiman2021.classProfile MeyerFeiman2021.ScalarItemClass.freeChoiceDisjunction = { altGen := MeyerFeiman2021.AltGenSource.online, altNeg := MeyerFeiman2021.AltNegMechanism.innocentInclusion }

inductive MeyerFeiman2021.ScalarItem : Type

Concrete scalar items used in the experiments.

• some_ : ScalarItem
• three : ScalarItem
• four : ScalarItem
• fcOr : ScalarItem

@[implicit_reducible]

instance MeyerFeiman2021.instDecidableEqScalarItem : DecidableEq ScalarItem

Equations

• MeyerFeiman2021.instDecidableEqScalarItem x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance MeyerFeiman2021.instReprScalarItem : Repr ScalarItem

Equations

• MeyerFeiman2021.instReprScalarItem = { reprPrec := MeyerFeiman2021.instReprScalarItem.repr }

def MeyerFeiman2021.instReprScalarItem.repr : ScalarItem → ℕ → Std.Format

Equations

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

def MeyerFeiman2021.itemClass : ScalarItem → ScalarItemClass

Classify a concrete item into its class.

Equations

• MeyerFeiman2021.itemClass MeyerFeiman2021.ScalarItem.some_ = MeyerFeiman2021.ScalarItemClass.quantifier
• MeyerFeiman2021.itemClass MeyerFeiman2021.ScalarItem.three = MeyerFeiman2021.ScalarItemClass.numeral
• MeyerFeiman2021.itemClass MeyerFeiman2021.ScalarItem.four = MeyerFeiman2021.ScalarItemClass.numeral
• MeyerFeiman2021.itemClass MeyerFeiman2021.ScalarItem.fcOr = MeyerFeiman2021.ScalarItemClass.freeChoiceDisjunction

def MeyerFeiman2021.itemProfile (item : ScalarItem) : ProcessProfile

Get the process profile for a concrete item.

Equations

• MeyerFeiman2021.itemProfile item = MeyerFeiman2021.classProfile (MeyerFeiman2021.itemClass item)

Priming Predictions

Meyer & Feiman's reasoning (§2.3, §5):

• Two items prime each other iff they share a sub-computation
• Shared ALT-NEG → cross-category priming (some ↔ numerals)
• Different ALT-NEG → no priming (FC ↮ some, FC ↮ numerals)
• Shared vs different ALT-GEN → asymmetry in priming strength

def MeyerFeiman2021.sharesAltNeg (a b : ScalarItemClass) : Bool

Whether two scalar item classes share ALT-NEG.

Equations

• MeyerFeiman2021.sharesAltNeg a b = ((MeyerFeiman2021.classProfile a).altNeg == (MeyerFeiman2021.classProfile b).altNeg)

def MeyerFeiman2021.sharesAltGen (a b : ScalarItemClass) : Bool

Whether two scalar item classes share ALT-GEN.

Equations

• MeyerFeiman2021.sharesAltGen a b = ((MeyerFeiman2021.classProfile a).altGen == (MeyerFeiman2021.classProfile b).altGen)

def MeyerFeiman2021.predictsPriming (a b : ScalarItemClass) : Bool

Predicted priming between two classes: occurs iff shared ALT-NEG.

Equations

• MeyerFeiman2021.predictsPriming a b = MeyerFeiman2021.sharesAltNeg a b

Experimental Data

structure MeyerFeiman2021.PrimingExperiment : Type

Result of a structural priming experiment.

Each experiment tests whether processing a scalar implicature with one item type facilitates processing with another.

• experiment : String

  Experiment identifier

• primeClass : ScalarItemClass

  Prime scalar item class

• targetClass : ScalarItemClass

  Target scalar item class

• primingObserved : Bool

  Was significant priming observed?

• nParticipants : ℕ

  Number of participants

• effectDescription : String

  Effect description

def MeyerFeiman2021.instReprPrimingExperiment.repr : PrimingExperiment → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance MeyerFeiman2021.instReprPrimingExperiment : Repr PrimingExperiment

Equations

• MeyerFeiman2021.instReprPrimingExperiment = { reprPrec := MeyerFeiman2021.instReprPrimingExperiment.repr }

def MeyerFeiman2021.exp1_2 : PrimingExperiment

Experiments 1–2: some primes numerals.

Equations

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

def MeyerFeiman2021.exp3_4 : PrimingExperiment

Experiments 3–4: numerals prime some.

Equations

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

def MeyerFeiman2021.exp5 : PrimingExperiment

Experiment 5: FC or does NOT prime some.

Equations

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

def MeyerFeiman2021.exp6 : PrimingExperiment

Experiment 6: FC or does NOT prime numerals.

Equations

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

def MeyerFeiman2021.allExperiments : List PrimingExperiment

All experiments from @cite{meyer-feiman-2021}.

Equations

• MeyerFeiman2021.allExperiments = [MeyerFeiman2021.exp1_2, MeyerFeiman2021.exp3_4, MeyerFeiman2021.exp5, MeyerFeiman2021.exp6]

Key Empirical Findings

structure MeyerFeiman2021.MainFindings : Type

The three main findings of the paper (§5).

• someNumeralPriming : Bool

  Finding 1: Bidirectional priming between some and numerals

• noFCSomePriming : Bool

  Finding 2: No priming between FC or and some

• noFCNumeralPriming : Bool

  Finding 3: No priming between FC or and numerals

def MeyerFeiman2021.instReprMainFindings.repr : MainFindings → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance MeyerFeiman2021.instReprMainFindings : Repr MainFindings

Equations

• MeyerFeiman2021.instReprMainFindings = { reprPrec := MeyerFeiman2021.instReprMainFindings.repr }

def MeyerFeiman2021.mainFindings : MainFindings

Equations

• MeyerFeiman2021.mainFindings = { someNumeralPriming := true, noFCSomePriming := true, noFCNumeralPriming := true }

Connections to Other Phenomena

The process profile classification connects to several existing phenomena in linglib.

def MeyerFeiman2021.scaleProfile (scale : Phenomena.ScalarImplicatures.HornScaleDatum) : ProcessProfile

For each scale in the library's basic data, which process profile applies.

This connects Meyer & Feiman's classification to the Horn scale data in Phenomena.ScalarImplicatures.Basic.

Equations

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

def MeyerFeiman2021.hurfordNumeralProfile : ProcessProfile

Numeral Hurford rescue (e.g., "three or all") involves the offline/online profile — alternatives are stored, so exhaustification ("exactly three") is immediately available for Hurford rescue.

Equations

• MeyerFeiman2021.hurfordNumeralProfile = MeyerFeiman2021.classProfile MeyerFeiman2021.ScalarItemClass.numeral

def MeyerFeiman2021.freeChoiceProfile : ProcessProfile

FC phenomena use a fundamentally different mechanism from standard SI.

This connects to Phenomena.FreeChoice, where the FC inference ◇(A ∨ B) → ◇A ∧ ◇B is derived via Innocent Inclusion rather than Innocent Exclusion.

Equations

• MeyerFeiman2021.freeChoiceProfile = MeyerFeiman2021.classProfile MeyerFeiman2021.ScalarItemClass.freeChoiceDisjunction

structure MeyerFeiman2021.SIvsFCContrast : Type

The asymmetry between SI and FC is a processing architecture difference, not just a semantic difference. Both involve alternatives, but:

• SI: negate alternatives (IE)
• FC: assert alternatives (II)

• siMechanism : AltNegMechanism

  Standard SI mechanism

• fcMechanism : AltNegMechanism

  FC mechanism

• sameMechanism : Bool

  Are they the same?

def MeyerFeiman2021.instReprSIvsFCContrast.repr : SIvsFCContrast → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance MeyerFeiman2021.instReprSIvsFCContrast : Repr SIvsFCContrast

Equations

• MeyerFeiman2021.instReprSIvsFCContrast = { reprPrec := MeyerFeiman2021.instReprSIvsFCContrast.repr }

def MeyerFeiman2021.siVsFc : SIvsFCContrast

Equations

• MeyerFeiman2021.siVsFc = { siMechanism := MeyerFeiman2021.AltNegMechanism.exhaustification, fcMechanism := MeyerFeiman2021.AltNegMechanism.innocentInclusion, sameMechanism := false }

Falsified Accounts

Meyer & Feiman's data rules out several theoretical positions (§5).

inductive MeyerFeiman2021.TheoreticalPosition : Type

Theoretical positions about scalar inference processing.

• uniformOnline : TheoreticalPosition

  All scalar inferences use the same online computation

• uniformOffline : TheoreticalPosition

  All scalar inferences use stored/default meanings

• decomposed : TheoreticalPosition

  Scalar items differ in ALT-GEN but share ALT-NEG (M&F's position)

• fullyIndependent : TheoreticalPosition

  Each scalar item class is fully independent

@[implicit_reducible]

instance MeyerFeiman2021.instDecidableEqTheoreticalPosition : DecidableEq TheoreticalPosition

Equations

• MeyerFeiman2021.instDecidableEqTheoreticalPosition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def MeyerFeiman2021.instReprTheoreticalPosition.repr : TheoreticalPosition → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance MeyerFeiman2021.instReprTheoreticalPosition : Repr TheoreticalPosition

Equations

• MeyerFeiman2021.instReprTheoreticalPosition = { reprPrec := MeyerFeiman2021.instReprTheoreticalPosition.repr }

def MeyerFeiman2021.compatibleWithData (pos : TheoreticalPosition) : Bool

Whether a theoretical position is compatible with the priming data.

Equations

• MeyerFeiman2021.compatibleWithData MeyerFeiman2021.TheoreticalPosition.uniformOnline = false
• MeyerFeiman2021.compatibleWithData MeyerFeiman2021.TheoreticalPosition.uniformOffline = false
• MeyerFeiman2021.compatibleWithData MeyerFeiman2021.TheoreticalPosition.decomposed = true
• MeyerFeiman2021.compatibleWithData MeyerFeiman2021.TheoreticalPosition.fullyIndependent = false

theorem MeyerFeiman2021.quantifier_numeral_shared_altNeg : sharesAltNeg ScalarItemClass.quantifier ScalarItemClass.numeral = true

Quantifiers and numerals share ALT-NEG (both use exhaustification).

theorem MeyerFeiman2021.quantifier_numeral_different_altGen : sharesAltGen ScalarItemClass.quantifier ScalarItemClass.numeral = false

Quantifiers and numerals differ on ALT-GEN.

theorem MeyerFeiman2021.fc_quantifier_different_altNeg : sharesAltNeg ScalarItemClass.freeChoiceDisjunction ScalarItemClass.quantifier = false

FC uses a different ALT-NEG mechanism from quantifiers.

theorem MeyerFeiman2021.fc_numeral_different_altNeg : sharesAltNeg ScalarItemClass.freeChoiceDisjunction ScalarItemClass.numeral = false

FC uses a different ALT-NEG mechanism from numerals.

theorem MeyerFeiman2021.some_three_same_altNeg : (itemProfile ScalarItem.some_).altNeg = (itemProfile ScalarItem.three).altNeg

some and three share exhaustification.

theorem MeyerFeiman2021.some_three_different_altGen : (itemProfile ScalarItem.some_).altGen ≠ (itemProfile ScalarItem.three).altGen

some and three differ on ALT-GEN source.

theorem MeyerFeiman2021.fcOr_some_different_mechanism : (itemProfile ScalarItem.fcOr).altNeg ≠ (itemProfile ScalarItem.some_).altNeg

FC or uses a completely different mechanism from some.

theorem MeyerFeiman2021.exp1_2_matches_prediction : exp1_2.primingObserved = predictsPriming exp1_2.primeClass exp1_2.targetClass

Exp 1–2: priming predicted (shared ALT-NEG) and observed.

theorem MeyerFeiman2021.exp3_4_matches_prediction : exp3_4.primingObserved = predictsPriming exp3_4.primeClass exp3_4.targetClass

Exp 3–4: priming predicted (shared ALT-NEG) and observed.

theorem MeyerFeiman2021.exp5_matches_prediction : exp5.primingObserved = predictsPriming exp5.primeClass exp5.targetClass

Exp 5: no priming predicted (different ALT-NEG) and none observed.

theorem MeyerFeiman2021.exp6_matches_prediction : exp6.primingObserved = predictsPriming exp6.primeClass exp6.targetClass

Exp 6: no priming predicted (different ALT-NEG) and none observed.

theorem MeyerFeiman2021.all_experiments_match : (allExperiments.all fun (e : PrimingExperiment) => e.primingObserved == predictsPriming e.primeClass e.targetClass) = true

All experiments match the profile-based prediction.

theorem MeyerFeiman2021.decomposed_compatible : compatibleWithData TheoreticalPosition.decomposed = true

The decomposed account is compatible with the data.

theorem MeyerFeiman2021.uniform_online_falsified : compatibleWithData TheoreticalPosition.uniformOnline = false

The uniform-online account is falsified.

theorem MeyerFeiman2021.uniform_offline_falsified : compatibleWithData TheoreticalPosition.uniformOffline = false

The uniform-offline account is falsified.

theorem MeyerFeiman2021.fully_independent_falsified : compatibleWithData TheoreticalPosition.fullyIndependent = false

The fully-independent account is falsified.

theorem MeyerFeiman2021.exactly_one_survives : List.filter compatibleWithData [TheoreticalPosition.uniformOnline, TheoreticalPosition.uniformOffline, TheoreticalPosition.decomposed, TheoreticalPosition.fullyIndependent] = [TheoreticalPosition.decomposed]

Exactly one of the four positions survives the data.

theorem MeyerFeiman2021.quantifier_scale_online : (scaleProfile Phenomena.ScalarImplicatures.quantifierScale).altGen = AltGenSource.online

The quantifier scale ⟨some, all⟩ has an online ALT-GEN profile.

theorem MeyerFeiman2021.numeral_scale_offline : (scaleProfile Phenomena.ScalarImplicatures.numeralScale).altGen = AltGenSource.offline

The numeral scale ⟨1, 2, 3,...⟩ has an offline ALT-GEN profile.

theorem MeyerFeiman2021.both_scales_exhaust : (scaleProfile Phenomena.ScalarImplicatures.quantifierScale).altNeg = (scaleProfile Phenomena.ScalarImplicatures.numeralScale).altNeg

Both quantifier and numeral scales share ALT-NEG = exhaustification.

theorem MeyerFeiman2021.connective_scale_exhaust : (scaleProfile Phenomena.ScalarImplicatures.connectiveScale).altNeg = AltNegMechanism.exhaustification

The connective scale ⟨or, and⟩ (standard, non-FC) also uses exhaustification.

theorem MeyerFeiman2021.hurford_numeral_rescue_available : hurfordNumeralProfile.altGen = AltGenSource.offline

Numeral Hurford rescue: "three or all" is rescued because exh(three) = "exactly three" is available via offline alternatives.

theorem MeyerFeiman2021.hurford_same_neg_mechanism : hurfordNumeralProfile.altNeg = (scaleProfile Phenomena.ScalarImplicatures.quantifierScale).altNeg

Both rescued-numeral and rescued-quantifier Hurford cases use the same strengthening mechanism (exhaustification).

theorem MeyerFeiman2021.fc_uses_inclusion : freeChoiceProfile.altNeg = AltNegMechanism.innocentInclusion

FC uses innocent inclusion, not exhaustification.

theorem MeyerFeiman2021.si_fc_different_mechanisms : siVsFc.sameMechanism = false

The SI/FC contrast is a processing architecture difference.

theorem MeyerFeiman2021.fc_data_distinct_from_si : (classProfile ScalarItemClass.freeChoiceDisjunction).altNeg ≠ (classProfile ScalarItemClass.quantifier).altNeg

FC data items are correctly classified as having a distinct mechanism from standard SI data items.

theorem MeyerFeiman2021.fc_cancellable_consistent : Phenomena.FreeChoice.explicitCancellation.felicitous = true

FC cancellability (from FreeChoice.lean) is consistent with the FC profile using innocentInclusion.

theorem MeyerFeiman2021.all_involve_alternatives : ([ScalarItemClass.quantifier, ScalarItemClass.numeral, ScalarItemClass.freeChoiceDisjunction].all fun (c : ScalarItemClass) => (classProfile c).altNeg != AltNegMechanism.none) = true

All three classes share the property of being scalar (involving alternatives), but differ in processing architecture.

theorem MeyerFeiman2021.all_profiles_distinct : classProfile ScalarItemClass.quantifier ≠ classProfile ScalarItemClass.numeral ∧ classProfile ScalarItemClass.quantifier ≠ classProfile ScalarItemClass.freeChoiceDisjunction ∧ classProfile ScalarItemClass.numeral ≠ classProfile ScalarItemClass.freeChoiceDisjunction

No two of the three classes have identical process profiles.