Miestamo (2005): Standard Negation

This file formalizes Miestamo's typology of standard negation. The negation of a declarative verbal main clause is symmetric when the negative differs from an affirmative only by the presence of the negative marker and asymmetric when further structural differences accompany it. A pair is symmetric when its negative is its affirmative with the marker inserted (IsSymmetric), and a construction is symmetric in its paradigm when its negative is some affirmative of the paradigm with the marker inserted (IsSymmetricIn), as the English negative of a simple tense is symmetric with the emphatic affirmative. Paradigms are asymmetric by the asymmetries found in them, symmetric paradigms being identified only by their absence (ParadigmAsymmetric): a paradigm neutralizes when distinct affirmatives share their negative (Neutralizes) and displaces when the negative of one member is built on the affirmative of another while the negatives stay distinct (Displaces). Paradigmatic asymmetry is therefore not neutralization: Tunica builds the negative of the habitual on the semelfactive and keeps the two apart by their markers (exists_paradigmAsymmetric_not_neutralizes). A language is of type Sym when neither its constructions nor its paradigms show asymmetry, of type Asy when every construction is asymmetric, and of type SymAsy otherwise (languageType), so the definitional cells of the book's fourth table follow (languageType_eq_symmetric_iff, languageType_eq_asymmetric_iff).

The types are instantiated on the book's examples, the rows of Data.Examples.Miestamo2005, each language's pairs being its negative rows with the affirmatives they cite and its fragment's standard negator as the marker, the German and Italian paradigms by their first person singular. Spanish, German, Italian, French and Russian are of type Sym. The Finnish negative auxiliary takes the ending of the finite verb and leaves the lexical verb without it; the plain Japanese negative inflects as an adjective, a less finite form than the verb; Maori negates with an initial negative verb, and Hixkaryana deverbalizes the lexical verb under an added copula: finiteness asymmetries, and type Asy. Mandarin and Turkish mix symmetric and asymmetric constructions. Burmese replaces its three postverbal tense–aspect markers with one negative suffix, asymmetric in construction and neutralizing in paradigm. The English negative is symmetric with the emphatic affirmative, not with the plain one, to which it adds do, and the paradigm loses the emphatic distinction of the simple tenses. The Imbabura Quechua negative is the polar interrogative with mana added, and has the interrogative's validator -chu where the declarative has -mi, on Cole's examples.

Implementation notes

A row's morphs are the forms of its text split at word and morph boundaries, and a pair compares forms; each language's theorem states that its rows are formed into pairs (Formed), so that no pair a row cites is lost. Forms that Miestamo sets aside as phonological are cited in one shape (cite): the Turkish negative -mE- as -mA- and the glide of the future -yecek, the Tunica vowel loss of lɔ'ta-w-ɛhɛ and its negative as -aha, the Hixkaryana -hra as -hɨra, and the French elided n'. The Mandarin constructions are compared through what each negator adds and excludes, the book giving no minimal pairs for them. The subtypes of asymmetry are not represented: Adds identifies an added element, the mark of the finite-element constructions, but which category a lost or changed marker belongs to is not recorded in a pair. Different-system asymmetry and paradigmatic gaps are not represented either, and nor are the representative sample and its frequency tables.

TODO

The Quechua asymmetry is paradigmatic displacement onto the interrogative, A/NonReal/Displc; its statement as Displaces needs an affirmative interrogative and a negative interrogative of one predicate and person, which the examples entered here do not give; Cole's grammar may supply them.

References

• [Mie05]
• [Col82]

Pairs from the rows

@[reducible, inline]

abbrev Miestamo2005.Form : Type

A morph form, as its characters.

Equations

• Miestamo2005.Form = List Char

def Miestamo2005.toForm (s : String) : Form

The form of a string.

Equations

• Miestamo2005.toForm s = s.toList

structure Miestamo2005.Pair : Type

An affirmative and the negative a marker forms from it, as the forms of their morphs in surface order.

• marker : Negation.Marker

  The marker of the negative.

• affirmative : List Form

  The affirmative.

• negative : List Form

  The negative.

def Miestamo2005.instDecidableEqPair.decEq (x✝ x✝¹ : Pair) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miestamo2005.instDecidableEqPair : DecidableEq Pair

Equations

• Miestamo2005.instDecidableEqPair = Miestamo2005.instDecidableEqPair.decEq

def Miestamo2005.Pair.markerForms (p : Pair) : List Form

The forms of a marker's morphs.

Equations

