Presuppositional Semantics of Phi-Features

@cite{sauerland-2003} @cite{sauerland-2008b} @cite{harbour-2016} @cite{heim-1991} @cite{wang-r-2023}

Phi-features (number, person, definiteness) are presuppositional partial identity functions on the entity domain, ordered by presuppositional strength via Features.PrivativePair.specLevel.

The core mathematical object is phiPresup: a single function that maps each PrivativePair cell to a PrProp, using two predicates (innerP, outerP) corresponding to the inner and outer privative features. Since the three well-formed cells have 2, 1, and 0 marked features respectively, their presuppositions are automatically nested — more marked features = stronger presupposition = smaller domain.

Domains

Domain	innerP	outerP	maximal (2)	intermediate (1)	minimal (0)
Number	Atom	MinimalGroup	singular	dual	plural
Person	speaker ≤ ·	speaker ≤ · ∨ addressee ≤ ·	1st	2nd	3rd
Gender	isInanimate	isFemale	neuter	feminine	masculine
Definiteness	familiar/unique	—	definite	—	indefinite

Semantic Markedness (@cite{wang-r-2023})

The semantically unmarked values (plural, 3rd person, indefinite) are precisely those at the minimal cell (specLevel 0) with vacuous presuppositions. These are the values recruited cross-linguistically for honorification — an observation that falls out from the presuppositional framework without stipulation.

Architecture

This file was extracted from Sauerland2003 to separate general phi-feature presuppositional theory (which belongs in Theories/) from Sauerland's specific arguments about number (which belong in Phenomena/Plurals/Studies/).

def Semantics.Presupposition.PhiFeatures.phiPresup {E : Type u_1} (innerP outerP : E → Prop) : Features.PrivativePair → Core.Presupposition.PrProp E

Generic presuppositional denotation from a privative feature pair.

Maps each PrivativePair cell to a PrProp using two predicates: innerP for [±inner] and outerP for [±outer].

Cell	outer	inner	Presupposition
maximal	+	+	innerP
intermediate	+	−	outerP
minimal	−	−	vacuous

Since [+inner] → [+outer] (privative containment), innerP implies outerP. So maximal's presupposition (innerP) is the strongest — no need to separately conjoin outerP.

Equations

• Semantics.Presupposition.PhiFeatures.phiPresup innerP outerP { outer := true, inner := true } = { presup := innerP, assertion := fun (x : E) => True }
• Semantics.Presupposition.PhiFeatures.phiPresup innerP outerP { outer := true, inner := false } = { presup := outerP, assertion := fun (x : E) => True }
• Semantics.Presupposition.PhiFeatures.phiPresup innerP outerP { outer := false, inner := inner } = { presup := fun (x : E) => True, assertion := fun (x : E) => True }

theorem Semantics.Presupposition.PhiFeatures.phiPresup_nesting {E : Type u_1} {innerP outerP : E → Prop} (hContain : ∀ (x : E), innerP x → outerP x) {c₁ c₂ : Features.PrivativePair} (hw₁ : c₁.wellFormed = true) (hw₂ : c₂.wellFormed = true) (hSpec : c₁.specLevel ≥ c₂.specLevel) (x : E) (h : Core.Presupposition.PrProp.defined x (phiPresup innerP outerP c₁)) : Core.Presupposition.PrProp.defined x (phiPresup innerP outerP c₂)

Feature-Subset Principle, derived from privative geometry.

If innerP → outerP (the containment [+inner] → [+outer]), then more specified cells have smaller presuppositional domains. This is the semantic content of PrivativePair.spec_strict_order — not a stipulation but a consequence of the algebraic structure.

theorem Semantics.Presupposition.PhiFeatures.phiPresup_same_assertion {E : Type u_1} (innerP outerP : E → Prop) (c₁ c₂ : Features.PrivativePair) (x : E) : (phiPresup innerP outerP c₁).assertion x ↔ (phiPresup innerP outerP c₂).assertion x

All phiPresup cells have the same (trivial) assertive content. This is the privative-geometric reason why φ-feature competition is presuppositional, not at-issue.

def Semantics.Presupposition.PhiFeatures.sgSem (E : Type u_1) [PartialOrder E] : Core.Presupposition.PrProp E

⟦Sg⟧: presupposes atomicity. The identity function restricted to atoms — defined only when the referent is an atom.

Equations

