Six criteria for distinguishing clitics from inflectional affixes, formalized as a diagnostic profile. The classification (clitic vs. affix) is derived from the profile, not stipulated. ZP's surprising result: English -n't scores affix-like on all six.

Criterion	Clitic-like	Affix-like
A. Selection	low (any category)	high (specific stems)
B. Paradigm gaps	none	present
C. Morphophonological idiosyncrasies	none	present
D. Semantic idiosyncrasies	none	present
E. Syntactic rules affect combination	no	yes
F. Attaches to cliticized material	yes	no

inductive Morphology.Diagnostics.SelectionDegree : Type

How restrictive a morpheme is about what it can attach to.

[ZP83] criterion A: clitics exhibit low selection (attach to virtually any word), while affixes exhibit high selection (attach only to specific stems or categories).

• low : SelectionDegree

  Attaches to words of virtually any category (prepositions, verbs, adjectives, adverbs). Characteristic of simple clitics.

• singleCategory : SelectionDegree

  Attaches to words of a single major category (e.g., past tense -ed to verbs, plural -s to nouns). Characteristic of inflectional affixes.

• closedClass : SelectionDegree

  Attaches only to a closed list of stems (e.g., -n't only to finite auxiliaries). Maximally selective.

@[instance_reducible]

instance Morphology.Diagnostics.instDecidableEqSelectionDegree : DecidableEq SelectionDegree

Equations

• Morphology.Diagnostics.instDecidableEqSelectionDegree x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Morphology.Diagnostics.instReprSelectionDegree.repr : SelectionDegree → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Morphology.Diagnostics.instReprSelectionDegree : Repr SelectionDegree

Equations

• Morphology.Diagnostics.instReprSelectionDegree = { reprPrec := Morphology.Diagnostics.instReprSelectionDegree.repr }

def Morphology.Diagnostics.SelectionDegree.IsHighSelection (s : SelectionDegree) : Prop

Affixes are more selective than clitics.

Equations

• s.IsHighSelection = (s ≠ Morphology.Diagnostics.SelectionDegree.low)

@[instance_reducible]

instance Morphology.Diagnostics.instDecidablePredSelectionDegreeIsHighSelection : DecidablePred SelectionDegree.IsHighSelection

Equations

• Morphology.Diagnostics.instDecidablePredSelectionDegreeIsHighSelection s = id inferInstance

inductive Morphology.Diagnostics.MorphStatus : Type

Morphological status of a linguistic form: the free-word / clitic / affix cline. The clitic–affix boundary is the central question of [ZP83]; the criteria A–F serve to locate a given morpheme on this scale, and CliticAffixProfile.classify derives the classification from a criteria profile.

• freeWord : MorphStatus

  Syntactically independent word.

• simpleClitic : MorphStatus

  Simple clitic: an optional variant of a full form, occurring in the same sentence positions as that full form — English contracted auxiliaries 's, 've, 'd. ([BN07] later redefine the class by low selectivity plus phonological dependence, dropping the full-form requirement; on that rival definition, full-form-less items [ZP83] class as special clitics count as simple.)

• specialClitic : MorphStatus

  Special clitic: either no corresponding free word exists (Latin -que, English possessive 's), or the distribution differs from the free word's (Romance pronominal clitics).

• inflAffix : MorphStatus

  Inflectional affix: paradigmatic, category-preserving, highly selective, with possible gaps and idiosyncrasies. English -ed, -s, -est, -n't.

• derivAffix : MorphStatus

  Derivational affix: potentially category-changing, often productive but may show lexical restrictions. English -ness, un-, -ize.

@[instance_reducible]

instance Morphology.Diagnostics.instDecidableEqMorphStatus : DecidableEq MorphStatus

Equations

• Morphology.Diagnostics.instDecidableEqMorphStatus x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Morphology.Diagnostics.instReprMorphStatus.repr : MorphStatus → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Morphology.Diagnostics.instReprMorphStatus : Repr MorphStatus

Equations

• Morphology.Diagnostics.instReprMorphStatus = { reprPrec := Morphology.Diagnostics.instReprMorphStatus.repr }

def Morphology.Diagnostics.MorphStatus.IsAffix (s : MorphStatus) : Prop

Is this an affix (inflectional or derivational)?

Equations

• s.IsAffix = (s = Morphology.Diagnostics.MorphStatus.inflAffix ∨ s = Morphology.Diagnostics.MorphStatus.derivAffix)

@[instance_reducible]

instance Morphology.Diagnostics.instDecidablePredMorphStatusIsAffix : DecidablePred MorphStatus.IsAffix

Equations

• Morphology.Diagnostics.instDecidablePredMorphStatusIsAffix x✝ = Morphology.Diagnostics.instDecidablePredMorphStatusIsAffix._aux_1 x✝

def Morphology.Diagnostics.MorphStatus.IsClitic (s : MorphStatus) : Prop

Is this a clitic (simple or special)?

Equations

• s.IsClitic = (s = Morphology.Diagnostics.MorphStatus.simpleClitic ∨ s = Morphology.Diagnostics.MorphStatus.specialClitic)

@[instance_reducible]

instance Morphology.Diagnostics.instDecidablePredMorphStatusIsClitic : DecidablePred MorphStatus.IsClitic

Equations

• Morphology.Diagnostics.instDecidablePredMorphStatusIsClitic x✝ = Morphology.Diagnostics.instDecidablePredMorphStatusIsClitic._aux_1 x✝

structure Morphology.Diagnostics.CliticAffixProfile : Type

• morpheme : String
• selection : SelectionDegree
• hasArbitraryGaps : Bool
• hasMorphophonIdiosyncrasies : Bool
• hasSemanticIdiosyncrasies : Bool
• syntacticRulesApply : Bool
• attachesToCliticizedMaterial : Bool

@[instance_reducible]

instance Morphology.Diagnostics.instReprCliticAffixProfile : Repr CliticAffixProfile

Equations

• Morphology.Diagnostics.instReprCliticAffixProfile = { reprPrec := Morphology.Diagnostics.instReprCliticAffixProfile.repr }

def Morphology.Diagnostics.instReprCliticAffixProfile.repr : CliticAffixProfile → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Morphology.Diagnostics.instBEqCliticAffixProfile : BEq CliticAffixProfile

Equations

• Morphology.Diagnostics.instBEqCliticAffixProfile = { beq := Morphology.Diagnostics.instBEqCliticAffixProfile.beq }

def Morphology.Diagnostics.instBEqCliticAffixProfile.beq : CliticAffixProfile → CliticAffixProfile → Bool

Equations

• One or more equations did not get rendered due to their size.
• Morphology.Diagnostics.instBEqCliticAffixProfile.beq x✝¹ x✝ = false

def Morphology.Diagnostics.CliticAffixProfile.affixLikeSelection (p : CliticAffixProfile) : Bool

Equations

• p.affixLikeSelection = decide p.selection.IsHighSelection

def Morphology.Diagnostics.CliticAffixProfile.affixScore (p : CliticAffixProfile) : ℕ

Equations

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

def Morphology.Diagnostics.CliticAffixProfile.cliticScore (p : CliticAffixProfile) : ℕ

Equations

• p.cliticScore = 6 - p.affixScore

def Morphology.Diagnostics.CliticAffixProfile.classify (p : CliticAffixProfile) : MorphStatus

Classification from a criteria profile. The two unanimous poles are the paper's: all six affix-like is an inflectional affix, all six clitic-like a simple clitic. The middle branch is a conservative default beyond the paper — [ZP83] define special clitics distributionally (their §5), not as an intermediate criteria score.

Equations

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

def Morphology.Diagnostics.CliticAffixProfile.isUnambiguousAffix (p : CliticAffixProfile) : Bool

Equations

• p.isUnambiguousAffix = (p.affixScore == 6)

def Morphology.Diagnostics.CliticAffixProfile.isUnambiguousClitic (p : CliticAffixProfile) : Bool

Equations

• p.isUnambiguousClitic = (p.cliticScore == 6)

theorem Morphology.Diagnostics.classify_all_affix (p : CliticAffixProfile) (h : p.affixScore = 6) : p.classify = MorphStatus.inflAffix

theorem Morphology.Diagnostics.classify_all_clitic (p : CliticAffixProfile) (h : p.affixScore = 0) : p.classify = MorphStatus.simpleClitic

theorem Morphology.Diagnostics.classify_total (p : CliticAffixProfile) : p.classify = MorphStatus.inflAffix ∨ p.classify = MorphStatus.simpleClitic ∨ p.classify = MorphStatus.specialClitic

[ZP83]: Cliticization vs. Inflection

[ZP83]

Empirical data and classification theorems for the argument that English contracted negator -n't is an inflectional affix, not a simple clitic.

Core argument

Six diagnostics (A–F) separate clitics from inflectional affixes. English simple clitics ('s, 've, 'd) score clitic-like on all six. English inflectional affixes (-ed, -s, -est) score affix-like on all six. The contracted negator -n't scores affix-like on all six — a surprising result given the near-universal prior assumption that it is a clitic.

Semantic scope bridge (criterion D)

The scope irregularity of negation with modals provides a bridge to Modality: can't means NOT(CAN(P)) but mustn't means MUST(NOT(P)). This non-compositional scope behavior is characteristic of inflectional affixes, not clitics.

Simple clitics: 's (has/is), 've, 'd

Z&P §2 (criteria A–D) and §3 (criteria E–F):

• A. Low selection: attach to prepositions, verbs, adjectives, adverbs
• B. No arbitrary gaps: combine with any phonologically suitable host
• C. No morphophonological idiosyncrasies: regular reduction
• D. No semantic idiosyncrasies: meaning identical to full form
• E. No syntactic rules affect the combination (no SAI on clitic groups)
• F. Can attach to material already containing clitics (I'd've)

def ZwickyPullum1983.cliticS : Morphology.Diagnostics.CliticAffixProfile

Equations

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

def ZwickyPullum1983.cliticVe : Morphology.Diagnostics.CliticAffixProfile

Equations

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

def ZwickyPullum1983.cliticD : Morphology.Diagnostics.CliticAffixProfile

Equations

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

Inflectional affixes: -ed (past), -s (plural), -est (superlative)

Z&P §2 (criteria A–D) and §3 (criteria E–F):

• A. High selection: each attaches to a single major category
• B. Arbitrary gaps: *strided, *goed
• C. Morphophonological idiosyncrasies: slept, went, best
• D. Semantic idiosyncrasies: last (superlative of late, but not "most recent" — rather "final")
• E. Syntactic rules affect affixed words (inflected nouns, verbs, adjectives are regular syntactic units)
• F. Cannot attach to cliticized material

def ZwickyPullum1983.affixEd : Morphology.Diagnostics.CliticAffixProfile

Equations

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

def ZwickyPullum1983.affixPluralS : Morphology.Diagnostics.CliticAffixProfile

Equations

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

def ZwickyPullum1983.affixEst : Morphology.Diagnostics.CliticAffixProfile

Equations

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

The contracted negator -n't

Z&P §4 (the core of the paper):

• A. High selection (closedClass): attaches only to finite auxiliaries (not to main verbs, prepositions, adjectives, adverbs)
• B. Arbitrary gaps: *mayn't, *amn't (Table 1)
• C. Morphophonological idiosyncrasies: won't [wont] ← will, can't [kænt] ← can, don't [dont] ← do, shan't ← shall
• D. Semantic idiosyncrasies: mustn't = MUST(NOT(P)), not NOT(MUST(P)); can't = NOT(CAN(P)), not CAN(NOT(P)). Scope of negation varies.
• E. SAI applies to -n't forms: Isn't he?, Can't you?, Haven't they?. Contracted negator moves with auxiliary under T-to-C.
• F. Cannot attach to cliticized material: *I'd'ven't (cf. I'd've)

def ZwickyPullum1983.negNt : Morphology.Diagnostics.CliticAffixProfile

Equations

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

The simple clitics classify as simpleClitic.

theorem ZwickyPullum1983.cliticS_is_clitic : cliticS.classify = Morphology.Diagnostics.MorphStatus.simpleClitic

theorem ZwickyPullum1983.cliticVe_is_clitic : cliticVe.classify = Morphology.Diagnostics.MorphStatus.simpleClitic

theorem ZwickyPullum1983.cliticD_is_clitic : cliticD.classify = Morphology.Diagnostics.MorphStatus.simpleClitic

The inflectional affixes classify as inflAffix.

theorem ZwickyPullum1983.affixEd_is_affix : affixEd.classify = Morphology.Diagnostics.MorphStatus.inflAffix

theorem ZwickyPullum1983.affixPluralS_is_affix : affixPluralS.classify = Morphology.Diagnostics.MorphStatus.inflAffix

theorem ZwickyPullum1983.affixEst_is_affix : affixEst.classify = Morphology.Diagnostics.MorphStatus.inflAffix

The main result: -n't classifies as inflAffix, not simpleClitic.

theorem ZwickyPullum1983.nt_is_affix : negNt.classify = Morphology.Diagnostics.MorphStatus.inflAffix

-n't scores 6/6 affix-like — unambiguous.

theorem ZwickyPullum1983.nt_unambiguous : negNt.isUnambiguousAffix = true

The simple clitics score 0/6 affix-like — unambiguous.

theorem ZwickyPullum1983.clitics_unambiguous : cliticS.isUnambiguousClitic = true ∧ cliticVe.isUnambiguousClitic = true ∧ cliticD.isUnambiguousClitic = true

Verify that the paradigm gaps in Table 1 are encoded in the Fragment data.

theorem ZwickyPullum1983.may_gap : English.Auxiliaries.may.negForm = none

may has no contracted negative form (*mayn't is a paradigm gap).

theorem ZwickyPullum1983.am_gap : English.Auxiliaries.am.negForm = none

am has no contracted negative form (*amn't is a paradigm gap).

Verify that the phonologically irregular forms are flagged in Fragment data.

theorem ZwickyPullum1983.wont_irregular : English.Auxiliaries.will.negIrregular = true

won't is phonologically irregular (not willn't).

theorem ZwickyPullum1983.cant_irregular : English.Auxiliaries.can.negIrregular = true

can't is phonologically irregular.

theorem ZwickyPullum1983.dont_irregular : English.Auxiliaries.do_.negIrregular = true

don't is phonologically irregular (not don't [dunt]).

theorem ZwickyPullum1983.shant_irregular : English.Auxiliaries.shall.negIrregular = true

shan't is phonologically irregular (not shalln't).

theorem ZwickyPullum1983.mustnt_irregular : English.Auxiliaries.must.negIrregular = true

mustn't shows [t]-deletion: [mʌsnt] not *[mʌstnt].

theorem ZwickyPullum1983.regular_negatives : English.Auxiliaries.could.negIrregular = false ∧ English.Auxiliaries.would.negIrregular = false ∧ English.Auxiliaries.should.negIrregular = false

Regular forms: couldn't, wouldn't, shouldn't show no irregularity.

Scope of negation with contracted modals

Z&P observe that can't and mustn't show opposite scope relations:

• You can't go home = NOT(CAN(P)): negation scopes over possibility
• You mustn't go home = MUST(NOT(P)): necessity scopes over negation

This is an irregularity in the connection between the contracted form and its uncontracted paraphrase. For can, You cannot go home = You can not go home = NOT(CAN(P)). But for must, You must not go home is ambiguous — it can mean MUST(NOT(P)) (the reading that mustn't unambiguously selects).

This scope irregularity is predicted by the inflectional-affix analysis: if -n't is an affix, it forms a lexical unit with the auxiliary, and lexical items can have idiosyncratic scope properties. If -n't were a clitic (a reduced form of not), its scope should always match not.

We formalize this using box/diamond from Intensional: a Kripke countermodel exhibits an accessibility relation under which the two scope readings diverge.

@[reducible, inline]

abbrev ZwickyPullum1983.World : Type

Equations

• ZwickyPullum1983.World = Fin 4

inductive ZwickyPullum1983.NegModalScope : Type

Scope of negation relative to a modal operator.

• negOverModal : NegModalScope

  Negation scopes over the modal: NOT(MODAL(P)). You can't go = it's not the case that you can go.

• modalOverNeg : NegModalScope

  Modal scopes over negation: MODAL(NOT(P)). You mustn't go = you must not go.

@[instance_reducible]

instance ZwickyPullum1983.instDecidableEqNegModalScope : DecidableEq NegModalScope

Equations

• ZwickyPullum1983.instDecidableEqNegModalScope x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def ZwickyPullum1983.instReprNegModalScope.repr : NegModalScope → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance ZwickyPullum1983.instReprNegModalScope : Repr NegModalScope

Equations

• ZwickyPullum1983.instReprNegModalScope = { reprPrec := ZwickyPullum1983.instReprNegModalScope.repr }

structure ZwickyPullum1983.ContractedNegScope : Type

The scope pattern for a contracted negative auxiliary.

can't: NOT(CAN(P)) — negOverModal with possibility mustn't: MUST(NOT(P)) — modalOverNeg with necessity

That these differ is the semantic idiosyncrasy. If -n't were simply a reduced form of not, both should have the same scope relation.

• auxiliary : String

  The base auxiliary form.

• force : Modality.ModalForce

  The modal force of the auxiliary.

• scope : NegModalScope

  Which scope reading the contracted form selects.

def ZwickyPullum1983.instReprContractedNegScope.repr : ContractedNegScope → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance ZwickyPullum1983.instReprContractedNegScope : Repr ContractedNegScope

Equations

• ZwickyPullum1983.instReprContractedNegScope = { reprPrec := ZwickyPullum1983.instReprContractedNegScope.repr }

@[instance_reducible]

instance ZwickyPullum1983.instBEqContractedNegScope : BEq ContractedNegScope

Equations

• ZwickyPullum1983.instBEqContractedNegScope = { beq := ZwickyPullum1983.instBEqContractedNegScope.beq }

def ZwickyPullum1983.instBEqContractedNegScope.beq : ContractedNegScope → ContractedNegScope → Bool

Equations

• ZwickyPullum1983.instBEqContractedNegScope.beq { auxiliary := a, force := a_1, scope := a_2 } { auxiliary := b, force := b_1, scope := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• ZwickyPullum1983.instBEqContractedNegScope.beq x✝¹ x✝ = false

def ZwickyPullum1983.cantScope : ContractedNegScope

can't selects NOT(CAN(P)): negation over possibility.

Equations

• ZwickyPullum1983.cantScope = { auxiliary := "can", force := Modality.ModalForce.possibility, scope := ZwickyPullum1983.NegModalScope.negOverModal }

def ZwickyPullum1983.mustntScope : ContractedNegScope

mustn't selects MUST(NOT(P)): necessity over negation.

Equations

• ZwickyPullum1983.mustntScope = { auxiliary := "must", force := Modality.ModalForce.necessity, scope := ZwickyPullum1983.NegModalScope.modalOverNeg }

theorem ZwickyPullum1983.scope_idiosyncrasy : cantScope.scope ≠ mustntScope.scope

The scope patterns differ — this is the semantic idiosyncrasy.

theorem ZwickyPullum1983.neg_over_poss_ne_poss_over_neg : ∃ (R : World → World → Prop), ¬∀ (p : World → Prop) (w : World), ¬ModalLogic.diamond R p w ↔ ModalLogic.diamond R (fun (w' : World) => ¬p w') w

NOT(CAN(P)) and CAN(NOT(P)) are not equivalent in general.

There exists a Kripke accessibility relation where ¬◇P ≠ ◇¬P: when w0 accesses worlds where P differs, ◇P and ◇¬P are both true, so ¬◇P = false but ◇¬P = true.

theorem ZwickyPullum1983.neg_over_nec_ne_nec_over_neg : ∃ (R : World → World → Prop), ¬∀ (p : World → Prop) (w : World), ¬ModalLogic.box R p w ↔ ModalLogic.box R (fun (w' : World) => ¬p w') w

NOT(MUST(P)) and MUST(NOT(P)) are not equivalent in general.

There exists a Kripke accessibility relation where ¬□P ≠ □¬P: failing to be necessary (¬□P = true when P fails at w2) is weaker than being necessarily false (□¬P = false when P holds at w1).

-n't attaches only to finite auxiliaries. Verify that the host set matches the auxiliary inventory from Fragments/English/FunctionWords.

theorem ZwickyPullum1983.aux_hosts_are_closed_class : (English.Auxiliaries.allAuxiliaries.all fun (a : English.Auxiliaries.AuxEntry) => a.auxType == English.Auxiliaries.AuxType.modal || a.auxType == English.Auxiliaries.AuxType.doSupport || a.auxType == English.Auxiliaries.AuxType.be || a.auxType == English.Auxiliaries.AuxType.have) = true

Every auxiliary in the inventory is either a modal, do-support, be, or have.

def ZwickyPullum1983.ntHostCount : ℕ

The number of auxiliaries with contracted negative forms (= the productive range of -n't).

Equations

• ZwickyPullum1983.ntHostCount = (List.filter (fun (a : English.Auxiliaries.AuxEntry) => a.negForm.isSome) English.Auxiliaries.allAuxiliaries).length

def ZwickyPullum1983.ntGapCount : ℕ

The number of paradigm gaps (auxiliaries without -n't).

Equations

• ZwickyPullum1983.ntGapCount = (List.filter (fun (a : English.Auxiliaries.AuxEntry) => a.negForm.isNone) English.Auxiliaries.allAuxiliaries).length

theorem ZwickyPullum1983.nt_has_gaps : ntGapCount > 0

Most auxiliaries have a contracted negative form, but there are gaps.

theorem ZwickyPullum1983.nt_has_irregulars : (List.filter (fun (a : English.Auxiliaries.AuxEntry) => a.negIrregular) English.Auxiliaries.allAuxiliaries).length ≥ 5

At least five auxiliaries show phonological irregularity in their contracted negative form (Z&P criterion C).