inductive Phenomena.Presupposition.Studies.LoGuercio2025.ACIJudgment : Type

Judgment status for whether an ACI arises.

• arises : ACIJudgment
• doesNotArise : ACIJudgment
• marginal : ACIJudgment

instance Phenomena.Presupposition.Studies.LoGuercio2025.instDecidableEqACIJudgment : DecidableEq ACIJudgment

Equations

• Phenomena.Presupposition.Studies.LoGuercio2025.instDecidableEqACIJudgment x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Presupposition.Studies.LoGuercio2025.instBEqACIJudgment.beq : ACIJudgment → ACIJudgment → Bool

Equations

• Phenomena.Presupposition.Studies.LoGuercio2025.instBEqACIJudgment.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Presupposition.Studies.LoGuercio2025.instBEqACIJudgment : BEq ACIJudgment

Equations

• Phenomena.Presupposition.Studies.LoGuercio2025.instBEqACIJudgment = { beq := Phenomena.Presupposition.Studies.LoGuercio2025.instBEqACIJudgment.beq }

instance Phenomena.Presupposition.Studies.LoGuercio2025.instReprACIJudgment : Repr ACIJudgment

Equations

• Phenomena.Presupposition.Studies.LoGuercio2025.instReprACIJudgment = { reprPrec := Phenomena.Presupposition.Studies.LoGuercio2025.instReprACIJudgment.repr }

def Phenomena.Presupposition.Studies.LoGuercio2025.instReprACIJudgment.repr : ACIJudgment → Nat → Std.Format

Equations

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

structure Phenomena.Presupposition.Studies.LoGuercio2025.EmpiricalItem : Type

A single empirical item from the paper.

• exampleNum : String

  Example number(s) from the paper

• sentence : String

  The sentence tested

• potentialACI : String

  The potential ACI content

• judgment : ACIJudgment

  Whether the ACI arises empirically

• priorContext : Option String

  Prior context (if any)

instance Phenomena.Presupposition.Studies.LoGuercio2025.instReprEmpiricalItem : Repr EmpiricalItem

Equations

• Phenomena.Presupposition.Studies.LoGuercio2025.instReprEmpiricalItem = { reprPrec := Phenomena.Presupposition.Studies.LoGuercio2025.instReprEmpiricalItem.repr }

def Phenomena.Presupposition.Studies.LoGuercio2025.instReprEmpiricalItem.repr : EmpiricalItem → Nat → Std.Format

Equations

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

def Phenomena.Presupposition.Studies.LoGuercio2025.ex18_outOfBlue_noACI : EmpiricalItem

Example (18): Out of the blue, NO epithet ACI.

"John arrived late." ⇝̸ ¬(John is a bastard)

Out of the blue, there's no inference that the speaker doesn't dislike John. The epithet alternative is not contextually relevant.

Equations

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

def Phenomena.Presupposition.Studies.LoGuercio2025.ex19_spanish_outOfBlue : EmpiricalItem

Example (19): Spanish honorific parallel, out of the blue.

"Diego entró." ⇝̸ ¬(speaker respects Diego)

Same pattern: no ACI without prior mention of honorific.

Equations

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

def Phenomena.Presupposition.Studies.LoGuercio2025.ex20_priorMention_ACI : EmpiricalItem

Example (20): With prior epithet mention, ACI arises.

Context: "John arrived first, then that bastard Pedro arrived." "John arrived" ⇝ ¬(John is a bastard)

When "bastard" is mentioned for Pedro, using bare "John" triggers the ACI.

Equations

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

def Phenomena.Presupposition.Studies.LoGuercio2025.ex21_contrastive_ACI : EmpiricalItem

Example (21): Contrastive epithet ACI.

"Juan arrived first, then that bastard Pedro arrived." ⇝ ¬(Juan is a bastard)

The asymmetry in CI content (bastard for Pedro, not Juan) triggers the ACI.

Equations

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

def Phenomena.Presupposition.Studies.LoGuercio2025.ex22_23_honorific_ACI : EmpiricalItem

Example (22)-(23): Spanish honorific ACI.

"Primero entró Donato. Después entró Don Pedro." ⇝ ¬(speaker respects Donato)

When "Don" is used for Pedro but not Donato, ACI arises.

Equations

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

def Phenomena.Presupposition.Studies.LoGuercio2025.ex31_32_appositive_ACI : EmpiricalItem

Example (31)-(32): Nominal appositive ACI.

"Diego recommended an aspirin. Laura, a doctor, recommended an antibiotic." ⇝ ¬(Diego is a doctor)

The appositive "a doctor" for Laura triggers ACI about Diego.

Equations

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

structure Phenomena.Presupposition.Studies.LoGuercio2025.PropertyTest : Type

Property test data structure.

• property : String

  Property being tested

• exampleNum : String

  Example number

• sentence : String

  Test sentence

• propertyHolds : Bool

  Result: does the property hold?

• comparison : Option String

  Comparison: how does this differ from SIs/antipresuppositions?

def Phenomena.Presupposition.Studies.LoGuercio2025.instReprPropertyTest.repr : PropertyTest → Nat → Std.Format

Equations

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

instance Phenomena.Presupposition.Studies.LoGuercio2025.instReprPropertyTest : Repr PropertyTest

