Corfield on presuppositions

This post continues from the conversation in this other post.

The book “Modal Homotopy Type Theory”, by David Corfield, proposes a type-theoretical interpretation of presuppositions:

With the idea of a context available, type theory should provide us with a way to distinguish between consequences and presuppositions. Whereas 'James has stopped smoking' presupposes that at some point he was in the habit of smoking, from the proposition 'n is the sum of two odd numbers' we may conclude that n is even. Presuppositions are what need to be in place for a type to be formed or a term introduced. Consequences result from application of rules to existing judgements. For example,

• Presupposition: from $A \times B : \text{Type}$, we must have that $A, B : \text{Type}$.
• Consequence: from $c : A \times B$, we can conclude that $p(c) : A$ and $q(c) : B$.

Despite this neat distinction, we are inclined to see an inference occurring in the case of presupposition just as much as in the case of consequence. It is easy to think that we infer from 'James has stopped smoking' that he was in the habit of smoking. What seems to be occurring is that we are presented with a proposition, $P$, such as 'James has stopped smoking'. Then, to interpret it, it is our job to provide the minimal context, $\Gamma$, which can support the formation of $P$:

$$ \Gamma \vdash P : \text{Prop}. $$

Then say $\Gamma = x_1 : A_1, x_2 : A_2, ..., x_n : A_n$, from which we extract one clause of the context

$$ x_1 : A_1, x_2 : A_2, ..., x_i : A_i, x_j : A_j, ..., x_n : A_n \vdash x_j : A_j \text{ for } 1 \leq j \leq n. $$

We have trivially

$$ x_1 : A_1, x_2 : A_2, ..., x_i : A_i, ..., x_n, y : P \vdash x_j : A_j, $$

at which point we forget the context and think we have an entailment

$$ y : P \vdash x_j : A_j. $$

This is to be contrasted with the case when we have the means in a context to derive a new proposition, such as with

$$ x : A, f : [A, B] \vdash f(x) : B. $$

Ranta in ‘Constructive Type Theory’ (2015, p. 358) proposes along similar lines that we distinguish these operations as follows:

• B presupposes A means $x : A \vdash B(x) : \text{Type}$.
• A semantically entails B means $x : A \vdash b(x) : B$.

Evaluate to what extent this captures the idea of presuppositions in pragmatics.

How Corfield & Ranta transpose presupposition into type-theoretic terms

	Pragmatic presupposition (traditional view)	Corfield/Ranta account
Intuition	Backgrounded content that must already be common ground for an utterance to be felicitous	Backgrounded typing assumptions that must already be in the context Γ for the judgment “Γ ⊢ P : Prop/Type” to be well-formed
Formal locus	A condition on the context of discourse (Stalnaker 1973)	A condition on the context of hypotheses in Martin-Löf type theory
Example	“James has stopped smoking” presupposes James smoked	The type of stoppedSmoking(james) can only be formed in a Γ that already contains a proof of Smokes(james)
Consequence	Survive negation, interrogation, etc.	Type-formation requirements are untouched by logical operators; Γ stays the same

In Corfield’s words, presuppositions are “what need to be in place for a type to be formed,” while consequences are what can be derived once the term exists (ncatlab.org). Ranta formulates the same idea as

“B presupposes A ⇝ x : A ⊢ B(x) : Type” (ncatlab.org)

so presupposition is treated as well-formedness, not as an entailment inside the calculus.

---

Where this mapping works well

Phenomenon	Match with type-theoretic treatment	Why
Need for a “licensing” context	✓ Exact: a judgment is ill-typed without the presupposed assumptions—mirrors pragmatic infelicity (“Hey, wait, James never smoked!”).
Projection under negation & questions	✓ Requirements in Γ are structural, so ¬P, ?P, if P then Q, etc. all still need Γ. This captures the classical projection profile of presuppositions.
Accommodation	✓ Γ can be extended on the fly: a hearer who lacks Smokes(james) can add it, mirroring Stalnaker-style accommodation. Dependently-typed dynamic frameworks (e.g. Bekki’s Dependent-Type Semantics) already implement such updates .
Distinction from entailment	✓ Clear: entailments are derivable judgments (Γ ⊢ b : B) while presuppositions are premises (A∈Γ). This dissolves the frequent classroom confusion “presupposition vs. implication”.

These points suggest that Corfield’s proposal captures the normative side of presupposition—the idea that an utterance demands a certain backdrop of accepted information.

---

Where the fit is incomplete

Empirical issue from pragmatics	How far the type-theoretic view goes	What is still missing
Lexical triggering spectrum (hard vs. soft triggers)	Hard triggers like stop map nicely to formation rules. Soft triggers (too, again) often feel like inferences rather than strict typing needs.	Would need graded or optional formation rules—something not standard in MLTT.
Local vs. global satisfaction / filtering (e.g. “If John smoked, he stopped”)	A single, monotone Γ can’t express that the antecedent satisfies the presupposition only inside the conditional’s branch.	Requires dynamic or multi-stage contexts (cf. DRT, dynamic predicate logic) (plato.stanford.edu) or dependent-type dynamic logics.
Cancellation / suspension of soft presuppositions	MLTT treats presuppositions as necessary for typing, so “cancelling” them is impossible.	Softness would need to be encoded as mergeable or optional assumptions, e.g. via modal types or proof irrelevance.
Processing asymmetries (experimental work on time-course, memory) (degruyterbrill.com)	Not addressed—type theory is static and proof-oriented.	Cognitive models of proof search or incremental context-building would have to be added.
Lexical idiosyncrasies & pragmatic strengthening	Requires heavy lexical typing for every trigger; quickly becomes unwieldy.	Hybrid approaches often delegate most trigger-specific content to the lexicon plus pragmatic reasoning.

---

Relation to other formal accounts

• Dynamic semantics views a sentence as a context-update function; presuppositions are defined preconditions on that function (plato.stanford.edu). Corfield’s Γ-typing idea is a Curry–Howard analogue of those preconditions.
• Dependent-Type Semantics (Bekki, Tanaka & Mineshima) refines this by giving proof-objects for presuppositions and showing how factive verbs or anaphora inject them compositionally .
• Modal variants of HoTT (Corfield ch. IV & VII) suggest using necessity or possibility modalities to mark information-state sensitivity; this dovetails with attempts to model soft presuppositions as default modal assumptions.

---

Bottom line

Corfield’s and Ranta’s treatment elegantly reconstructs the structural side of presupposition within dependent type theory: Presuppositions are precisely those pieces of information that must already be typed in the context for the utterance to compile.

This gives a clean logical contrast with consequential entailment and provides a Curry–Howard bridge to dynamic‐semantics talk of context preconditions. However, the approach is only a first pass on the full pragmatic phenomenon:

• It handles projection and accommodation in a principled way,
• but it lacks mechanisms for soft triggers, local filtering, speaker‐oriented cancellation, and psycholinguistic gradience.

To reach empirical adequacy, one needs to enrich the pure MLTT picture with dynamic context-updates, graded modalities, and lexical semantics—directions already explored in Dependent-Type Semantics and recent modal HoTT work. Still, Corfield’s proposal shows that type theory can serve as a unifying proof-theoretic backbone for future, more linguistically realistic models of presupposition.