• Semantics.Presupposition.PhiFeatures.sgSem E = { presup := Mereology.Atom, assertion := fun (x : E) => True }

def Semantics.Presupposition.PhiFeatures.plSem (E : Type u_1) : Core.Presupposition.PrProp E

⟦Pl⟧: no inherent presupposition. The unrestricted identity function. Its distribution is constrained pragmatically by Maximize Presupposition, not by any semantic content.

Equations

• Semantics.Presupposition.PhiFeatures.plSem E = { presup := fun (x : E) => True, assertion := fun (x : E) => True }

def Semantics.Presupposition.PhiFeatures.dualSem {E : Type u_1} (minimalP : E → Prop) : Core.Presupposition.PrProp E

⟦Du⟧: presupposes minimality (no proper non-atomic subpart). The intermediate cell (specLevel 1).

Equations

• Semantics.Presupposition.PhiFeatures.dualSem minimalP = { presup := minimalP, assertion := fun (x : E) => True }

@[simp]

theorem Semantics.Presupposition.PhiFeatures.sgSem_eq_phiPresup {E : Type u_1} [PartialOrder E] (outerP : E → Prop) : phiPresup Mereology.Atom outerP Features.PrivativePair.maximal = sgSem E

sgSem is phiPresup at the maximal cell.

@[simp]

theorem Semantics.Presupposition.PhiFeatures.dualSem_eq_phiPresup {E : Type u_1} [PartialOrder E] (minimalP : E → Prop) : phiPresup Mereology.Atom minimalP Features.PrivativePair.intermediate = dualSem minimalP

dualSem is phiPresup at the intermediate cell.

@[simp]

theorem Semantics.Presupposition.PhiFeatures.plSem_eq_phiPresup {E : Type u_1} (innerP outerP : E → Prop) : phiPresup innerP outerP Features.PrivativePair.minimal = plSem E

plSem is phiPresup at the minimal cell.

@[simp]

theorem Semantics.Presupposition.PhiFeatures.sg_is_maximal_cell : Features.PhiFeatures.toPair Features.Number.singularF = Features.PrivativePair.maximal

Singular features map to the maximal PrivativePair cell (specLevel 2).

@[simp]

theorem Semantics.Presupposition.PhiFeatures.pl_is_minimal_cell : Features.PhiFeatures.toPair Features.Number.pluralF = Features.PrivativePair.minimal

Plural features map to the minimal cell (specLevel 0).

theorem Semantics.Presupposition.PhiFeatures.presup_strength_tracks_specLevel : Features.PhiFeatures.specLevel Features.Number.singularF > Features.PhiFeatures.specLevel Features.Number.pluralF

The presuppositional asymmetry tracks specification level: singular (specLevel 2) has content; plural (specLevel 0) is vacuous.

def Semantics.Presupposition.PhiFeatures.firstSem {E : Type u_1} [PartialOrder E] (speaker : E) : Core.Presupposition.PrProp E

⟦1st⟧: presupposes the referent includes the speaker. Maximal cell [+author, +participant] (specLevel 2).

Equations

• Semantics.Presupposition.PhiFeatures.firstSem speaker = { presup := fun (x : E) => speaker ≤ x, assertion := fun (x : E) => True }

def Semantics.Presupposition.PhiFeatures.secondSem {E : Type u_1} [PartialOrder E] (speaker addressee : E) : Core.Presupposition.PrProp E

⟦2nd⟧: presupposes the referent includes a speech-act participant. Intermediate cell [−author, +participant] (specLevel 1).

Equations

• Semantics.Presupposition.PhiFeatures.secondSem speaker addressee = { presup := fun (x : E) => speaker ≤ x ∨ addressee ≤ x, assertion := fun (x : E) => True }

def Semantics.Presupposition.PhiFeatures.thirdSem {E : Type u_1} : Core.Presupposition.PrProp E

⟦3rd⟧: vacuous presupposition. Minimal cell [−author, −participant] (specLevel 0).

Equations

• Semantics.Presupposition.PhiFeatures.thirdSem = { presup := fun (x : E) => True, assertion := fun (x : E) => True }

theorem Semantics.Presupposition.PhiFeatures.person_domain_nesting {E : Type u_1} [PartialOrder E] (speaker addressee : E) : (∀ (x : E), Core.Presupposition.PrProp.defined x (firstSem speaker) → Core.Presupposition.PrProp.defined x (secondSem speaker addressee)) ∧ ∀ (x : E), Core.Presupposition.PrProp.defined x (secondSem speaker addressee) → Core.Presupposition.PrProp.defined x thirdSem

