English Negation Fragment

@cite{miestamo-2005} @cite{dryer-haspelmath-2013}

English expresses standard negation with the particle not (contracted n't). WALS classifies English as both symmetric and asymmetric (SymAsy):

• Symmetric: with modals, be, and have, negation simply adds not with no structural change: He can swim → He cannot swim.

• Asymmetric (A/Cat): with lexical verbs, negation introduces auxiliary do (do-support): He eats → He does not eat. This is a category-level change — the finite verb becomes an auxiliary, and the lexical verb appears as a bare infinitive.

Negative indefinites (Ch 115)

WALS classifies English as mixed:

• nobody, nothing preclude predicate negation: Nobody came / *Nobody didn't come
• anything, ever require predicate negation: I didn't see anything / *I saw anything

def Fragments.English.Negation.negMarker : String

The standard negation particle.

Equations

• Fragments.English.Negation.negMarker = "not"

def Fragments.English.Negation.negContracted : String

The contracted form.

Equations

• Fragments.English.Negation.negContracted = "n't"

structure Fragments.English.Negation.NegExample : Type

An English negation example.

• affirmative : String
• negative : String
• glossAff : String
• glossNeg : String
• doSupport : Bool

  Does this construction require do-support?

• symmetric : Bool

  Is this construction symmetric (neg = aff + neg marker, no other change)?

instance Fragments.English.Negation.instReprNegExample : Repr NegExample

Equations

• Fragments.English.Negation.instReprNegExample = { reprPrec := Fragments.English.Negation.instReprNegExample.repr }

def Fragments.English.Negation.instReprNegExample.repr : NegExample → Nat → Std.Format

Equations

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

instance Fragments.English.Negation.instBEqNegExample : BEq NegExample

Equations

• Fragments.English.Negation.instBEqNegExample = { beq := Fragments.English.Negation.instBEqNegExample.beq }

def Fragments.English.Negation.instBEqNegExample.beq : NegExample → NegExample → Bool

Equations

• One or more equations did not get rendered due to their size.
• Fragments.English.Negation.instBEqNegExample.beq x✝¹ x✝ = false

def Fragments.English.Negation.modal : NegExample

Modal can: symmetric (no do-support).

Equations

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

def Fragments.English.Negation.copula : NegExample

Copula be: symmetric (no do-support).

Equations

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

def Fragments.English.Negation.auxHave : NegExample

Auxiliary have: symmetric (no do-support).

Equations

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

def Fragments.English.Negation.lexicalPresent : NegExample

Lexical verb, present: asymmetric (do-support required).

Equations

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

def Fragments.English.Negation.lexicalPast : NegExample

Lexical verb, past: asymmetric (do-support required).

Equations

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

def Fragments.English.Negation.allExamples : List NegExample

Equations

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

Verification

theorem Fragments.English.Negation.negMarker_is_not : negMarker = "not"

theorem Fragments.English.Negation.all_examples_count : allExamples.length = 5

theorem Fragments.English.Negation.symasy_distribution : (List.filter (fun (x : NegExample) => x.symmetric) allExamples).length = 3 ∧ (List.filter (fun (e : NegExample) => !e.symmetric) allExamples).length = 2

3 symmetric + 2 asymmetric = SymAsy.

theorem Fragments.English.Negation.asymmetric_iff_dosupport : (allExamples.all fun (e : NegExample) => e.symmetric == !e.doSupport) = true

Asymmetric constructions all involve do-support.

theorem Fragments.English.Negation.symmetric_no_dosupport : ((List.filter (fun (x : NegExample) => x.symmetric) allExamples).all fun (e : NegExample) => !e.doSupport) = true

Symmetric constructions do not involve do-support.