Equations

• Phenomena.Presupposition.Studies.LoGuercio2025.instReprPropertyTest = { reprPrec := Phenomena.Presupposition.Studies.LoGuercio2025.instReprPropertyTest.repr }

def Phenomena.Presupposition.Studies.LoGuercio2025.ex50_different_assertion : PropertyTest

Example (50): ACIs do not require same assertive content.

"Juan called María or that bastard Pedro" ACI: ¬(María is a bastard)

Even though the stronger alternative "Juan called María and that bastard Pedro" has different assertive content (and vs or), the ACI still arises.

This distinguishes ACIs from antipresuppositions (which do require same assertion).

Equations

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

def Phenomena.Presupposition.Studies.LoGuercio2025.ex52_cancellable : PropertyTest

Example (52): ACIs are cancellable.

"Juan arrived first, then that bastard Pedro arrived (by the way, Juan is also a bastard)"

The parenthetical cancels the ACI.

Equations

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

def Phenomena.Presupposition.Studies.LoGuercio2025.ex61_de_insensitive : PropertyTest

Example (61): ACIs not affected by downward-entailing contexts.

"I doubt that Juan or that bastard Pedro passed" SI blocked: ⇝̸ ¬(I doubt Juan and Pedro passed) ACI not blocked: ⇝ ¬(Juan is a bastard)

DE context blocks the scalar implicature but not the ACI.

Equations

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

def Phenomena.Presupposition.Studies.LoGuercio2025.ex63_reinforceable : PropertyTest

Example (63): ACIs are reinforceable.

"Juan arrived first, that bastard Pedro arrived second (by the way, Juan is not a bastard)"

The reinforcement is informative, not redundant (unlike presupposition reinforcement).

Equations

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

structure Phenomena.Presupposition.Studies.LoGuercio2025.InferenceTypeComparison : Type

Comparison of scalar inference types from Lo Guercio Table 1.

• name : String

  Inference type name

• requiresSameAssertion : Bool

  Does it require same assertive content?

• affectedByDE : Bool

  Is it affected by DE contexts?

• cancellable : Bool

  Is it cancellable?

• reinforceable : Bool

  Is it reinforceable (without redundancy)?

def Phenomena.Presupposition.Studies.LoGuercio2025.instReprInferenceTypeComparison.repr : InferenceTypeComparison → Nat → Std.Format

Equations

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

instance Phenomena.Presupposition.Studies.LoGuercio2025.instReprInferenceTypeComparison : Repr InferenceTypeComparison

Equations

• Phenomena.Presupposition.Studies.LoGuercio2025.instReprInferenceTypeComparison = { reprPrec := Phenomena.Presupposition.Studies.LoGuercio2025.instReprInferenceTypeComparison.repr }

def Phenomena.Presupposition.Studies.LoGuercio2025.siComparison : InferenceTypeComparison

Scalar Implicature properties from Lo Guercio

Equations

• Phenomena.Presupposition.Studies.LoGuercio2025.siComparison = { name := "Scalar Implicature", requiresSameAssertion := false, affectedByDE := true, cancellable := true, reinforceable := true }

def Phenomena.Presupposition.Studies.LoGuercio2025.antipresupComparison : InferenceTypeComparison

Antipresupposition properties from Lo Guercio

Equations

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

def Phenomena.Presupposition.Studies.LoGuercio2025.aciComparison : InferenceTypeComparison

ACI properties from Lo Guercio

Equations

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

inductive Phenomena.Presupposition.Studies.LoGuercio2025.CIExpressionType : Type

CI expression types tested in the paper.

• epithet : CIExpressionType
• honorific : CIExpressionType
• nominalAppositive : CIExpressionType
• supplementaryAdverb : CIExpressionType
• emotiveMarker : CIExpressionType

instance Phenomena.Presupposition.Studies.LoGuercio2025.instDecidableEqCIExpressionType : DecidableEq CIExpressionType

Equations

• Phenomena.Presupposition.Studies.LoGuercio2025.instDecidableEqCIExpressionType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Presupposition.Studies.LoGuercio2025.instBEqCIExpressionType.beq : CIExpressionType → CIExpressionType → Bool

Equations

• Phenomena.Presupposition.Studies.LoGuercio2025.instBEqCIExpressionType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Presupposition.Studies.LoGuercio2025.instBEqCIExpressionType : BEq CIExpressionType

Equations

• Phenomena.Presupposition.Studies.LoGuercio2025.instBEqCIExpressionType = { beq := Phenomena.Presupposition.Studies.LoGuercio2025.instBEqCIExpressionType.beq }

def Phenomena.Presupposition.Studies.LoGuercio2025.instReprCIExpressionType.repr : CIExpressionType → Nat → Std.Format

Equations

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

instance Phenomena.Presupposition.Studies.LoGuercio2025.instReprCIExpressionType : Repr CIExpressionType

Equations

• Phenomena.Presupposition.Studies.LoGuercio2025.instReprCIExpressionType = { reprPrec := Phenomena.Presupposition.Studies.LoGuercio2025.instReprCIExpressionType.repr }

def Phenomena.Presupposition.Studies.LoGuercio2025.expressionTypeCoverage : List (CIExpressionType × String × Bool)

Evidence for ACI arising with each expression type.

Equations

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