inductive Phenomena.Polarity.Studies.Schwab2022.Condition : Type

Condition in the 2×3 design

• grammatical : Condition
• illusion : Condition
• ungrammatical : Condition

instance Phenomena.Polarity.Studies.Schwab2022.instDecidableEqCondition : DecidableEq Condition

Equations

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

instance Phenomena.Polarity.Studies.Schwab2022.instBEqCondition : BEq Condition

Equations

• Phenomena.Polarity.Studies.Schwab2022.instBEqCondition = { beq := Phenomena.Polarity.Studies.Schwab2022.instBEqCondition.beq }

def Phenomena.Polarity.Studies.Schwab2022.instBEqCondition.beq : Condition → Condition → Bool

Equations

• Phenomena.Polarity.Studies.Schwab2022.instBEqCondition.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Polarity.Studies.Schwab2022.instReprCondition : Repr Condition

Equations

• Phenomena.Polarity.Studies.Schwab2022.instReprCondition = { reprPrec := Phenomena.Polarity.Studies.Schwab2022.instReprCondition.repr }

def Phenomena.Polarity.Studies.Schwab2022.instReprCondition.repr : Condition → Nat → Std.Format

Equations

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

inductive Phenomena.Polarity.Studies.Schwab2022.NPIType : Type

NPI type tested

• strengthening : NPIType
• attenuating : NPIType

instance Phenomena.Polarity.Studies.Schwab2022.instDecidableEqNPIType : DecidableEq NPIType

Equations

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

def Phenomena.Polarity.Studies.Schwab2022.instBEqNPIType.beq : NPIType → NPIType → Bool

Equations

• Phenomena.Polarity.Studies.Schwab2022.instBEqNPIType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Polarity.Studies.Schwab2022.instBEqNPIType : BEq NPIType

Equations

• Phenomena.Polarity.Studies.Schwab2022.instBEqNPIType = { beq := Phenomena.Polarity.Studies.Schwab2022.instBEqNPIType.beq }

def Phenomena.Polarity.Studies.Schwab2022.instReprNPIType.repr : NPIType → Nat → Std.Format

Equations

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

instance Phenomena.Polarity.Studies.Schwab2022.instReprNPIType : Repr NPIType

Equations

• Phenomena.Polarity.Studies.Schwab2022.instReprNPIType = { reprPrec := Phenomena.Polarity.Studies.Schwab2022.instReprNPIType.repr }

structure Phenomena.Polarity.Studies.Schwab2022.ExperimentalDatum : Type

A single experimental datum

• npiType : NPIType
• condition : Condition
• acceptanceRate : Float

  Mean acceptance rate (0–1)

• bayesFactor : Float

  Bayes factor for grammaticality (BF₁₀ > 3 = substantial evidence)

• accepted : Bool

  Accepted as grammatical? (BF₁₀ > 3)

instance Phenomena.Polarity.Studies.Schwab2022.instReprExperimentalDatum : Repr ExperimentalDatum

Equations

• Phenomena.Polarity.Studies.Schwab2022.instReprExperimentalDatum = { reprPrec := Phenomena.Polarity.Studies.Schwab2022.instReprExperimentalDatum.repr }

def Phenomena.Polarity.Studies.Schwab2022.instReprExperimentalDatum.repr : ExperimentalDatum → Nat → Std.Format

Equations

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

def Phenomena.Polarity.Studies.Schwab2022.jemals_grammatical : ExperimentalDatum

jemals (strengthening) in grammatical condition

Equations

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

def Phenomena.Polarity.Studies.Schwab2022.jemals_illusion : ExperimentalDatum

jemals (strengthening) in illusion condition — ACCEPTED (illusion!)

Equations

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

def Phenomena.Polarity.Studies.Schwab2022.jemals_ungrammatical : ExperimentalDatum

jemals (strengthening) in ungrammatical condition

Equations

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

def Phenomena.Polarity.Studies.Schwab2022.soRecht_grammatical : ExperimentalDatum

soRecht (attenuating) in grammatical condition

Equations

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

def Phenomena.Polarity.Studies.Schwab2022.soRecht_illusion : ExperimentalDatum

soRecht (attenuating) in illusion condition — REJECTED (no illusion!)

Equations

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

def Phenomena.Polarity.Studies.Schwab2022.soRecht_ungrammatical : ExperimentalDatum

soRecht (attenuating) in ungrammatical condition

Equations

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

def Phenomena.Polarity.Studies.Schwab2022.experimentalData : List ExperimentalDatum

All experimental data

Equations

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

structure Phenomena.Polarity.Studies.Schwab2022.IllusionAsymmetry : Type

The illusion asymmetry: strengthening NPIs show illusion, attenuating don't.

• strengtheningIllusion : Bool

  Strengthening NPIs accepted in illusion condition

• attenuatingIllusion : Bool

  Attenuating NPIs accepted in illusion condition

• asymmetry : self.strengtheningIllusion = true ∧ self.attenuatingIllusion = false

  The asymmetry holds: strengthening shows illusion, attenuating doesn't

def Phenomena.Polarity.Studies.Schwab2022.observedAsymmetry : IllusionAsymmetry

The observed illusion asymmetry from Experiment 2

Equations

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

def Phenomena.Polarity.Studies.Schwab2022.npiTypeToScalarDirection : NPIType → Core.Lexical.PolarityItem.ScalarDirection

Map from NPI type to scalar direction

Equations

• Phenomena.Polarity.Studies.Schwab2022.npiTypeToScalarDirection Phenomena.Polarity.Studies.Schwab2022.NPIType.strengthening = Core.Lexical.PolarityItem.ScalarDirection.strengthening
• Phenomena.Polarity.Studies.Schwab2022.npiTypeToScalarDirection Phenomena.Polarity.Studies.Schwab2022.NPIType.attenuating = Core.Lexical.PolarityItem.ScalarDirection.attenuating

def Phenomena.Polarity.Studies.Schwab2022.predictsIllusion (npi : NPIType) : Bool

Predict whether an NPI type shows illusion based on scalar direction. Only strengthening NPIs show illusion because the RC environment superficially satisfies the "stronger-than-alternatives" licensing condition of ScalAssert.

Equations

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

theorem Phenomena.Polarity.Studies.Schwab2022.illusion_asymmetry_from_scalar_direction : predictsIllusion NPIType.strengthening = true ∧ predictsIllusion NPIType.attenuating = false

Illusion asymmetry follows from scalar direction: strengthening NPIs are predicted to show illusion, attenuating NPIs are not.