• p.markerForms = List.map (fun (x : Morphology.Morph) => Miestamo2005.toForm x.form) p.marker.morphs

def Miestamo2005.citations : List (Glottocode × String × String)

The forms set aside as phonological, by language, with the shape they are cited in.

Equations

• Miestamo2005.citations = [("nucl1301", "me", "mA"), ("nucl1301", "yecek", "ecek"), ("tuni1252", "w", "wi"), ("tuni1252", "ɛhɛ", "aha"), ("hixk1239", "hra", "hɨra"), ("stan1290", "n'", "ne")]

def Miestamo2005.cite (l : Glottocode) (f : Form) : Form

The citation form of a morph in a language.

Equations

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

def Miestamo2005.forms (e : Datum) : List Form

The cited forms of the morphs of a row's text.

Equations

• Miestamo2005.forms e = List.map (Miestamo2005.cite e.language) (Morphology.Morph.wordsOf e.primaryText).flatten

def Miestamo2005.standard : Glottocode → List Negation.Marker

The standard negators of a language, from its fragment.

Equations

• Miestamo2005.standard "stan1288" = Spanish.Negation.standard
• Miestamo2005.standard "stan1295" = German.Negation.standard
• Miestamo2005.standard "ital1282" = Italian.Negation.standard
• Miestamo2005.standard "stan1290" = French.Negation.standard
• Miestamo2005.standard "russ1263" = Russian.Negation.standard
• Miestamo2005.standard "finn1318" = Finnish.Negation.standard
• Miestamo2005.standard "nucl1643" = Japanese.Negation.standard
• Miestamo2005.standard "maor1246" = Maori.Negation.standard
• Miestamo2005.standard "hixk1239" = Hixkaryana.Negation.standard
• Miestamo2005.standard "nucl1301" = Turkish.Negation.standard
• Miestamo2005.standard "nucl1310" = Burmese.Negation.standard
• Miestamo2005.standard "stan1293" = English.Negation.standard
• Miestamo2005.standard "tuni1252" = Tunica.Negation.standard
• Miestamo2005.standard x✝ = []

def Miestamo2005.rows (l : Glottocode) : List Datum

The rows of a language.

Equations

• Miestamo2005.rows l = List.filter (fun (x : Datum) => decide (x.language = l)) Miestamo2005.Examples.all

def Miestamo2005.pairsOf (rs : List Datum) (n : Datum) : List Pair

The pairs a negative row forms with the affirmatives among rs it cites, the marker being the standard negator whose morphs the negative contains.

Equations

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

def Miestamo2005.pairs (l : Glottocode) : List Pair

The pairs of a language.

Equations

• Miestamo2005.pairs l = List.flatMap (Miestamo2005.pairsOf (Miestamo2005.rows l)) (Miestamo2005.rows l)

def Miestamo2005.Formed (l : Glottocode) : Prop

A language's rows are formed into pairs when it has rows and each negative forms a pair with every affirmative it cites.

Equations

• Miestamo2005.Formed l = (Miestamo2005.rows l ≠ [] ∧ ∀ n ∈ Miestamo2005.rows l, (Miestamo2005.pairsOf (Miestamo2005.rows l) n).length = (n.features "affirmative").length)

@[instance_reducible]

instance Miestamo2005.instDecidableFormed (l : Glottocode) : Decidable (Formed l)

Equations

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

Constructions

def Miestamo2005.IsSymmetric (p : Pair) : Prop

A construction is symmetric when the negative is the affirmative with the negative marker inserted: the affirmative is a sublist of the negative, and the two differ by exactly the marker's morphs.

Equations

• Miestamo2005.IsSymmetric p = (p.affirmative.Sublist p.negative ∧ p.negative.Perm (p.affirmative ++ p.markerForms))

@[instance_reducible]

instance Miestamo2005.instDecidablePredPairIsSymmetric : DecidablePred IsSymmetric

Equations

• Miestamo2005.instDecidablePredPairIsSymmetric p = { decide := decide (p.affirmative.Sublist p.negative) && decide (p.negative.Perm (p.affirmative ++ p.markerForms)), reflects_decide := ⋯ }

def Miestamo2005.IsSymmetricIn (ps : List Pair) (p : Pair) : Prop

A construction is symmetric in a paradigm when its negative is some affirmative of the paradigm with its marker inserted.

Equations

• Miestamo2005.IsSymmetricIn ps p = ∃ q ∈ ps, Miestamo2005.IsSymmetric { marker := p.marker, affirmative := q.affirmative, negative := p.negative }