Person domain nesting: dom(1st) ⊆ dom(2nd) ⊆ dom(3rd).

theorem Semantics.Presupposition.PhiFeatures.firstSem_eq_phiPresup {E : Type u_1} [PartialOrder E] (speaker addressee : E) : phiPresup (fun (x : E) => speaker ≤ x) (fun (x : E) => speaker ≤ x ∨ addressee ≤ x) Features.PrivativePair.maximal = firstSem speaker

theorem Semantics.Presupposition.PhiFeatures.secondSem_eq_phiPresup {E : Type u_1} [PartialOrder E] (speaker addressee : E) : phiPresup (fun (x : E) => speaker ≤ x) (fun (x : E) => speaker ≤ x ∨ addressee ≤ x) Features.PrivativePair.intermediate = secondSem speaker addressee

theorem Semantics.Presupposition.PhiFeatures.thirdSem_eq_phiPresup {E : Type u_1} [PartialOrder E] (speaker addressee : E) : phiPresup (fun (x : E) => speaker ≤ x) (fun (x : E) => speaker ≤ x ∨ addressee ≤ x) Features.PrivativePair.minimal = thirdSem

theorem Semantics.Presupposition.PhiFeatures.person_nesting_from_phi {E : Type u_1} [PartialOrder E] (speaker addressee : E) {c₁ c₂ : Features.PrivativePair} (hw₁ : c₁.wellFormed = true) (hw₂ : c₂.wellFormed = true) (hSpec : c₁.specLevel ≥ c₂.specLevel) (x : E) (h : Core.Presupposition.PrProp.defined x (phiPresup (fun (x : E) => speaker ≤ x) (fun (x : E) => speaker ≤ x ∨ addressee ≤ x) c₁)) : Core.Presupposition.PrProp.defined x (phiPresup (fun (x : E) => speaker ≤ x) (fun (x : E) => speaker ≤ x ∨ addressee ≤ x) c₂)

Person nesting is a corollary of phiPresup_nesting — the same theorem that derives number nesting also derives person nesting, because both use the same PrivativePair structure.

theorem Semantics.Presupposition.PhiFeatures.person_number_isomorphism : Features.PhiFeatures.specLevel Features.Person.first = Features.PhiFeatures.specLevel Features.Number.singularF ∧ Features.PhiFeatures.specLevel Features.Person.second = Features.PhiFeatures.specLevel Features.Number.dualF ∧ Features.PhiFeatures.specLevel Features.Person.third = Features.PhiFeatures.specLevel Features.Number.pluralF

Person and number have the same specLevel ordering — this is the semantic content of @cite{harbour-2016}'s phi kernel isomorphism. Both are phiPresup instances over the same PrivativePair cells, so phiPresup_nesting applies to both: the nesting is structural, not a per-domain coincidence.

§3b: Gender Presuppositions (@cite{sauerland-2003} §6)

Gender features [±feminine, ±neuter] form a third PrivativePair instance, with containment [+neuter] → [+feminine] (see Features.Gender.Features).

The presuppositional semantics mirrors number and person:

• neuter (maximal, specLevel 2): presupposes inanimate
• feminine (intermediate, specLevel 1): presupposes female
• masculine (minimal, specLevel 0): vacuous (default/unmarked)

@cite{wang-r-2023}: masculine, as the semantically unmarked gender, is available for honorific use cross-linguistically — paralleling the use of plural (unmarked number) and 3rd person (unmarked person) for politeness.

def Semantics.Presupposition.PhiFeatures.neutSem {E : Type u_1} (isInanimate : E → Prop) : Core.Presupposition.PrProp E

⟦Neut⟧: presupposes the referent is inanimate. Maximal cell [+feminine, +neuter] (specLevel 2).

Equations

• Semantics.Presupposition.PhiFeatures.neutSem isInanimate = { presup := isInanimate, assertion := fun (x : E) => True }

def Semantics.Presupposition.PhiFeatures.femSem {E : Type u_1} (isFemale : E → Prop) : Core.Presupposition.PrProp E

⟦Fem⟧: presupposes the referent is female. Intermediate cell [+feminine, −neuter] (specLevel 1).

Equations

• Semantics.Presupposition.PhiFeatures.femSem isFemale = { presup := isFemale, assertion := fun (x : E) => True }

