Schlenker (2009): Local Contexts #
A restriction on the denotation of an expression is transparent in a syntactic environment, relative
to a context set, when conjoining it to any denotation of the expression's type changes the truth
value at no world of the context. The local context of the expression is the least transparent
restriction, and a presupposition is satisfied when its local context entails it. Each theory has
two versions (Version): the incremental version consults every good final of the string up to the
expression, the first parsing point, and the symmetric version only the sentence itself, the last
(Version.parsingPoint). Transparency and local satisfaction check each trigger's presupposition at
that parsing point (Transparency, Satisfaction, over the occurrences of
Presupposition.Occurrence, for formulas and quantified clauses alike), and Strong Kleene and
supervaluation acceptability check the definedness of the sentences the version completes with its
finals (Version.Finals, Version.completions). This file covers the propositional fragment of the
paper's language after its Appendix C, its quantified clauses, the belief reports of its third
section, and the comparison with supervaluations and Strong Kleene logic in the appendix of
Schlenker's 2008 manuscript, which the published appendix shortens.
Main statements #
isLocalContext_incremental: the incremental local context of every position is Karttunen's, the global context except in a second argument, which takes the context updated with the first argument, or with its negation in a disjunction.satisfaction_iff_transparency,satisfaction_incremental_iff_admits: satisfaction in the local context is Transparency on either version, and on the incremental one it is admittance by Heim's context change potentials with Beaver's disjunction.isLocalContext_believe,satisfied_believe_iff_admits: the local context of the complement of believe pairs each world of the context with the worlds compatible with the agent's beliefs there, and it entails a presupposition iff the context admits the report under Heim's belief rule.strongKleeneAcceptable_iff_supervaluationAcceptable_incremental,Transparency.strongKleeneAcceptable,transparency_symmetric_not_strongKleeneAcceptable_not_supervaluationAcceptable: on the incremental version Strong Kleene and supervaluation acceptability coincide and follow from Transparency, and on the symmetric version Transparency accepts a sentence that both reject.transparent_scope_iff_universal,not_exists_isLocalContext_infinitelyMany,transparentAt_not_transparent_no: in a quantified sentence Transparency gives universal projection under Non-Triviality, the scope of infinitely many has no local context, and with no Strong Kleene accepts a sentence that Transparency rejects.QuantifiedClause.strongKleeneAcceptable_trigger_iff: a clause with a final trigger is Kleene acceptable iff the trigger is transparent at its assertion.
Implementation notes #
- The gap's denotation ranges over all propositions, where the paper quantifies over the expressions that may fill the gap and assumes that every proposition is denoted.
- The continuations a theory consults at a gap are the functions from the gap's truth set to the sentence's. For the first argument of a conjunction or a disjunction the connective follows the gap in the string and is itself free. The finals the trivalent theories complete a sentence with carry no trigger after the gap (items 26a, 29a).
- A trigger whose presupposition fails at a world may be resolved either way (
resolve). Supervaluation resolves all tokens of a trigger alike (SupervaluationDefined) and Kleene each token separately (TokenDefined), whichtokenDefined_iffshows is the Strong Kleene evaluation. On the symmetric version both evaluate the sentence itself (strongKleeneAcceptable_symmetric_iff,supervaluationAcceptable_symmetric_iff, items 26b and 29b). - The incremental Kleene and supervaluation results are proved by reducing acceptability to
entailment of the filtering presupposition (
strongKleeneAcceptable_incremental_iff,supervaluationAcceptable_incremental_iff), not by the manuscript's induction on the number of triggers. - In a quantified clause the continuations at the first parsing point after a restrictor are every predicate, by Expressivity, while the clauses Strong Kleene and supervaluation acceptability evaluate take formula scopes, which a token resolution needs.
TODO #
- Theorem 2 of C.9 is formalized for a single quantified clause, against the universal presupposition rather than a dynamic semantics for quantifiers, which linglib does not define. The conditions on quantificational clauses and domains in the equivalence with dynamic semantics hold trivially in the propositional fragment and are omitted there.
References #
Transparency and local satisfaction #
The two versions of a theory of projection: the incremental version consults every good final of the string up to an expression, and the symmetric version only the sentence itself (C.8).
Instances For
Equations
- Schlenker2009.instDecidableEqVersion x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯
The parsing point a version consults: the first, where every good final is consulted, or the last, where only the sentence itself is.
Equations
Instances For
The finals the trivalent theories complete a sentence with at the gap of K: on the
incremental version each good final without triggers (items 26a, 29a), on the symmetric version
K itself.
Equations
- Schlenker2009.Version.incremental.Finals x✝¹ x✝ = (x✝¹.SameInitialString x✝ ∧ x✝.TriggerFreeFinal)
- Schlenker2009.Version.symmetric.Finals x✝¹ x✝ = (x✝ = x✝¹)
Instances For
Transparency on a version: at every trigger the presupposition is transparent at the parsing point the version consults (C.8).
Equations
- Schlenker2009.Transparency r C os = ∀ o ∈ os, o.Transparent r.parsingPoint C
Instances For
Local satisfaction on a version: at every trigger the local context at the parsing point the version consults entails the presupposition (C.17).
Equations
- Schlenker2009.Satisfaction r C os = ∀ o ∈ os, o.Satisfied r.parsingPoint C
Instances For
Incremental Transparency implies symmetric Transparency, since the last parsing point consults fewer continuations (C.20).
Local contexts in the propositional fragment #
The incremental local context of any gap is [Kar74a]'s (C.16 with §2.3).
The first argument of a connective takes the global context, (18) and (27).
Negation is a hole, (21).
The second argument of a conjunction or a conditional takes the context updated with the first, the second disjunct the context updated with the first's negation, (24), (30) and (33).
The symmetric local context of any gap is the worlds of the context at which the truth value of the actual sentence depends on the gap.
Transparency, satisfaction and dynamic semantics #
Local satisfaction is Transparency, on either version (C.21).
Incremental satisfaction predicts presuppositions at least as strong as symmetric satisfaction (C.20).
Incremental Transparency is admittance by the formula's context change potential, which updates
the context to its worlds at which the formula is true (Formula.ccp_get; Theorem 1 of C.9).
Incremental satisfaction is admittance by the formula's context change potential (C.22).
Symmetric satisfaction requires each trigger's presupposition at the worlds of the context at which the truth value of the sentence depends on the trigger.
Examples (§2.3) #
On the incremental theory (pp' and q) and (pp' or q) presuppose p, (20).
On the incremental theory (not pp') presupposes p, (23).
On the incremental theory (if pp' . q) presupposes p, (29).
On the incremental theory (if p . qq') presupposes (if p . q), (32).
A trigger alone, and conjunction on both versions #
A trigger standing alone presupposes p on either version.
(q and pp') presupposes (if q . p) on either version, (26).
On the symmetric theory (pp' and q) presupposes (if q . p), since the local context of a
conjunct is the context updated with the other conjunct, whichever comes first.
Belief reports (§3.1.2) #
The meaning of (believe _) on two-dimensional denotations, sets of pairs of an utterance world
and a world of evaluation. The report holds at the utterance world when the complement holds at
every world compatible with the agent's beliefs there, (51).
Equations
- Schlenker2009.believe Dox = {fun (d : Set (W × W)) => {w₀ : W | ∀ w ∈ Dox w₀, (w₀, w) ∈ d}}
Instances For
The local context of the complement of believe pairs each utterance world of the context with the worlds compatible with the agent's beliefs there, (52).
The worlds of evaluation of the local context of the complement of believe are the image of the context under the doxastic accessibility, the worlds compatible with the agent's beliefs at some world of the context.
A presupposition about the world of evaluation is satisfied in the complement of believe iff every world compatible with the agent's beliefs at a world of the context satisfies it (p. 3:32).
The complement's presupposition is satisfied in the complement of believe iff the context admits the report under rule (18) of [Hei92], which the paper calls the standard result obtained in Heim's framework (p. 3:32).
For if the king has a son, the king's son is bald, incremental satisfaction is admittance by Heim's context change potential, both holding iff the context entails a king.
The classical value at w of F, at the gap K of a larger formula, when each trigger whose
presupposition fails at w takes the value ρ gives its position and its type (items 24–25).
Equations
- One or more equations did not get rendered due to their size.
- Schlenker2009.resolve I w ρ x✝ (Presupposition.Formula.atom p) = (w ∈ I p)
- Schlenker2009.resolve I w ρ x✝ (Presupposition.Formula.trigger p p') = (w ∈ I p ∧ w ∈ I p' ∨ w ∉ I p ∧ ρ x✝ p p')
- Schlenker2009.resolve I w ρ x✝ F.not = ¬Schlenker2009.resolve I w ρ (Presupposition.SyntacticEnvironment.Step.not :: x✝) F
Instances For
F is supervaluation-defined at w when every resolution of its trigger types gives it the
same value (item 25).
Equations
- One or more equations did not get rendered due to their size.
Instances For
F is Kleene-defined at w when every resolution of its trigger tokens gives it the same value
(items 27–28).
Equations
- Schlenker2009.TokenDefined I w F = ∀ (ρ ρ' : Presupposition.SyntacticEnvironment Atom → Atom → Atom → Prop), Schlenker2009.resolve I w ρ [] F ↔ Schlenker2009.resolve I w ρ' [] F
Instances For
The sentences a version evaluates: the string up to each trigger completed by each final the version consults, which on the symmetric version is the sentence itself (items 26, 29).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Strong Kleene acceptability on a version: every sentence the version evaluates has a Strong
Kleene value at every world of C, by the evaluation of item 40, which Theorem 41
(tokenDefined_iff) shows equivalent to items 27–28 (item 29).
Equations
- Schlenker2009.StrongKleeneAcceptable I r C F = ∀ w ∈ C, ∀ X ∈ r.completions F, Presupposition.Formula.strongKleene I X w ≠ 0
Instances For
Supervaluation acceptability on a version: every sentence the version evaluates is
supervaluation-defined at every world of C (item 26).
Equations
- Schlenker2009.SupervaluationAcceptable I r C F = ∀ w ∈ C, ∀ X ∈ r.completions F, Schlenker2009.SupervaluationDefined I w X
Instances For
The symmetric version evaluates the sentence itself, if it holds a trigger.
Resolutions #
A resolution of trigger types does not depend on the positions.
On its filtering presupposition, a formula takes its classical value under every resolution.
Theorem 41: Strong Kleene is supervaluation over trigger tokens #
Where the Strong Kleene evaluation is defined, every resolution of the tokens gives its value (the value half of Theorem 41).
A formula is Kleene-defined in the sense of items 27–28 iff its Strong Kleene evaluation is defined (Theorem 41).
Lemmas 6–8 and 11: Kleene and supervaluations #
Where the Strong Kleene evaluation is defined, the supervaluation is defined, with the same
value by resolve_iff_of_ne_zero (Lemma 7, item 31).
When every trigger occurs once, the supervaluation and the Strong Kleene evaluation are defined together (Lemma 6, item 30).
Strong Kleene acceptability implies supervaluation acceptability on either version (Lemma 8, item 32).
Incremental acceptability #
On its filtering presupposition, a formula's Strong Kleene evaluation is its classical value.
Incremental Strong Kleene acceptability is entailment of the filtering presupposition, the route by which Theorems 36 and 38a are proved here.
Incremental supervaluation acceptability is entailment of the filtering presupposition.
Symmetric Strong Kleene acceptability is Strong Kleene definedness of the sentence (item 29b).
Symmetric supervaluation acceptability is supervaluation definedness of the sentence (item 26b).
Incremental Strong Kleene acceptability is incremental supervaluation acceptability (Theorem 36, item 36).
As item 20 notes for every theory, incremental Strong Kleene acceptability implies symmetric Strong Kleene acceptability.
As item 20 notes for every theory, incremental supervaluation acceptability implies symmetric supervaluation acceptability.
Incremental Transparency implies incremental Strong Kleene and supervaluation acceptability (Theorem 38a, item 38).
With a world where p and q fail and one where both hold, (pp' and qq') satisfies symmetric
Transparency but is neither Strong Kleene nor supervaluation acceptable (Theorem 39a, item 39).
(pp' or (not pp')) is symmetrically supervaluation acceptable in the set of all worlds, but
not Strong Kleene acceptable there when p is not a tautology (Lemma 11, item 37).
Where q is not constant on the row of the restrictor's size at any world of the context, as
C.9's Non-Triviality and Constancy together guarantee, a presupposition triggered in the nuclear
scope is transparent iff every individual of the restrictor satisfies it at every world of the
context. This is universal projection, the consequence of Theorem 2 of C.9 for a quantified
clause.
The truth set of (Infinitely-many P. _) at a single world where every natural number is a
P, as a function of its scope.
Equations
- Schlenker2009.infinitelyMany d = {u : Unit | {n : ℕ | (u, n) ∈ d}.Infinite}
Instances For
A presupposition that fails of finitely many individuals is transparent in the scope of infinitely many, which does not then presuppose that every individual satisfies it (C.23ii).
The scope of infinitely many has no local context. Leaving out any one individual is transparent, so a least transparent restriction would contain no individual, but the empty restriction is not transparent (C.23i).
With one world and two individuals, the first not Q and the second Q and Q', the sentence
(No P. QQ') is false however the first individual is resolved, so the trigger is transparent at
its assertion and the sentence is Strong Kleene and supervaluation acceptable
(QuantifiedClause.strongKleeneAcceptable_trigger_iff), but Transparency rejects it, since for a
scope false of the second individual the first decides (Theorems 38b and 39b; the trigger is final,
so the incremental and symmetric versions coincide).
Quantified clauses #
In a clause whose scope is a trigger and whose restrictor holds none, symmetric Transparency is universal projection over the restrictor, at each world where the quantifier is not constant on the row of the restrictor's size.
Strong Kleene and supervaluations #
The value at w of a clause when each trigger token of the restrictor whose presupposition
fails of an individual takes the value ρR gives it for that individual, and each token of the
scope the value ρS gives it (items 24–25, individual by individual).
Equations
- One or more equations did not get rendered due to their size.
Instances For
A clause is Kleene-defined at w when every resolution of its trigger tokens gives it the same
value (items 27–28).
Equations
- One or more equations did not get rendered due to their size.
Instances For
A clause is supervaluation-defined at w when every resolution of its trigger types, alike for
all their tokens, gives it the same value (item 25).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The finals a version consults at the gap of a clause's environment, as Version.Finals does
for formulas: on the incremental version each good final without triggers, on the symmetric version
the environment itself.
Equations
- Schlenker2009.QuantifiedClause.Finals Schlenker2009.Version.incremental x✝¹ x✝ = (x✝¹.SameInitialString x✝ ∧ x✝.TriggerFreeFinal)
- Schlenker2009.QuantifiedClause.Finals Schlenker2009.Version.symmetric x✝¹ x✝ = (x✝ = x✝¹)
Instances For
The clauses a version evaluates: the string up to each trigger completed by each final the
version consults, as Version.completions does for formulas.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Strong Kleene acceptability of a clause on a version (item 29).
Equations
- Schlenker2009.QuantifiedClause.StrongKleeneAcceptable J r C c = ∀ w ∈ C, ∀ X ∈ Schlenker2009.QuantifiedClause.completions r c, Schlenker2009.QuantifiedClause.TokenDefined J w X
Instances For
Supervaluation acceptability of a clause on a version (item 26).
Equations
- Schlenker2009.QuantifiedClause.SupervaluationAcceptable J r C c = ∀ w ∈ C, ∀ X ∈ Schlenker2009.QuantifiedClause.completions r c, Schlenker2009.QuantifiedClause.SupervaluationDefined J w X
Instances For
A clause without triggers is Strong Kleene acceptable in every context, on either version.
A clause without triggers is supervaluation acceptable in every context, on either version.
A clause whose scope is a trigger and whose restrictor holds none is the one clause either version evaluates, since the trigger is final.
A clause whose scope is a trigger and whose restrictor holds none is Strong Kleene acceptable, on either version, iff the trigger is transparent at its assertion.
A clause whose scope is a trigger and whose restrictor holds none is supervaluation acceptable, on either version, iff the trigger is transparent at its assertion.