@[instance_reducible]

instance Miestamo2005.instDecidablePredPairIsSymmetricIn (ps : List Pair) : DecidablePred (IsSymmetricIn ps)

Equations

• Miestamo2005.instDecidablePredPairIsSymmetricIn ps p = Miestamo2005.instDecidablePredPairIsSymmetricIn._aux_1 ps p

theorem Miestamo2005.IsSymmetric.isSymmetricIn {ps : List Pair} {p : Pair} (hp : p ∈ ps) (h : IsSymmetric p) : IsSymmetricIn ps p

def Miestamo2005.Adds (p : Pair) : Prop

The negative contains an element, other than the marker, that the affirmative lacks, as the constructions that add a finite element do.

Equations

• Miestamo2005.Adds p = ∃ x ∈ p.negative, x ∉ p.markerForms ∧ x ∉ p.affirmative

@[instance_reducible]

instance Miestamo2005.instDecidablePredPairAdds : DecidablePred Adds

Equations

• Miestamo2005.instDecidablePredPairAdds p = Miestamo2005.instDecidablePredPairAdds._aux_1 p

theorem Miestamo2005.not_isSymmetric_of_adds {p : Pair} (h : Adds p) : ¬IsSymmetric p

A construction that adds an element is asymmetric.

Paradigms

def Miestamo2005.Neutralizes (ps : List Pair) : Prop

A paradigm neutralizes when distinct affirmatives share their negative.

Equations

• Miestamo2005.Neutralizes ps = ∃ p ∈ ps, ∃ q ∈ ps, p.affirmative ≠ q.affirmative ∧ p.negative = q.negative

def Miestamo2005.Displaces (ps : List Pair) : Prop

A paradigm displaces when the negative of one member is the affirmative of another with the first member's marker inserted, while the two negatives stay distinct.

Equations

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

def Miestamo2005.ParadigmAsymmetric (ps : List Pair) : Prop

A paradigm is asymmetric when it neutralizes or displaces: symmetric paradigms are those in which no asymmetry is found.

Equations

• Miestamo2005.ParadigmAsymmetric ps = (Miestamo2005.Neutralizes ps ∨ Miestamo2005.Displaces ps)

@[instance_reducible]

instance Miestamo2005.instDecidableNeutralizes (ps : List Pair) : Decidable (Neutralizes ps)

Equations

• Miestamo2005.instDecidableNeutralizes ps = Miestamo2005.instDecidableNeutralizes._aux_1 ps

@[instance_reducible]

instance Miestamo2005.instDecidableDisplaces (ps : List Pair) : Decidable (Displaces ps)

Equations

• Miestamo2005.instDecidableDisplaces ps = Miestamo2005.instDecidableDisplaces._aux_1 ps

@[instance_reducible]

instance Miestamo2005.instDecidableParadigmAsymmetric (ps : List Pair) : Decidable (ParadigmAsymmetric ps)

Equations

• Miestamo2005.instDecidableParadigmAsymmetric ps = { decide := decide (Miestamo2005.Neutralizes ps) || decide (Miestamo2005.Displaces ps), reflects_decide := ⋯ }

Language types

def Miestamo2005.languageType {α : Type u_1} (cs : List α) (sym : α → Prop) [DecidablePred sym] (paradigmAsymmetric : Prop) [Decidable paradigmAsymmetric] : Data.WALS.F113A.NegationSymmetry

The three types of language, from the symmetry of each construction and whether some paradigm is asymmetric: symmetric negation when no asymmetry is found, asymmetric when every construction is asymmetric, and both otherwise.

Equations

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

@[reducible, inline]

abbrev Miestamo2005.pairsType (ps : List Pair) : Data.WALS.F113A.NegationSymmetry

The type of a language whose constructions form the paradigm ps.

Equations

• Miestamo2005.pairsType ps = Miestamo2005.languageType ps (Miestamo2005.IsSymmetricIn ps) (Miestamo2005.ParadigmAsymmetric ps)

theorem Miestamo2005.languageType_eq_symmetric_iff {α : Type u_1} (cs : List α) (sym : α → Prop) [DecidablePred sym] (P : Prop) [Decidable P] : languageType cs sym P = Data.WALS.F113A.NegationSymmetry.symmetric ↔ (∀ c ∈ cs, sym c) ∧ ¬P

theorem Miestamo2005.languageType_eq_asymmetric_iff {α : Type u_1} (cs : List α) (sym : α → Prop) [DecidablePred sym] (P : Prop) [Decidable P] (hne : cs ≠ []) : languageType cs sym P = Data.WALS.F113A.NegationSymmetry.asymmetric ↔ ∀ c ∈ cs, ¬sym c

