Veridicality ↔ Presupposition Bridge #
@cite{beaver-condoravdi-2003} @cite{heim-1983} @cite{ogihara-steinert-threlkeld-2024}
Connects three layers of the temporal connective formalization:
- Fragment field:
TemporalExprEntry.complementVeridical : Bool - Theory proof: e.g.,
Anscombe.after A B → ∃ t, t ∈ timeTrace B - Presupposition theory: veridical connectives presuppose their complement
(modeled as
PrPropwith complement occurrence as presupposition)
What This File Proves #
For each temporal connective:
- The Fragment's
complementVeridicalfield is grounded in a theory-level proof: veridical entries have proofs that the connective entails complement instantiation; non-veridical entries have counterexamples. - The
complementVeridicalfield matches the empirical data in the O&@cite{ogihara-steinert-threlkeld-2024} study (data layer agreement).
The Explanatory Chain #
Theory (Karttunen.lean) Fragment (TemporalExpressions.lean)
after_veridical_complement ───────► after_.complementVeridical = true
before_nonveridical (counterex.) ──► before_.complementVeridical = false
when_veridical_complement ─────────► when_conn.complementVeridical = true
until_veridical_complement ────────► until_.complementVeridical = true
since_veridical_complement ────────► since_conn.complementVeridical = true
by_veridical_main ─────────────────► by_deadline.complementVeridical = true
│
▼
Data (OgiharaST2024/Data.lean)
after_veridical.complementEntailed = true
before_nonveridical.complementEntailed = false
Presupposition Modeling #
Veridical temporal connectives can be modeled as presuppositional propositions (PrProp) where the presupposition is that the complement event is instantiated. Non-veridical connectives carry no such presupposition. This connects the temporal connective veridicality to the general presupposition projection framework.
Veridical connectives #
For each connective with complementVeridical = true, the theory proves
that the connective entails the existence of a complement witness.
after is veridical: Fragment field matches theory proof.
Theory: Anscombe.after A B → ∃ t, t ∈ timeTrace B.
Fragment: after_.complementVeridical = true.
when is veridical: Fragment field matches theory proof.
Theory: Karttunen.when_ A B → ∃ t, t ∈ timeTrace B.
Fragment: when_conn.complementVeridical = true.
until (durative) is veridical: Fragment field matches theory proof.
Theory: Karttunen.until A B → ∃ t, t ∈ timeTrace B (= when_veridical).
Fragment: until_.complementVeridical = true.
since is veridical: Fragment field matches theory proof.
Theory: Karttunen.since A B → ∃ t, t ∈ timeTrace B.
Fragment: since_conn.complementVeridical = true.
by is veridical w.r.t. its main clause: Fragment field matches theory proof.
Theory: Karttunen.by_ A B → ∃ t, t ∈ timeTrace A.
Fragment: by_deadline.complementVeridical = true.
Note: by is veridical for its main clause argument, not its complement
(the deadline). We record complementVeridical = true because the
nominal complement (the deadline time) is trivially instantiated.
Non-veridical connectives #
For each connective with complementVeridical = false, the theory provides
a counterexample: a scenario where the connective holds but the complement
has no witness.
before is non-veridical: Fragment field matches theory counterexample.
Theory: ∃ A B, Anscombe.before A B ∧ ¬(∃ t, t ∈ timeTrace B).
Fragment: before_.complementVeridical = false.
The counterexample uses A = {point(0)}, B = ∅: "A before nothing"
is vacuously true because ∀t'∈∅, 0 < t'.
The Fragment's complementVeridical field matches the empirical data
from the O&@cite{ogihara-steinert-threlkeld-2024} study for after.
The Fragment's complementVeridical field matches the empirical data
from the O&@cite{ogihara-steinert-threlkeld-2024} study for before.
Three-layer consistency for after: data, fragment, and theory all agree.
Data: complementEntailed = true
Fragment: complementVeridical = true
Theory: proof of complement veridicality
Three-layer consistency for before: data, fragment, and theory all agree.
Data: complementEntailed = false
Fragment: complementVeridical = false
Theory: counterexample to complement veridicality
whenever is veridical w.r.t. its complement (when B is nonempty):
∀t∈B, t∈A requires B-witnesses to exist for a non-vacuous claim.
Fragment: whenever_conn.complementVeridical = true.
as soon as is veridical: truth-conditionally equivalent to after.
Fragment: asSoonAs.complementVeridical = true.
as long as is veridical: truth-conditionally equivalent to while.
Fragment: asLongAs.complementVeridical = true.
The veridicality pattern is determined by quantifier force: ∃-based connectives (after, when, until_dur, since) are veridical because ∃ requires a witness; ∀-based connectives (before) are non-veridical because ∀ is vacuously true on the empty set.
This is the core theoretical explanation: complementVeridical
is not stipulated — it follows from the quantifier structure of
each connective's definition.
A temporal connective modeled as a presuppositional proposition. The presupposition records whether the complement must be instantiated (veridical) or not (non-veridical). The assertion is the temporal ordering relation.
- For after: presup = "B occurred" (complement is instantiated), assertion = "some A-time follows some B-time"
- For before: presup = ⊤ (no complement presupposition), assertion = "some A-time precedes all B-times"
This connects temporal connective veridicality to the general presupposition framework. Veridical connectives are like factive verbs (know, regret) — they presuppose their complement.
Equations
Instances For
A veridical connective (after, when, etc.) presupposes its complement. When the presupposition fails (complement not instantiated), the sentence is undefined — there is no truth value to assign. "He left after she arrived" presupposes "she arrived."
A non-veridical connective (before) does NOT presuppose its complement. "He left before she arrived" makes no commitment about arrival. The sentence is defined (has a truth value) regardless of whether the complement event occurred.
Negating a veridical connective preserves its complement presupposition. "He didn't leave after she arrived" still presupposes "she arrived." This is the hallmark of presuppositions: projection through negation.
@cite{beaver-condoravdi-2003} identify three readings of before, distinguished by whether the complement event is instantiated in the context set. Each corresponds to a different presuppositional status of the complement:
- Veridical: complement occurs in all context worlds → complement presupposed (filtered by context)
- Counterfactual: complement occurs in no context world → complement counterpresupposed (known to be false)
- Non-committal: complement occurs in some context worlds → no presupposition either way
The common thread: before itself carries NO complement presupposition. The apparent veridicality or counterfactuality comes from context.
- veridical : BeforeContextualStatus
- counterfactual : BeforeContextualStatus
- nonCommittal : BeforeContextualStatus
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
All three readings of before are compatible with complementVeridical = false.
This is because before never ENTAILS complement occurrence — each
reading is a different contextual restriction on the non-veridical
base semantics.
The O&@cite{ogihara-steinert-threlkeld-2024} data covers all three B&C readings:
before_nonveridical: basic non-veridical (compatible with any reading)before_counterfactual: counterfactual reading (bomb example)before_noncommittal: non-committal reading (Supreme Court example)