Accounts of presupposition projection #
A theory of projection says when a context accepts a sentence of the fragment that the theories
share, under an interpretation of its atoms (Eval.Projection.Theory): a formula of the
propositional fragment, and a quantified clause if the theory covers them. A theory silent on
quantified clauses is not thereby wrong about them. A theory predicts an inference from a formula
when every context that accepts the formula entails it (Theory.Predicts). This is the linking
hypothesis by which a theory's acceptance conditions meet the judgments of an inference task,
stated once and shared by every task that uses it.
The accounts linglib formalizes are registered as theories by their own acceptability predicates,
from Semantics/Presupposition or the paper's study (Account.Accepts): Heim's context change
potentials with Beaver's disjunction, Peters's filtering connectives, Schlenker's Transparency,
local satisfaction, Strong Kleene and supervaluationist theories, each checked incrementally and
symmetrically, and Kalomoiros's Limited Symmetry. Schlenker's accounts also cover quantified
clauses (Account.AcceptsClause); dynamic semantics, filtering and Limited Symmetry are stated for
the propositional fragment and are silent on them. A theory under development in Lab is
scored the same way. A theory is stronger than another when every context that accepts a formula by
the first accepts it by the second, so that it predicts presuppositions at least as strong
(Theory.Stronger).
References #
When a context accepts a quantified clause, under an interpretation of its atoms as sets of world–individual pairs.
Equations
- Eval.Projection.ClauseAcceptance = ((Atom W E : Type) → (Atom → Set (W × E)) → Set W → Presupposition.QuantifiedClause Atom → Prop)
Instances For
A theory of projection says when a context accepts a formula, under an interpretation of its atoms, and, if it covers them, when a context accepts a quantified clause.
- accepts {Atom W : Type} : (Atom → Set W) → Set W → Presupposition.Formula Atom → Prop
Whether the theory accepts a formula in a context.
- acceptsClause : Option ClauseAcceptance
Whether the theory accepts a quantified clause in a context, if it covers them.
Instances For
T predicts presuppositions at least as strong as T' when every context that accepts a
formula by T accepts it by T'.
Equations
- T.Stronger T' = ∀ (Atom W : Type) (I : Atom → Set W) (C : Set W) (F : Presupposition.Formula Atom), T.accepts I C F → T'.accepts I C F
Instances For
The linking hypothesis of inference tasks. A theory predicts the inference φ from F when,
under every interpretation of the atoms, every context that accepts F entails φ, so that a
hearer who accommodates what the sentence needs draws the inference.
Instances For
A stronger theory predicts every inference that a weaker one predicts.
The accounts of projection in the propositional fragment.
- dynamic : Account
- filtering : Account
[Pet79]'s filtering connectives.
- transparencyIncremental : Account
[Sch09a]'s Transparency, over every good final.
- transparencySymmetric : Account
[Sch09a]'s Transparency, over the actual sentence.
- satisfactionIncremental : Account
[Sch09a]'s local satisfaction, over every good final.
- satisfactionSymmetric : Account
[Sch09a]'s local satisfaction, over the actual sentence.
- kleeneIncremental : Account
Strong Kleene definedness after each trigger with every good final ([Sch08e]).
- kleeneSymmetric : Account
Strong Kleene definedness of the sentence ([Sch08e]).
- supervaluationIncremental : Account
Supervaluationist definedness after each trigger with every good final ([Sch08e]).
- supervaluationSymmetric : Account
Supervaluationist definedness of the sentence ([Sch08e]).
- limitedSymmetry : Account
[Kal23]'s Limited Symmetry.
Instances For
Equations
- Eval.Projection.instDecidableEqAccount x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯
Equations
- Eval.Projection.instReprAccount = { reprPrec := Eval.Projection.instReprAccount.repr }
Equations
- One or more equations did not get rendered due to their size.
Instances For
Whether an account accepts a formula in a context, under an interpretation of the atoms, is given by the theory's own predicate.
Equations
- One or more equations did not get rendered due to their size.
- Eval.Projection.Account.dynamic.Accepts = fun (I : Atom → Set W) (C : Set W) (F : Presupposition.Formula Atom) => DynamicSemantics.PartialUpdate.Admits (Presupposition.Formula.ccp I F) C
- Eval.Projection.Account.filtering.Accepts = fun (I : Atom → Set W) (C : Set W) (F : Presupposition.Formula Atom) => C ⊆ Function.support (Presupposition.Formula.middleKleene I F)
- Eval.Projection.Account.kleeneIncremental.Accepts = fun (I : Atom → Set W) => Schlenker2009.StrongKleeneAcceptable I Schlenker2009.Version.incremental
- Eval.Projection.Account.kleeneSymmetric.Accepts = fun (I : Atom → Set W) => Schlenker2009.StrongKleeneAcceptable I Schlenker2009.Version.symmetric
- Eval.Projection.Account.supervaluationIncremental.Accepts = fun (I : Atom → Set W) => Schlenker2009.SupervaluationAcceptable I Schlenker2009.Version.incremental
- Eval.Projection.Account.supervaluationSymmetric.Accepts = fun (I : Atom → Set W) => Schlenker2009.SupervaluationAcceptable I Schlenker2009.Version.symmetric
- Eval.Projection.Account.limitedSymmetry.Accepts = fun (I : Atom → Set W) (C : Set W) (F : Presupposition.Formula Atom) => Kalomoiros2023.LimitedSymmetry C (Presupposition.Formula.occurrences I F)
Instances For
Whether an account accepts a quantified clause, for the accounts defined on them.
Equations
- One or more equations did not get rendered due to their size.
- x✝.AcceptsClause = none
Instances For
The theory an account registers.