structure Phenomena.Negation.DoubleNegation.DNEDatum : Type

A DNE datum comparing original and double-negated versions.

• original : String

  The original sentence with indefinite

• doubleNegated : String

  The double-negated version

• followUp : String

  Follow-up sentence with anaphora

• anaphor : String

  The anaphoric element

• originalFelicitous : Bool

  Is original + follow-up felicitous?

• doubleNegFelicitous : Bool

  Is double-negated + follow-up felicitous?

• shouldBeEquivalent : Bool

  Should they be equivalent (by DNE)?

• notes : String

  Notes

• source : String

  Source

@[implicit_reducible]

instance Phenomena.Negation.DoubleNegation.instReprDNEDatum : Repr DNEDatum

Equations

• Phenomena.Negation.DoubleNegation.instReprDNEDatum = { reprPrec := Phenomena.Negation.DoubleNegation.instReprDNEDatum.repr }

def Phenomena.Negation.DoubleNegation.instReprDNEDatum.repr : DNEDatum → Nat → Std.Format

Equations

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

def Phenomena.Negation.DoubleNegation.basicExistential : DNEDatum

Basic existential

Equations

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

def Phenomena.Negation.DoubleNegation.bathroomDNE : DNEDatum

Bathroom pattern

Equations

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

def Phenomena.Negation.DoubleNegation.complexDNE : DNEDatum

More complex structure

Equations

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

structure Phenomena.Negation.DoubleNegation.StandardDSPrediction : Type

In standard dynamic semantics, DNE fails for anaphora.

The negative dimension "traps" discourse referents.

• sentence : String
• standardDSResult : String
• drefAccessible : Bool
• notes : String

@[implicit_reducible]

instance Phenomena.Negation.DoubleNegation.instReprStandardDSPrediction : Repr StandardDSPrediction

Equations

• Phenomena.Negation.DoubleNegation.instReprStandardDSPrediction = { reprPrec := Phenomena.Negation.DoubleNegation.instReprStandardDSPrediction.repr }

def Phenomena.Negation.DoubleNegation.instReprStandardDSPrediction.repr : StandardDSPrediction → Nat → Std.Format

Equations

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

def Phenomena.Negation.DoubleNegation.standardDSNegation : StandardDSPrediction

Equations

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

def Phenomena.Negation.DoubleNegation.standardDSDoubleNeg : StandardDSPrediction

Equations

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

structure Phenomena.Negation.DoubleNegation.BUSPrediction : Type

In bilateral semantics, negation swaps positive and negative.

¬¬φ = φ definitionally, so DNE holds for anaphora.

• sentence : String
• positiveUpdate : String
• negativeUpdate : String
• drefAccessible : Bool
• notes : String

def Phenomena.Negation.DoubleNegation.instReprBUSPrediction.repr : BUSPrediction → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Negation.DoubleNegation.instReprBUSPrediction : Repr BUSPrediction

Equations

• Phenomena.Negation.DoubleNegation.instReprBUSPrediction = { reprPrec := Phenomena.Negation.DoubleNegation.instReprBUSPrediction.repr }

def Phenomena.Negation.DoubleNegation.busNegation : BUSPrediction

Equations

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

def Phenomena.Negation.DoubleNegation.busDoubleNeg : BUSPrediction

Equations

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

structure Phenomena.Negation.DoubleNegation.ICDRTPrediction : Type

In ICDRT, drefs are introduced globally (flat), tracked by propositional drefs.

• sentence : String
• flatUpdate : String
• propDref : String
• drefAccessible : Bool
• notes : String

def Phenomena.Negation.DoubleNegation.instReprICDRTPrediction.repr : ICDRTPrediction → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Negation.DoubleNegation.instReprICDRTPrediction : Repr ICDRTPrediction

Equations

• Phenomena.Negation.DoubleNegation.instReprICDRTPrediction = { reprPrec := Phenomena.Negation.DoubleNegation.instReprICDRTPrediction.repr }

def Phenomena.Negation.DoubleNegation.icdrtNegation : ICDRTPrediction

Equations

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

def Phenomena.Negation.DoubleNegation.icdrtDoubleNeg : ICDRTPrediction

Equations

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

structure Phenomena.Negation.DoubleNegation.JudgmentDatum : Type

Empirical judgment on DNE felicity.

• discourse : List String
• felicitous : Bool
• certainty : String
• notes : String
• source : String

@[implicit_reducible]

instance Phenomena.Negation.DoubleNegation.instReprJudgmentDatum : Repr JudgmentDatum

Equations

• Phenomena.Negation.DoubleNegation.instReprJudgmentDatum = { reprPrec := Phenomena.Negation.DoubleNegation.instReprJudgmentDatum.repr }

def Phenomena.Negation.DoubleNegation.instReprJudgmentDatum.repr : JudgmentDatum → Nat → Std.Format

Equations

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

def Phenomena.Negation.DoubleNegation.clearOriginal : JudgmentDatum

Clear case: original

Equations

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

def Phenomena.Negation.DoubleNegation.clearNegBlocks : JudgmentDatum

Clear case: single negation blocks

Equations

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

def Phenomena.Negation.DoubleNegation.testDoubleNeg : JudgmentDatum

Test case: double negation

Equations

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

def Phenomena.Negation.DoubleNegation.naturalDoubleNeg : JudgmentDatum

More natural double negation

Equations

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

def Phenomena.Negation.DoubleNegation.tripleNegation : DNEDatum

Triple negation: ¬¬¬φ = ¬φ

Equations

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

def Phenomena.Negation.DoubleNegation.dneData : List DNEDatum

All DNE test cases

Equations

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

def Phenomena.Negation.DoubleNegation.standardDSPredictions : List StandardDSPrediction

Standard DS predictions

Equations

• Phenomena.Negation.DoubleNegation.standardDSPredictions = [Phenomena.Negation.DoubleNegation.standardDSNegation, Phenomena.Negation.DoubleNegation.standardDSDoubleNeg]

def Phenomena.Negation.DoubleNegation.busPredictions : List BUSPrediction

BUS predictions

Equations

• Phenomena.Negation.DoubleNegation.busPredictions = [Phenomena.Negation.DoubleNegation.busNegation, Phenomena.Negation.DoubleNegation.busDoubleNeg]

def Phenomena.Negation.DoubleNegation.icdrtPredictions : List ICDRTPrediction

ICDRT predictions

Equations

• Phenomena.Negation.DoubleNegation.icdrtPredictions = [Phenomena.Negation.DoubleNegation.icdrtNegation, Phenomena.Negation.DoubleNegation.icdrtDoubleNeg]

def Phenomena.Negation.DoubleNegation.judgments : List JudgmentDatum

Empirical judgments

Equations

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