A language with only asymmetric constructions is of type Asy whatever its paradigms.

theorem Miestamo2005.languageType_eq_both_iff {α : Type u_1} (cs : List α) (sym : α → Prop) [DecidablePred sym] (P : Prop) [Decidable P] : languageType cs sym P = Data.WALS.F113A.NegationSymmetry.both ↔ (∃ c ∈ cs, sym c) ∧ ((∃ c ∈ cs, ¬sym c) ∨ P)

Type SymAsy has a symmetric construction by definition, together with some asymmetry.

Paradigmatic displacement: Tunica

theorem Miestamo2005.tunica_displaces : Formed "tuni1252" ∧ (∀ p ∈ pairs "tuni1252", IsSymmetricIn (pairs "tuni1252") p) ∧ Displaces (pairs "tuni1252") ∧ ¬Neutralizes (pairs "tuni1252")

Tunica negates the habitual on the semelfactive form, (5): each construction is symmetric in the paradigm, and the paradigm displaces without neutralizing, the two negative markers keeping the aspects apart.

theorem Miestamo2005.exists_paradigmAsymmetric_not_neutralizes : ∃ (ps : List Pair), ParadigmAsymmetric ps ∧ ¬Neutralizes ps

Paradigmatic asymmetry does not always lead to neutralization.

Symmetric negation: Spanish, German, Italian, French, Russian

theorem Miestamo2005.spanish_symmetric : Formed "stan1288" ∧ pairsType (pairs "stan1288") = Data.WALS.F113A.NegationSymmetry.symmetric

theorem Miestamo2005.german_symmetric : Formed "stan1295" ∧ pairsType (pairs "stan1295") = Data.WALS.F113A.NegationSymmetry.symmetric

theorem Miestamo2005.italian_symmetric : Formed "ital1282" ∧ pairsType (pairs "ital1282") = Data.WALS.F113A.NegationSymmetry.symmetric

theorem Miestamo2005.french_symmetric : Formed "stan1290" ∧ pairsType (pairs "stan1290") = Data.WALS.F113A.NegationSymmetry.symmetric

Both members of the French double marker are removed.

theorem Miestamo2005.russian_symmetric : Formed "russ1263" ∧ pairsType (pairs "russ1263") = Data.WALS.F113A.NegationSymmetry.symmetric

Finiteness asymmetry: Finnish, Japanese, Maori, Hixkaryana

theorem Miestamo2005.finnish_negVerb : Finnish.Negation.ending.cells = Agreement.Bundle.personNumberCells ∧ Formed "finn1318" ∧ (∀ p ∈ pairs "finn1318", p.negative = p.markerForms ++ p.affirmative.reverse) ∧ pairsType (pairs "finn1318") = Data.WALS.F113A.NegationSymmetry.asymmetric

The Finnish negative auxiliary has an ending for every person and number, and in the negative of a stem with its ending the auxiliary takes the ending and the stem follows bare: the negative verb is the finite element of the clause, and the language is of type Asy.

theorem Miestamo2005.japanese_negative_adjectival : Formed "nucl1643" ∧ ∀ p ∈ pairs "nucl1643", p.marker = Japanese.Negation.na → ∃ e ∈ List.map (fun (x : Morphology.Morph) => toForm x.form) Japanese.Negation.adjectivalEndings, p.negative = List.take 1 p.affirmative ++ p.markerForms ++ [e] ∧ ∀ m ∈ List.drop 1 p.affirmative, m ∉ List.map (fun (x : Morphology.Morph) => toForm x.form) Japanese.Negation.adjectivalEndings

The plain Japanese negative is the verb root, the negator -na- and an adjectival tense ending, where the affirmative has a verbal one: the verb becomes an adjective, less finite than the verb, which the book files, as an atypical member, under the finiteness asymmetry with a nonfinite lexical verb.

theorem Miestamo2005.japanese_asymmetric : (∃ p ∈ pairs "nucl1643", p.marker = Japanese.Negation.en ∧ Adds p) ∧ ¬ParadigmAsymmetric (pairs "nucl1643") ∧ pairsType (pairs "nucl1643") = Data.WALS.F113A.NegationSymmetry.asymmetric

The plain and the polite negatives are asymmetric, the polite past adding the copula, while the paradigm shows no asymmetry.