def Semantics.Presupposition.PhiFeatures.mascSem {E : Type u_1} : Core.Presupposition.PrProp E

⟦Masc⟧: vacuous presupposition. Minimal cell [−feminine, −neuter] (specLevel 0).

Equations

• Semantics.Presupposition.PhiFeatures.mascSem = { presup := fun (x : E) => True, assertion := fun (x : E) => True }

@[simp]

theorem Semantics.Presupposition.PhiFeatures.neutSem_eq_phiPresup {E : Type u_1} (isInanimate isFemale : E → Prop) : phiPresup isInanimate isFemale Features.PrivativePair.maximal = neutSem isInanimate

neutSem is phiPresup at the maximal cell.

@[simp]

theorem Semantics.Presupposition.PhiFeatures.femSem_eq_phiPresup {E : Type u_1} (isInanimate isFemale : E → Prop) : phiPresup isInanimate isFemale Features.PrivativePair.intermediate = femSem isFemale

femSem is phiPresup at the intermediate cell.

@[simp]

theorem Semantics.Presupposition.PhiFeatures.mascSem_eq_phiPresup {E : Type u_1} (innerP outerP : E → Prop) : phiPresup innerP outerP Features.PrivativePair.minimal = mascSem

mascSem is phiPresup at the minimal cell.

@[simp]

theorem Semantics.Presupposition.PhiFeatures.neut_is_maximal_cell : Features.PhiFeatures.toPair Features.Gender.neuterF = Features.PrivativePair.maximal

Neuter features map to the maximal PrivativePair cell (specLevel 2).

@[simp]

theorem Semantics.Presupposition.PhiFeatures.fem_is_intermediate_cell : Features.PhiFeatures.toPair Features.Gender.feminineF = Features.PrivativePair.intermediate

Feminine features map to the intermediate cell (specLevel 1).

@[simp]

theorem Semantics.Presupposition.PhiFeatures.masc_is_minimal_cell : Features.PhiFeatures.toPair Features.Gender.masculineF = Features.PrivativePair.minimal

Masculine features map to the minimal cell (specLevel 0).

theorem Semantics.Presupposition.PhiFeatures.gender_domain_nesting {E : Type u_1} (isInanimate isFemale : E → Prop) (hContain : ∀ (x : E), isInanimate x → isFemale x) : (∀ (x : E), Core.Presupposition.PrProp.defined x (neutSem isInanimate) → Core.Presupposition.PrProp.defined x (femSem isFemale)) ∧ ∀ (x : E), Core.Presupposition.PrProp.defined x (femSem isFemale) → Core.Presupposition.PrProp.defined x mascSem

Gender domain nesting: dom(Neut) ⊆ dom(Fem) ⊆ dom(Masc). Parallels number (sg ⊆ pl) and person (1st ⊆ 3rd).

theorem Semantics.Presupposition.PhiFeatures.gender_nesting_from_phi {E : Type u_1} (isInanimate isFemale : E → Prop) (hContain : ∀ (x : E), isInanimate x → isFemale x) {c₁ c₂ : Features.PrivativePair} (hw₁ : c₁.wellFormed = true) (hw₂ : c₂.wellFormed = true) (hSpec : c₁.specLevel ≥ c₂.specLevel) (x : E) (h : Core.Presupposition.PrProp.defined x (phiPresup isInanimate isFemale c₁)) : Core.Presupposition.PrProp.defined x (phiPresup isInanimate isFemale c₂)

Gender nesting via phiPresup_nesting — structurally identical to person nesting and number nesting.

theorem Semantics.Presupposition.PhiFeatures.gender_person_number_isomorphism : Features.PhiFeatures.specLevel Features.Gender.neuterF = Features.PhiFeatures.specLevel Features.Person.first ∧ Features.PhiFeatures.specLevel Features.Gender.neuterF = Features.PhiFeatures.specLevel Features.Number.singularF ∧ Features.PhiFeatures.specLevel Features.Gender.feminineF = Features.PhiFeatures.specLevel Features.Person.second ∧ Features.PhiFeatures.specLevel Features.Gender.masculineF = Features.PhiFeatures.specLevel Features.Person.third

Gender, person, and number have the same specLevel ordering — all three domains share the phi kernel structure.

§4: Definiteness as Presupposition

