ABLE: A Bit Like English #
@cite{beaver-2001}
ABLE is the fragment language of @cite{beaver-2001}'s Presupposition and Assertion in Dynamic Semantics. It serves as the formal object language for Presuppositional Update Logic (PUL), mapping English-like formulas to context change potentials.
Core Ideas #
ABLE's key innovation is the presupposition operator ∂ (D59), a test that checks whether the current context already entails a proposition. When it does, the context passes through unchanged; when it doesn't, the update is undefined (yields ∅). This makes presupposition projection fall out of structural admittance (D30) — the requirement that each subformula's presupposition be satisfied at its local context.
Formal Definitions #
The formalization captures the propositional core of PUL (@cite{beaver-2001} Ch. 6) and ABLE (Ch. 7), without discourse markers or extended sequences. Connectives follow D52 (Ch. 7 §7.4), modals follow D60 (Ch. 8 §8.3), and the presupposition operator is D59 (Ch. 7 §7.6).
| ABLE | Formal | CCP equivalent |
|---|---|---|
pred sat | {p ∈ σ \| sat p} | updateFromSat |
NOT φ | σ \ σ[φ] | (PUL-specific) |
AND φ ψ | σ[φ][ψ] | CCP.seq |
MIGHT φ | σ if σ[φ]≠∅, ∅ o/w | CCP.might |
∂ φ | σ if σ[φ]=σ, ∅ o/w | CCP.must |
Important: ABLE NOT uses set complement within the input (σ \ σ[φ]),
which differs from CCP.neg (test-based pass/fail). This is how PUL
handles negation — it is eliminative but not a test.
Simplification: Full ABLE (D52) takes anaphoric closure (↓) before negation to strip discourse markers; our set-based version omits this since we don't model discourse markers.
Key Results #
- Fact 8.1: Presupposition projects through NOT, AND, IF...THEN
- Fact 8.3: Conditional presupposition — second conjunct's presupposition becomes conditional on first conjunct
- Lemma 8.6: Satisfaction ↔ inconsistency with NOT (eliminativity bridge)
- Fact 8.7: MUST is a test for satisfaction
- Facts 8.5, 8.8: MIGHT and MUST are tests; presupposition projects through them
- D45/MP5: Entailment — equivalent to
CCP.entails(eliminativity makes guard redundant)
ABLE formula type. @cite{beaver-2001} Ch. 7.
The five constructors correspond to the five basic ABLE operations. Connectives (NOT, AND) are D52 (§7.4), epistemic modality (MIGHT) is D60 (§8.3), and the presupposition operator (∂) is D59 (§7.6). Derived connectives (IF...THEN, MUST, OR) are defined as abbreviations.
- pred
{P : Type u_2}
(sat : P → Prop)
: Formula P
Predicational update: filter by satisfaction. D48.
- not
{P : Type u_2}
(φ : Formula P)
: Formula P
Negation: complement within input. D52.
- and
{P : Type u_2}
(φ ψ : Formula P)
: Formula P
Conjunction (sequencing): update by φ then ψ. D52.
- might
{P : Type u_2}
(φ : Formula P)
: Formula P
Epistemic possibility: compatibility test. D60.
- presup
{P : Type u_2}
(φ : Formula P)
: Formula P
Presupposition operator ∂: full support test. D59.
Instances For
Evaluate an ABLE formula as a CCP. @cite{beaver-2001} D52, D59, D60.
Each constructor maps to its PUL update:
pred: filter by satisfaction (updateFromSat) — D48not: set complement within input (σ \ σ[φ]) — D52and: sequential update (σ[φ][ψ]) — D52might: compatibility test — D60presup(∂): full support test — D59
Equations
- (Semantics.Dynamic.ABLE.Formula.pred sat).eval = fun (σ : Semantics.Dynamic.Core.InfoStateOf P) => {p : P | p ∈ σ ∧ sat p}
- φ.not.eval = fun (σ : Semantics.Dynamic.Core.InfoStateOf P) => σ \ φ.eval σ
- (φ.and ψ).eval = fun (σ : Semantics.Dynamic.Core.InfoStateOf P) => ψ.eval (φ.eval σ)
- φ.might.eval = fun (σ : Semantics.Dynamic.Core.InfoStateOf P) => if Set.Nonempty (φ.eval σ) then σ else ∅
- φ.presup.eval = fun (σ : Semantics.Dynamic.Core.InfoStateOf P) => if φ.eval σ = σ then σ else ∅
Instances For
Structural admittance: a formula's presuppositions are satisfied at every local context encountered during evaluation.
This captures @cite{beaver-2001} D30 (Admittance) recursively over formula structure — the key to presupposition projection. A state σ admits φ iff:
- For
pred: always admitted (no presuppositions) - For
not φ: σ admits φ - For
and φ ψ: σ admits φ AND σ[φ] admits ψ - For
might φ: σ admits φ - For
∂ φ: σ already entails φ (i.e., σ[φ] = σ)
Equations
- (Semantics.Dynamic.ABLE.Formula.pred sat).pulAdmits = fun (x : Semantics.Dynamic.Core.InfoStateOf P) => True
- φ.not.pulAdmits = fun (σ : Semantics.Dynamic.Core.InfoStateOf P) => φ.pulAdmits σ
- (φ.and ψ).pulAdmits = fun (σ : Semantics.Dynamic.Core.InfoStateOf P) => φ.pulAdmits σ ∧ ψ.pulAdmits (φ.eval σ)
- φ.might.pulAdmits = fun (σ : Semantics.Dynamic.Core.InfoStateOf P) => φ.pulAdmits σ
- φ.presup.pulAdmits = fun (σ : Semantics.Dynamic.Core.InfoStateOf P) => φ.eval σ = σ
Instances For
∂ is a test: it either passes (returns input) or fails (returns ∅). @cite{beaver-2001} D59, D61 (Tests).
∂ is eliminative.
Admittance of ∂φ is equivalent to σ[φ] = σ.
Fact 8.1 (i): Presupposition projects through NOT.
If φ presupposes ψ (i.e., φ = ∂ψ AND χ), then NOT φ also presupposes ψ. Here we prove the component: admitting NOT φ requires admitting φ.
Fact 8.1 (ii): Left presupposition projects through AND.
Admitting AND φ ψ requires admitting φ (among other things).
Admitting AND φ ψ requires that the intermediate context σ[φ] admits ψ. This is the structural basis for conditional presupposition projection (used in the proof of Fact 8.3).
Fact 8.1 (iii): Presupposition projects through IF...THEN.
Admitting IF φ THEN ψ (= NOT(φ AND NOT ψ)) requires admitting φ.
Fact 8.5: MIGHT is a test.
MIGHT is eliminative.
Fact 8.8 (1): Presupposition projects through MIGHT.
Admitting MIGHT φ requires admitting φ.
Fact 8.8 (2): MUST φ = NOT(MIGHT(NOT φ)) projects presuppositions of φ. Admitting MUST φ requires admitting φ.
ABLE pred = updateFromSat (via identity).
The predicational constructor pred sat is definitionally equal to
updateFromSat when the satisfaction relation ignores the formula
parameter.
ABLE NOT ≠ CCP.neg in general.
PUL negation is set complement within the input (σ \ σ[φ]),
while CCP.neg is a test (pass/fail on the whole context).
They coincide only when φ is eliminative AND σ[φ] = ∅ or σ[φ] = σ.
Predicational updates are eliminative.
NOT is always eliminative (σ \ X ⊆ σ, regardless of X).
AND preserves eliminativity.
All ABLE formulas are eliminative (output ⊆ input). This is the inductive closure of the per-constructor eliminativity results above.
A state σ satisfies φ iff σ[φ] = σ (updating adds no information). @cite{beaver-2001} D29 / MP4 (closure-based; we use the set-based equivalent: φ is satisfied when the update is a fixed point).
Instances For
A formula φ presupposes ψ iff every state that admits φ also satisfies ψ. @cite{beaver-2001} D46, MP6.
Equations
- φ.presupposes ψ = ∀ (σ : Semantics.Dynamic.Core.InfoStateOf P), φ.pulAdmits σ → ψ.satisfies σ
Instances For
Lemma 8.6: Satisfaction ↔ inconsistency with NOT.
σ satisfies φ iff σ is not consistent with NOT φ. @cite{beaver-2001} Ch. 8 §8.3.
The proof uses eliminativity: since φ.eval σ ⊆ σ (all ABLE formulas are eliminative), the fixed-point condition φ.eval σ = σ reduces to checking that σ \ φ.eval σ is empty.
Fact 8.7 (1): MUST is a test. @cite{beaver-2001} Ch. 8 §8.3.
MUST is eliminative.
Fact 8.7 (2–3): MUST φ is a test for satisfaction of φ.
σ⟦MUST φ⟧ = σ iff σ satisfies φ; σ⟦MUST φ⟧ = ∅ iff ¬σ satisfies φ.
The proof chains through Lemma 8.6: satisfaction ↔ ¬consistent-with-NOT ↔ MIGHT(NOT φ) fails ↔ NOT(MIGHT(NOT φ)) passes. @cite{beaver-2001} Ch. 8 §8.3.
Fact 8.1: If φ presupposes ψ, then NOT φ, φ AND χ, and φ IMPLIES χ all presuppose ψ. @cite{beaver-2001} Ch. 8 §8.2.1.
The key insight: the set of contexts admitting NOT φ (or φ AND χ, etc.) is a SUBSET of those admitting φ. So if every context admitting φ satisfies ψ, then every context admitting NOT φ also satisfies ψ.
Fact 8.2: Transitivity of presupposition. If φ presupposes ψ, and ψ presupposes χ, then φ presupposes χ. @cite{beaver-2001} Ch. 8 §8.2.1.
This follows because admitting φ implies satisfying ψ (= ψ.eval σ = σ), which means σ trivially admits ψ (since ψ.eval σ = σ makes every subformula's presupposition vacuously satisfied at a fixed point).
Fact 8.3: Conditional presupposition. If φ presupposes ψ, then χ AND φ presupposes χ IMPLIES ψ. @cite{beaver-2001} Ch. 8 §8.2.1.
The second conjunct's presupposition becomes conditional on the first conjunct. This is the hallmark of CCP-based projection.
Fact 8.8: Presupposition projects through MIGHT and MUST. If φ presupposes ψ, then MIGHT φ and MUST φ also presuppose ψ. @cite{beaver-2001} Ch. 8 §8.3.
Entailment in ABLE (D45): φ entails ψ iff every state resulting from updating with φ satisfies ψ.
@cite{beaver-2001} Ch. 7 §7.2, Meaning Postulate MP5:
entails = λF λF' [∀I∀J, I{F}J → J satisfies F']
In our set-based formulation (without discourse markers), this reduces to: for all σ, ψ.eval(φ.eval σ) = φ.eval σ.
Instances For
ABLE entailment ↔ CCP entailment.
The nonemptiness guard in CCP.entails is redundant for ABLE formulas
because all ABLE formulas are eliminative: ψ.eval ∅ = ∅.
@cite{beaver-2001} D45 = CCP.entails modulo this vacuous case.
Entailment preserves satisfaction: if φ ⊨ ψ and σ satisfies φ, then σ satisfies ψ.