theorem Miestamo2005.maori_asymmetric : Formed "maor1246" ∧ pairsType (pairs "maor1246") = Data.WALS.F113A.NegationSymmetry.asymmetric

Maori negates only with the initial negative verb, after which the subject precedes the tense particle and the verb, so it is of type Asy.

theorem Miestamo2005.hixkaryana_asymmetric : Formed "hixk1239" ∧ (∀ p ∈ pairs "hixk1239", Adds p) ∧ pairsType (pairs "hixk1239") = Data.WALS.F113A.NegationSymmetry.asymmetric

Hixkaryana negates only by deverbalizing the lexical verb under an added copula, so it is of type Asy.

Mixed languages: Mandarin and Turkish

def Miestamo2005.IsSymmetricNegator (n : Mandarin.Negation.Negator) : Prop

A Mandarin negator's construction is symmetric when it adds nothing but the negator, so that no verb comes with it and no aspect particle of the affirmative is excluded.

Equations

• Miestamo2005.IsSymmetricNegator n = (n.verb = none ∧ n.excludes = [])

@[instance_reducible]

instance Miestamo2005.instDecidablePredNegatorIsSymmetricNegator : DecidablePred IsSymmetricNegator

Equations

• Miestamo2005.instDecidablePredNegatorIsSymmetricNegator n = { decide := decide (n.verb = none) && decide (n.excludes = []), reflects_decide := ⋯ }

theorem Miestamo2005.mandarin_both : IsSymmetricNegator Mandarin.Negation.bu ∧ ¬IsSymmetricNegator Mandarin.Negation.mei ∧ languageType Mandarin.Negation.negators IsSymmetricNegator False = Data.WALS.F113A.NegationSymmetry.both

Mandarin negates non-perfectives symmetrically with bù and perfectives with méi, which brings in the existential verb yǒu as the finite element of the negative clause, or is itself the negative existential verb, and loses the perfective le: a finiteness asymmetry, so the language is of type SymAsy.

theorem Miestamo2005.turkish_both : Formed "nucl1301" ∧ (∀ p ∈ pairs "nucl1301", IsSymmetric p ↔ toForm "ir" ∉ p.affirmative) ∧ ¬ParadigmAsymmetric (pairs "nucl1301") ∧ pairsType (pairs "nucl1301") = Data.WALS.F113A.NegationSymmetry.both

Turkish negation is symmetric except in the aorist, whose marker -ir changes or drops in the negative, a category asymmetry; the paradigm shows no asymmetry.

Paradigmatic neutralization: Burmese and English

theorem Miestamo2005.burmese_neutralizes : Formed "nucl1310" ∧ Neutralizes (pairs "nucl1310") ∧ pairsType (pairs "nucl1310") = Data.WALS.F113A.NegationSymmetry.asymmetric

The Burmese negative suffix replaces the postverbal tense–aspect markers, so the construction is asymmetric and one negative form corresponds to three affirmative forms.

theorem Miestamo2005.english_both : Formed "stan1293" ∧ (∀ p ∈ pairs "stan1293", ¬IsSymmetric p → Adds p) ∧ Neutralizes (pairs "stan1293") ∧ pairsType (pairs "stan1293") = Data.WALS.F113A.NegationSymmetry.both

The English negative is symmetric with the compound tenses and with the emphatic affirmatives of the simple tenses, while to the plain simple tenses it adds do; the plain and the emphatic affirmative of a simple tense share one negative, so English is of type SymAsy.

Non-realized marking: Imbabura Quechua

theorem Miestamo2005.quechua_negative_of_interrogative : IsSymmetric { marker := Quechua.Negation.mana, affirmative := List.drop 2 (forms Cole1982.Examples.ex_333), negative := List.drop 1 (forms Cole1982.Examples.ex_332) } ∧ IsSymmetric { marker := Quechua.Negation.mana, affirmative := List.map (fun (m : Form) => if m = toForm "mi" then toForm Quechua.Negation.chu.form else m) (List.drop 1 (forms Cole1982.Examples.ex_89b)), negative := forms Cole1982.Examples.ex_90 } ∧ toForm "mi" ∈ forms Cole1982.Examples.ex_89b ∧ toForm "mi" ∉ forms Cole1982.Examples.ex_90

The Imbabura Quechua negative is the polar interrogative with mana inserted, the two compared without their possessors ñuka 'my' and kan-paj 'your', (63c, d), Cole's (332) and (333). Against the declarative it has the interrogative validator -chu where the declarative has the assertive -mi, Cole's (89b) and (90), ari 'yes' set aside.