Definiteness exhibits the same presuppositional asymmetry as number and person: definites carry a familiarity/uniqueness presupposition (@cite{heim-1991}, @cite{strawson-1950}), while indefinites carry no presupposition. Unlike number and person, definiteness is a binary contrast (no intermediate cell), so we instantiate phiPresup at the maximal and minimal cells only.

@cite{wang-r-2023} relies on this: indefinites are semantically unmarked (vacuous presupposition), so they are recruited for honorification in languages like Ainu.

def Semantics.Presupposition.PhiFeatures.defSem {E : Type u_1} (familiar : E → Prop) : Core.Presupposition.PrProp E

⟦DEF⟧: presupposes the referent satisfies a contextual familiarity or uniqueness condition. The predicate familiar is abstract — concretely it may be Heim's familiarity or Russell's uniqueness (cf. Features.Definiteness.DefPresupType).

Equations

• Semantics.Presupposition.PhiFeatures.defSem familiar = { presup := familiar, assertion := fun (x : E) => True }

def Semantics.Presupposition.PhiFeatures.indefSem {E : Type u_1} : Core.Presupposition.PrProp E

⟦INDEF⟧: no presupposition. Like plSem and thirdSem, its distribution is constrained pragmatically by Maximize Presupposition. Using an indefinite when a definite's presupposition is satisfied would violate MP!.

Equations

• Semantics.Presupposition.PhiFeatures.indefSem = { presup := fun (x : E) => True, assertion := fun (x : E) => True }

@[simp]

theorem Semantics.Presupposition.PhiFeatures.defSem_eq_phiPresup {E : Type u_1} (familiar : E → Prop) : phiPresup familiar familiar Features.PrivativePair.maximal = defSem familiar

defSem is phiPresup at the maximal cell (with outerP = familiar).

@[simp]

theorem Semantics.Presupposition.PhiFeatures.indefSem_eq_phiPresup {E : Type u_1} (innerP outerP : E → Prop) : phiPresup innerP outerP Features.PrivativePair.minimal = indefSem

indefSem is phiPresup at the minimal cell.

theorem Semantics.Presupposition.PhiFeatures.def_domain_subset_indef {E : Type u_1} (familiar : E → Prop) (x : E) : Core.Presupposition.PrProp.defined x (defSem familiar) → Core.Presupposition.PrProp.defined x indefSem

Definiteness domain nesting: dom(DEF) ⊆ dom(INDEF).

theorem Semantics.Presupposition.PhiFeatures.def_strictly_stronger {E : Type u_1} (familiar : E → Prop) (x : E) (hUnfamiliar : ¬familiar x) : Core.Presupposition.PrProp.defined x indefSem ∧ ¬Core.Presupposition.PrProp.defined x (defSem familiar)

The containment is strict: there exist unfamiliar entities in dom(INDEF) \ dom(DEF).

§5: Semantic Markedness (@cite{wang-r-2023})

A phi-feature value is semantically unmarked iff its presupposition is vacuous — i.e., it is at the minimal PrivativePair cell (specLevel 0). Semantically unmarked values are compatible with a wider range of contexts, making them available for pragmatic co-optation (honorification).

This definition is domain-general: it applies uniformly to number (plural), person (3rd), and definiteness (indefinite).

def Semantics.Presupposition.PhiFeatures.isSemanticUnmarked (c : Features.PrivativePair) : Bool

A phi-feature value is semantically unmarked iff its specLevel is 0 (vacuous presupposition).

Equations

• Semantics.Presupposition.PhiFeatures.isSemanticUnmarked c = (c.specLevel == 0)

def Semantics.Presupposition.PhiFeatures.isSemanticMarked (c : Features.PrivativePair) : Bool

A phi-feature value is semantically marked iff its specLevel is > 0 (substantive presupposition).

Equations

• Semantics.Presupposition.PhiFeatures.isSemanticMarked c = decide (c.specLevel > 0)

@[simp]

theorem Semantics.Presupposition.PhiFeatures.minimal_is_unmarked : isSemanticUnmarked Features.PrivativePair.minimal = true

The minimal cell is the unique unmarked cell.

@[simp]

theorem Semantics.Presupposition.PhiFeatures.maximal_is_marked : isSemanticMarked Features.PrivativePair.maximal = true

The maximal cell is marked.

@[simp]

theorem Semantics.Presupposition.PhiFeatures.intermediate_is_marked : isSemanticMarked Features.PrivativePair.intermediate = true

