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

structure Morphology.Diagnostics.CliticAffixProfile : Type

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

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

Equations

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

@[implicit_reducible]

instance Morphology.Diagnostics.instReprCliticAffixProfile : Repr CliticAffixProfile

Equations

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

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

@[implicit_reducible]

instance Morphology.Diagnostics.instBEqCliticAffixProfile : BEq CliticAffixProfile

Equations

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

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) : Core.Morphology.MorphStatus

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 = Core.Morphology.MorphStatus.inflAffix

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

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

@cite{zwicky-pullum-1983}: Cliticization vs. Inflection

@cite{zwicky-pullum-1983}

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 Semantics.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 Phenomena.Morphology.ZwickyPullum1983.cliticS : Morphology.Diagnostics.CliticAffixProfile

Equations

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

def Phenomena.Morphology.ZwickyPullum1983.cliticVe : Morphology.Diagnostics.CliticAffixProfile

Equations

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

def Phenomena.Morphology.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 Phenomena.Morphology.ZwickyPullum1983.affixEd : Morphology.Diagnostics.CliticAffixProfile

Equations

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

def Phenomena.Morphology.ZwickyPullum1983.affixPluralS : Morphology.Diagnostics.CliticAffixProfile

Equations

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

def Phenomena.Morphology.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 Phenomena.Morphology.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 Phenomena.Morphology.ZwickyPullum1983.cliticS_is_clitic : cliticS.classify = Core.Morphology.MorphStatus.simpleClitic

theorem Phenomena.Morphology.ZwickyPullum1983.cliticVe_is_clitic : cliticVe.classify = Core.Morphology.MorphStatus.simpleClitic

theorem Phenomena.Morphology.ZwickyPullum1983.cliticD_is_clitic : cliticD.classify = Core.Morphology.MorphStatus.simpleClitic

The inflectional affixes classify as inflAffix.

theorem Phenomena.Morphology.ZwickyPullum1983.affixEd_is_affix : affixEd.classify = Core.Morphology.MorphStatus.inflAffix

theorem Phenomena.Morphology.ZwickyPullum1983.affixPluralS_is_affix : affixPluralS.classify = Core.Morphology.MorphStatus.inflAffix

theorem Phenomena.Morphology.ZwickyPullum1983.affixEst_is_affix : affixEst.classify = Core.Morphology.MorphStatus.inflAffix

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

theorem Phenomena.Morphology.ZwickyPullum1983.nt_is_affix : negNt.classify = Core.Morphology.MorphStatus.inflAffix

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

theorem Phenomena.Morphology.ZwickyPullum1983.nt_unambiguous : negNt.isUnambiguousAffix = true

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

theorem Phenomena.Morphology.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 Phenomena.Morphology.ZwickyPullum1983.may_gap : Fragments.English.Auxiliaries.may.negForm = none

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

theorem Phenomena.Morphology.ZwickyPullum1983.am_gap : Fragments.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 Phenomena.Morphology.ZwickyPullum1983.wont_irregular : Fragments.English.Auxiliaries.will.negIrregular = true

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

theorem Phenomena.Morphology.ZwickyPullum1983.cant_irregular : Fragments.English.Auxiliaries.can.negIrregular = true

can't is phonologically irregular.

theorem Phenomena.Morphology.ZwickyPullum1983.dont_irregular : Fragments.English.Auxiliaries.do_.negIrregular = true

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

theorem Phenomena.Morphology.ZwickyPullum1983.shant_irregular : Fragments.English.Auxiliaries.shall.negIrregular = true

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

theorem Phenomena.Morphology.ZwickyPullum1983.mustnt_irregular : Fragments.English.Auxiliaries.must.negIrregular = true

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

theorem Phenomena.Morphology.ZwickyPullum1983.regular_negatives : Fragments.English.Auxiliaries.could.negIrregular = false ∧ Fragments.English.Auxiliaries.would.negIrregular = false ∧ Fragments.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 boxR/diamondR from Core.Logic.Intensional: a Kripke countermodel exhibits an accessibility relation under which the two scope readings diverge.

@[reducible, inline]

abbrev Phenomena.Morphology.ZwickyPullum1983.World : Type

Equations

• Phenomena.Morphology.ZwickyPullum1983.World = Fin 4

inductive Phenomena.Morphology.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.

@[implicit_reducible]

instance Phenomena.Morphology.ZwickyPullum1983.instDecidableEqNegModalScope : DecidableEq NegModalScope

Equations

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

@[implicit_reducible]

instance Phenomena.Morphology.ZwickyPullum1983.instReprNegModalScope : Repr NegModalScope

Equations

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

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

Equations

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

structure Phenomena.Morphology.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 : Core.Modality.ModalForce

  The modal force of the auxiliary.

• scope : NegModalScope

  Which scope reading the contracted form selects.

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

Equations

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

@[implicit_reducible]

instance Phenomena.Morphology.ZwickyPullum1983.instReprContractedNegScope : Repr ContractedNegScope

Equations

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

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

Equations

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

@[implicit_reducible]

instance Phenomena.Morphology.ZwickyPullum1983.instBEqContractedNegScope : BEq ContractedNegScope

Equations

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

def Phenomena.Morphology.ZwickyPullum1983.cantScope : ContractedNegScope

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

Equations

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

def Phenomena.Morphology.ZwickyPullum1983.mustntScope : ContractedNegScope

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

Equations

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

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

The scope patterns differ — this is the semantic idiosyncrasy.

theorem Phenomena.Morphology.ZwickyPullum1983.neg_over_poss_ne_poss_over_neg : ∃ (R : Core.Logic.Intensional.AccessRel World), ¬∀ (p : World → Prop) (w : World), ¬Core.Logic.Intensional.diamondR R p w ↔ Core.Logic.Intensional.diamondR 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 Phenomena.Morphology.ZwickyPullum1983.neg_over_nec_ne_nec_over_neg : ∃ (R : Core.Logic.Intensional.AccessRel World), ¬∀ (p : World → Prop) (w : World), ¬Core.Logic.Intensional.boxR R p w ↔ Core.Logic.Intensional.boxR 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 Phenomena.Morphology.ZwickyPullum1983.aux_hosts_are_closed_class : (Fragments.English.Auxiliaries.allAuxiliaries.all fun (a : Fragments.English.Auxiliaries.AuxEntry) => a.auxType == Fragments.English.Auxiliaries.AuxType.modal || a.auxType == Fragments.English.Auxiliaries.AuxType.doSupport || a.auxType == Fragments.English.Auxiliaries.AuxType.be || a.auxType == Fragments.English.Auxiliaries.AuxType.have) = true

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

def Phenomena.Morphology.ZwickyPullum1983.ntHostCount : ℕ

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

Equations

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

def Phenomena.Morphology.ZwickyPullum1983.ntGapCount : ℕ

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

Equations

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

theorem Phenomena.Morphology.ZwickyPullum1983.nt_has_gaps : ntGapCount > 0

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

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

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