Derive CG requirement from a VerbEntry's veridicality.
This is the BRIDGE function that interprets Fragment data theoretically. The derivation lives HERE (Theory layer), not in Fragments.
Equations
Instances For
Get effective CG requirement for a verb, handling exceptions.
For most verbs: derived from veridicality For yǐwéi: exceptional postsupposition ◇¬p (weak contrafactive)
Equations
- One or more equations did not get rendered due to their size.
Instances For
Theorem: yǐwéi is flagged as having exceptional postsupposition.
This theorem would BREAK if:
- yǐwéi is removed from the exception list
- The flag function changes behavior
Breakage signals: re-evaluate whether yǐwéi still needs special handling.
Theorem: yǐwéi's effective CG requirement is weak contrafactive.
This captures @cite{glass-2025}: yǐwéi requires CG ◇ ¬p.
Theorem: yǐwéi's derived CG requirement (from veridicality) is NONE.
This proves the exception IS necessary: veridicality alone gives nothing, but yǐwéi actually has a weak contrafactive postsupposition.
Theorem: yǐwéi's exception IS justified.
The exception provides something (weak contrafactive) that derivation doesn't (none). If this theorem ever becomes FALSE, the exception is no longer needed.
Map a CGRequirement to the corresponding causal variables for PLC checking.
- Factive (positive × necessity): presup = p, at-issue = B(a)(p)
- Strong contrafactive (negative × necessity): presup = ¬p, at-issue = B(a)(p)
For weak contrafactives and nonfactives, the PLC doesn't directly apply because they have postsuppositions or no CG requirement.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Check if a CGRequirement satisfies the Predicate Lexicalization Constraint.
Returns none if the PLC doesn't apply (postsuppositions, no CG requirement).
Returns some true if it satisfies PLC.
Returns some false if it violates PLC.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Theorem: Factive requirements satisfy the PLC.
Factives like "know" have presup=p and at-issue=B(a)(p). There's a causal chain p → indic(p) → acq(a)(iₚ) → B(a)(p).
Theorem: Strong contrafactive requirements violate the PLC.
Hypothetical "contra" would have presup=¬p and at-issue=B(a)(p). There's NO causal chain from ¬p to B(a)(p).
Theorem: Weak contrafactive requirements are not subject to the PLC.
@cite{glass-2025} @cite{roberts-ozyildiz-2025} argues that yǐwéi's falsity inference is a postsupposition about the output context, not a presupposition about the input context. The PLC constrains presupposition-assertion pairs, not postsuppositions.
For verbs with a CGRequirement, check if the requirement is theoretically valid. A requirement is valid if it either:
- Satisfies the PLC (for presuppositions), or
- Is not subject to the PLC (for postsuppositions)
Equations
Instances For
Key Result: Strong contrafactives are invalid.
This is WHY they're unattested: they would require a causal chain from ¬p to B(x)(p), which doesn't exist in normal belief formation.
The Contrafactive Gap Explained
The gap between factives and strong contrafactives follows from:
- A general causal constraint on lexicalization (the PLC)
- The asymmetric structure of belief formation
This is not a stipulation but a DERIVATION from:
- Facts about how beliefs are formed (via evidence acquisition)
- The requirement that presuppositions causally support at-issue content
The result: {factive, weak_contrafactive} are valid; {strong_contrafactive} is not.
Per-Verb Verification #
Each verb gets explicit theorems that will BREAK if:
- Its semantic structure changes incompatibly
- The derivation rules change
This creates the "dense web" where changes propagate and get caught.
All English attitude verbs for batch verification
Equations
- One or more equations did not get rendered due to their size.
Instances For
Verify all English attitude verbs have valid derived CG requirements.
Valid means: either satisfies PLC or is not subject to PLC.
CGRequirement.satisfied: Concrete Evaluation #
The derivation chain is:
attitudeBuilder → veridicality → deriveCGRequirement → CGRequirement → satisfied
This section exercises the final link: given a concrete context set and proposition, does the CG requirement hold?
We construct a minimal 2-world model: w₀ where p is true, w₁ where p is
false. A factive context (where all interlocutors take p for granted) contains
only w₀. A neutral context contains both.
Factive requirement is satisfied in a factive context (CG ⊨ p).
Factive requirement fails in a neutral context (some worlds lack p).
Weak contrafactive requirement (◇¬p) is satisfied in neutral context.
Weak contrafactive requirement fails in factive context (no ¬p worlds).
Strong contrafactive requirement (CG ⊨ ¬p) is satisfied only in counter-factive context. This requirement type is UNATTESTED.
Strong contrafactive fails in neutral context.
End-to-end: derive "know"'s CG requirement from its Fragment data, then verify it's satisfied in a factive context.
This closes the full chain:
know.attitudeBuilder →.veridical → deriveCGRequirement →.factive → satisfied
End-to-end: "know"'s requirement fails in a neutral context.
End-to-end: "believe" has no CG requirement, so satisfaction is vacuously none.
Handling yǐwéi's Exception #
yǐwéi's postsupposition (◇¬p) is exceptional because:
- It's NOT a presupposition (input context) but a postsupposition (output)
- It cannot be derived from veridicality alone
- It's specific to certain Mandarin verbs
This exception is handled in the Mandarin bridge module, NOT in Fragments. The Fragment layer remains theory-neutral.
What Happens If yǐwéi's Exception Becomes Derivable? #
If future analysis shows yǐwéi's ◇¬p requirement IS derivable from some general principle (e.g., a new veridicality category), then:
- Add the new derivation rule to
deriveCGRequirementin Doxastic.lean - Update verbs in Fragments/Mandarin to have the appropriate attitudeBuilder
- Per-verb theorems here verify the derivation produces correct results
- The Mandarin bridge exception becomes unnecessary
The system enforces: derive what you can, stipulate only what you must.