The intermediate cell is marked.

theorem Semantics.Presupposition.PhiFeatures.unmarked_iff_minimal (c : Features.PrivativePair) (hw : c.wellFormed = true) : isSemanticUnmarked c = true ↔ c = Features.PrivativePair.minimal

Only the minimal cell is unmarked among well-formed cells.

theorem Semantics.Presupposition.PhiFeatures.unmarked_vacuous_presup {E : Type u_1} (innerP outerP : E → Prop) (c : Features.PrivativePair) (hw : c.wellFormed = true) (hu : isSemanticUnmarked c = true) (x : E) : Core.Presupposition.PrProp.defined x (phiPresup innerP outerP c)

Unmarked cells have vacuous presuppositions via phiPresup.

theorem Semantics.Presupposition.PhiFeatures.wellFormed_specLevel_le_two (c : Features.PrivativePair) (hw : c.wellFormed = true) : c.specLevel ≤ 2

Well-formed cells have specLevel ≤ 2. This follows from the three-cell structure of PrivativePair — the maximum is maximal.specLevel = 2.

def Semantics.Presupposition.PhiFeatures.presupStrength (c : Features.PrivativePair) : ℕ

Presuppositional strength = specLevel. Higher specLevel = stronger presupposition = smaller domain.

Equations

• Semantics.Presupposition.PhiFeatures.presupStrength c = c.specLevel

def Semantics.Presupposition.PhiFeatures.presupWeakerThan (c₁ c₂ : Features.PrivativePair) : Bool

c₁ has a weaker presupposition than c₂.

Equations

• Semantics.Presupposition.PhiFeatures.presupWeakerThan c₁ c₂ = decide (c₁.specLevel < c₂.specLevel)

def Semantics.Presupposition.PhiFeatures.presupStrongerThan (c₁ c₂ : Features.PrivativePair) : Bool

c₁ has a stronger presupposition than c₂.

Equations

• Semantics.Presupposition.PhiFeatures.presupStrongerThan c₁ c₂ = decide (c₁.specLevel > c₂.specLevel)

theorem Semantics.Presupposition.PhiFeatures.minimal_weakest (c : Features.PrivativePair) (hw : c.wellFormed = true) (hne : c ≠ Features.PrivativePair.minimal) : presupWeakerThan Features.PrivativePair.minimal c = true

Minimal has the weakest presupposition among all cells.

theorem Semantics.Presupposition.PhiFeatures.maximal_strongest (c : Features.PrivativePair) (hw : c.wellFormed = true) (hne : c ≠ Features.PrivativePair.maximal) : presupStrongerThan Features.PrivativePair.maximal c = true

Maximal has the strongest presupposition among all cells.

§7: Conceivability Lifting of Phi-Feature Presuppositions

@cite{enguehard-2024} argues that number marking on indefinites triggers a conceivability presupposition: a singular indefinite presupposes it is conceivable the witness set has exactly one member; a plural indefinite presupposes it is conceivable the witness set has more than one member.

Conceivability is a general lifting on phi-feature presuppositions. For any phiPresup cell with entity-level presupposition p, the conceivability version asks whether p is satisfiable in a domain of conceivable entities. This interacts with Maximize Presupposition: when exactly one number's conceivability presupposition is satisfied, MP forces that number; when both are satisfied, the choice is underdetermined — opening the space for gradient probabilistic effects.

Entity-Level vs Cardinality Conceivability

Two layers of conceivability arise:

1. Entity-level (conceivableIn): some conceivable entity satisfies the presupposition p. This is the general lifting applicable to all phi-feature presuppositions (number, person, definiteness).

2. Cardinality (cardConceivable): some conceivable situation has a witness set of the right cardinality. This is specific to indefinite number marking, where the presupposition is about the predicate's extension rather than a particular entity.

The two layers connect: if a conceivable situation has exactly one witness, that witness is atomic; if ≥ 2, their sum is non-atomic.

Connection to PresuppositionContext.presupSatisfiable

Conceivability = satisfiability in context: presupSatisfiable c p from Core.Semantics.PresuppositionContext checks whether p.presup is compatible with context set c. The conceivability presupposition of an indefinite is the meta-requirement that the number feature's entity-level presupposition be satisfiable.

def Semantics.Presupposition.PhiFeatures.conceivableIn {E : Type u_1} (p C : E → Prop) : Prop

