📄 Compositionality for Presuppositions over Tableaux

Summary

The paper tackles a long-standing puzzle: how to compute the presuppositions of a compound statement built with if…then, and, and or from the presuppositions of its atomic parts, without falling into the trap where presupposition-as-entailment makes every presupposition a tautology. Gervás represents sentences as propositional formulas and uses a modified tableau calculus in which the branching (β) rules list every truth-value combination explicitly rather than the minimal set of cases. This yields the Coverage Property: every atom appears, negated or not, on every open branch, so each branch behaves like a truth-table row that can be pruned when it becomes inconsistent. Two simple rules then decide presupposition. On a branch, a presupposition holds unless the branch already asserts it, asserts its negation, or contains a clashing presupposition. A whole tableau presupposes whatever its open branches presuppose. The rules reproduce the classic textbook judgments, including disjunction and context effects in discourse. The paper argues the method is better grounded than the accounts of Beaver, Mercer and van der Sandt.

Key points

• Venue: the workshop Computational Logic for Natural Language Processing (COMPULOG/ELSNET/EAGLES), Edinburgh, April 1995.
• Change to the calculus: only the β-rules differ from standard semantic tableaux (ST). The resulting presuppositional tableaux (PT) are argued to close exactly when ST tableaux do, so PT still works as a decision method.
• Rule 1 (branch level): a presupposition on an open branch survives unless one of three things is true:
  • the branch already asserts it;
  • the branch asserts its negation;
  • another atom on the branch presupposes its negation.
• Rule 2 (tableau level): a tableau presupposes something if and only if an open branch does. By the Coverage Property, branches never disagree on this.
• Satisfaction and cancellation:
  • A presupposition φ is satisfied when adding ¬φ closes the tableau.
  • It is canceled when adding φ closes it.
  • In hybrid cases, some branches close on φ and others on ¬φ. One example is a conditional whose antecedent states that a typewriter exists and whose consequent says that this typewriter is blue; such cases are handled by blocking the presupposition locally.
• Stated limitations: asserted and presupposed information are not treated in a unified way, and defeasibility is not addressed. Both are deferred to follow-up work.

Interesting ideas

• I1. Treating presupposition as information weaker than assertion, so it is dropped whenever it duplicates or contradicts an asserted literal, gives one principled filter instead of a separate projection rule for each connective.
• I2. Expanding disjunctions and conditionals into every compatible truth combination, not the minimal proof-oriented set, keeps all atoms visible on every alternative and makes "open possibilities" explicit.
• I3. Checking presuppositions locally per alternative, rather than globally against the whole context, is what lets the method handle mixed cases where some readings support a presupposition and others refute it.
• I4. Defining satisfaction and cancellation as "does adding ¬φ, or φ, make the state inconsistent" turns vague pragmatic notions into mechanical consistency tests.
• I5. Because the rules rely only on general semantics plus the Coverage Property, new connectives can be added without new presupposition rules.

For Mova

How these ideas could serve Mova, our small open language model — its files, stages and tests:

• I1 (frames): prag could store presupposition triggers (definites, factives) as weak candidate facts and discard them when the clause or the discourse already asserts or denies them.
• I2 (world): when a text says "either X or Y", the world model could keep fully enumerated alternative worlds, where X and Y each appear as true or false, and prune them as later sentences close some of them.
• I3 (answer): a QA reader on tales could check a question's presupposition (e.g. "Why did the fox leave?") branch by branch. It would answer "unknown" or point out a false premise when the alternatives disagree.
• I4 (learn): these closure tests could serve as negative controls in evaluation, checking that the system never asserts a presupposition the world state cancels.
• I5 (frames): new discourse connectives (e.g. unless, only if) could be supported just by giving their truth-table expansion, with presupposition handling inherited automatically.