General conceivability: a property p is conceivable over a domain C iff some entity in C satisfies it. This lifts entity-level presuppositions to context-level satisfiability requirements.

Equations

• Semantics.Presupposition.PhiFeatures.conceivableIn p C = ∃ (e : E), C e ∧ p e

def Semantics.Presupposition.PhiFeatures.cellConceivableIn {E : Type u_1} (innerP outerP : E → Prop) (c : Features.PrivativePair) (C : E → Prop) : Prop

Conceivability lifting of a phi-feature presupposition: it is conceivable that the presupposition of cell c could be satisfied by some entity in domain C.

Equations

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

theorem Semantics.Presupposition.PhiFeatures.minimal_always_conceivable {E : Type u_1} (innerP outerP C : E → Prop) (hne : ∃ (e : E), C e) : cellConceivableIn innerP outerP Features.PrivativePair.minimal C

The minimal cell is always conceivable over any non-empty domain (vacuous presupposition).

theorem Semantics.Presupposition.PhiFeatures.conceivable_nesting {E : Type u_1} {innerP outerP : E → Prop} (hContain : ∀ (x : E), innerP x → outerP x) {c₁ c₂ : Features.PrivativePair} (hw₁ : c₁.wellFormed = true) (hw₂ : c₂.wellFormed = true) (hSpec : c₁.specLevel ≥ c₂.specLevel) (C : E → Prop) : cellConceivableIn innerP outerP c₁ C → cellConceivableIn innerP outerP c₂ C

Conceivability nests: if a more specified cell is conceivable, all less specified cells are too. Mirrors phiPresup_nesting.

theorem Semantics.Presupposition.PhiFeatures.sg_conceivable_iff_atom {E : Type u_1} [PartialOrder E] (outerP C : E → Prop) : cellConceivableIn Mereology.Atom outerP Features.PrivativePair.maximal C ↔ conceivableIn Mereology.Atom C

Sg conceivability ↔ some conceivable entity is atomic.

theorem Semantics.Presupposition.PhiFeatures.actual_implies_conceivable {E : Type u_1} (p C : E → Prop) (e : E) (hC : C e) (hp : p e) : conceivableIn p C

Actuality implies conceivability: if p e holds and e ∈ C, then p is conceivable in C. Standard presuppositions are special cases of conceivability presuppositions where the actual referent is in the conceivable domain.

theorem Semantics.Presupposition.PhiFeatures.conceivable_mono {E : Type u_1} (p : E → Prop) {C₁ C₂ : E → Prop} (hle : ∀ (e : E), C₁ e → C₂ e) : conceivableIn p C₁ → conceivableIn p C₂

Conceivability is monotone in the domain: enlarging the set of conceivable entities preserves conceivability.

def Semantics.Presupposition.PhiFeatures.cardConceivable {W : Type u_1} (witnessCard : W → ℕ) (conceivable : W → Prop) (cardPred : ℕ → Prop) : Prop

Witness-cardinality conceivability: some conceivable situation has a witness set whose cardinality satisfies cardPred.

W is a type of conceivable situations, witnessCard gives the cardinality of the indefinite's witness set in each situation, and cardPred is the number feature's cardinality requirement.

This generalizes the binary sg/pl contrast: for dual, cardPred = (· = 2); for paucal, cardPred = (2 ≤ · ∧ · ≤ 5).

Equations

• Semantics.Presupposition.PhiFeatures.cardConceivable witnessCard conceivable cardPred = ∃ (w : W), conceivable w ∧ cardPred (witnessCard w)

def Semantics.Presupposition.PhiFeatures.sgCardConceivable {W : Type u_1} (witnessCard : W → ℕ) (conceivable : W → Prop) : Prop

Sg indefinite conceivability: ∃ conceivable situation with exactly one witness (@cite{enguehard-2024} generalization 7).

Equations

• Semantics.Presupposition.PhiFeatures.sgCardConceivable witnessCard conceivable = Semantics.Presupposition.PhiFeatures.cardConceivable witnessCard conceivable fun (x : ℕ) => x = 1

def Semantics.Presupposition.PhiFeatures.plCardConceivable {W : Type u_1} (witnessCard : W → ℕ) (conceivable : W → Prop) : Prop

Pl indefinite conceivability: ∃ conceivable situation with ≥ 2 witnesses (@cite{enguehard-2024} generalization 7).

Equations

• Semantics.Presupposition.PhiFeatures.plCardConceivable witnessCard conceivable = Semantics.Presupposition.PhiFeatures.cardConceivable witnessCard conceivable fun (x : ℕ) => x ≥ 2

def Semantics.Presupposition.PhiFeatures.duCardConceivable {W : Type u_1} (witnessCard : W → ℕ) (conceivable : W → Prop) : Prop

Du indefinite conceivability: ∃ conceivable situation with exactly 2 witnesses.

Equations

• Semantics.Presupposition.PhiFeatures.duCardConceivable witnessCard conceivable = Semantics.Presupposition.PhiFeatures.cardConceivable witnessCard conceivable fun (x : ℕ) => x = 2

theorem Semantics.Presupposition.PhiFeatures.both_sg_pl_conceivable {W : Type u_1} (witnessCard : W → ℕ) (conceivable : W → Prop) (w₁ : W) (h₁c : conceivable w₁) (h₁ : witnessCard w₁ = 1) (w₂ : W) (h₂c : conceivable w₂) (h₂ : witnessCard w₂ ≥ 2) : sgCardConceivable witnessCard conceivable ∧ plCardConceivable witnessCard conceivable

Sg and pl conceivability are not complementary: both can hold when the conceivable domain contains situations of both kinds. This is the structural reason MP is underdetermined in intermediate cases.

theorem Semantics.Presupposition.PhiFeatures.sg_only_when_always_unique {W : Type u_1} (witnessCard : W → ℕ) (conceivable : W → Prop) (hall : ∀ (w : W), conceivable w → witnessCard w = 1) (hne : ∃ (w : W), conceivable w) : sgCardConceivable witnessCard conceivable ∧ ¬plCardConceivable witnessCard conceivable

When ALL conceivable situations have unique witnesses, only sg is conceivable — pl conceivability fails.

theorem Semantics.Presupposition.PhiFeatures.pl_only_when_never_unique {W : Type u_1} (witnessCard : W → ℕ) (conceivable : W → Prop) (hall : ∀ (w : W), conceivable w → witnessCard w ≥ 2) (hne : ∃ (w : W), conceivable w) : plCardConceivable witnessCard conceivable ∧ ¬sgCardConceivable witnessCard conceivable

When ALL conceivable situations have multiple witnesses, only pl is conceivable — sg conceivability fails.

theorem Semantics.Presupposition.PhiFeatures.conceivability_presups_incomparable : (∃ (witnessCard : Unit → ℕ) (conceivable : Unit → Prop), sgCardConceivable witnessCard conceivable ∧ ¬plCardConceivable witnessCard conceivable) ∧ ∃ (witnessCard : Unit → ℕ) (conceivable : Unit → Prop), ¬sgCardConceivable witnessCard conceivable ∧ plCardConceivable witnessCard conceivable

Conceivability presuppositions are incomparable: neither sg's entails pl's nor vice versa. This means standard Maximize Presupposition (which requires a strength ordering) cannot select between them — a structural gap that gradient probabilistic effects fill (@cite{enguehard-2024} §4.1).

theorem Semantics.Presupposition.PhiFeatures.negative_context_nontrivial {W : Type u_1} (witnessCard : W → ℕ) (w₀ : W) (hzero : witnessCard w₀ = 0) : ¬witnessCard w₀ = 1 ∧ ¬witnessCard w₀ ≥ 2

In negative contexts (witness set empty in the actual situation), the conceivability presupposition is non-trivially about OTHER conceivable situations — the actual one witnesses neither sg nor pl conceivability. This is why conceivability presuppositions are observable under negation while scalar implicatures are not.

theorem Semantics.Presupposition.PhiFeatures.du_implies_pl {W : Type u_1} (witnessCard : W → ℕ) (conceivable : W → Prop) : duCardConceivable witnessCard conceivable → plCardConceivable witnessCard conceivable

Du conceivability entails pl conceivability: if exactly 2 is conceivable, then ≥ 2 is conceivable.

theorem Semantics.Presupposition.PhiFeatures.cardConceivable_mono {W : Type u_1} (witnessCard : W → ℕ) {C₁ C₂ : W → Prop} (cardPred : ℕ → Prop) (hle : ∀ (w : W), C₁ w → C₂ w) : cardConceivable witnessCard C₁ cardPred → cardConceivable witnessCard C₂ cardPred

Conceivability is monotone in the conceivable domain: enlarging the set of conceivable situations preserves conceivability.