Documentation

Eval.Projection.Map

The map of projection accounts #

The comparisons between the accounts of Eval.Projection.Account that the library proves. An edge (a, b) says that a predicts presuppositions at least as strong as b (edges, edges_sound); a cut (a, b) says that it does not, because some context accepts a formula by a and rejects it by b (cuts, cuts_sound). Every edge and cut is a theorem about the accounts' own definitions, taken from the study that proves it; a pair in neither list is open.

In the propositional fragment the incremental accounts coincide: dynamic semantics, filtering, incremental Transparency, incremental local satisfaction, and incremental Kleene and supervaluation acceptability are edges in both directions (Theorem 1, C.21 and C.22 of Local Contexts, and Theorem 36 of its manuscript). Each incremental account is stronger than its symmetric counterpart (item 20), and symmetric Kleene is stronger than symmetric supervaluation (Lemma 8). Symmetric Transparency is incomparable with symmetric Kleene and supervaluation in one direction (Theorem 39a) and supervaluation is not stronger than Kleene (Lemma 11); the symmetric accounts are not stronger than the incremental ones (Chemla and Schlenker's (13b)). Kalomoiros's Limited Symmetry lies strictly between the two Transparencies: incremental Transparency is stronger than it and it is stronger than symmetric Transparency, since the good finals it consults shrink from the incremental theory's to the sentence itself, and it is not stronger than incremental Transparency (Fact 3.4.3). Symmetric supervaluation is not stronger than Limited Symmetry (Fact 3.4.1).

References #

Edges #

theorem Eval.Projection.Account.dynamic_stronger_filtering :

dynamic.Stronger filtering

theorem Eval.Projection.Account.filtering_stronger_dynamic :

filtering.Stronger dynamic

theorem Eval.Projection.Account.transparencyIncremental_stronger_dynamic :

transparencyIncremental.Stronger dynamic

theorem Eval.Projection.Account.dynamic_stronger_transparencyIncremental :

dynamic.Stronger transparencyIncremental

theorem Eval.Projection.Account.satisfactionIncremental_stronger_transparencyIncremental :

satisfactionIncremental.Stronger transparencyIncremental

theorem Eval.Projection.Account.transparencyIncremental_stronger_satisfactionIncremental :

transparencyIncremental.Stronger satisfactionIncremental

theorem Eval.Projection.Account.satisfactionSymmetric_stronger_transparencySymmetric :

satisfactionSymmetric.Stronger transparencySymmetric

theorem Eval.Projection.Account.transparencySymmetric_stronger_satisfactionSymmetric :

transparencySymmetric.Stronger satisfactionSymmetric

theorem Eval.Projection.Account.kleeneIncremental_stronger_filtering :

kleeneIncremental.Stronger filtering

theorem Eval.Projection.Account.filtering_stronger_kleeneIncremental :

filtering.Stronger kleeneIncremental

theorem Eval.Projection.Account.supervaluationIncremental_stronger_filtering :

supervaluationIncremental.Stronger filtering

theorem Eval.Projection.Account.filtering_stronger_supervaluationIncremental :

filtering.Stronger supervaluationIncremental

theorem Eval.Projection.Account.transparencyIncremental_stronger_transparencySymmetric :

transparencyIncremental.Stronger transparencySymmetric

theorem Eval.Projection.Account.satisfactionIncremental_stronger_satisfactionSymmetric :

satisfactionIncremental.Stronger satisfactionSymmetric

theorem Eval.Projection.Account.kleeneIncremental_stronger_kleeneSymmetric :

kleeneIncremental.Stronger kleeneSymmetric

theorem Eval.Projection.Account.supervaluationIncremental_stronger_supervaluationSymmetric :

supervaluationIncremental.Stronger supervaluationSymmetric

theorem Eval.Projection.Account.kleeneSymmetric_stronger_supervaluationSymmetric :

kleeneSymmetric.Stronger supervaluationSymmetric

theorem Eval.Projection.Account.transparencyIncremental_stronger_limitedSymmetry :

transparencyIncremental.Stronger limitedSymmetry

Limited Symmetry consults at each parsing point only incremental good finals.

theorem Eval.Projection.Account.limitedSymmetry_stronger_transparencySymmetric :

limitedSymmetry.Stronger transparencySymmetric

At its last parsing point Limited Symmetry consults the sentence itself.

Cuts #

theorem Eval.Projection.Account.not_transparencySymmetric_stronger_kleeneSymmetric :

¬transparencySymmetric.Stronger kleeneSymmetric

theorem Eval.Projection.Account.not_transparencySymmetric_stronger_supervaluationSymmetric :

¬transparencySymmetric.Stronger supervaluationSymmetric

theorem Eval.Projection.Account.not_supervaluationSymmetric_stronger_kleeneSymmetric :

¬supervaluationSymmetric.Stronger kleeneSymmetric

By Lemma 11, (pp' or (not pp')) separates the two where p fails somewhere.

theorem Eval.Projection.Account.not_supervaluationSymmetric_stronger_supervaluationIncremental :

¬supervaluationSymmetric.Stronger supervaluationIncremental

theorem Eval.Projection.Account.not_kleeneSymmetric_stronger_kleeneIncremental :

¬kleeneSymmetric.Stronger kleeneIncremental

theorem Eval.Projection.Account.not_limitedSymmetry_stronger_transparencyIncremental :

¬limitedSymmetry.Stronger transparencyIncremental

By Fact 3.4.3, (pp' or q) separates the two where p fails and q holds.

theorem Eval.Projection.Account.not_supervaluationSymmetric_stronger_limitedSymmetry :

¬supervaluationSymmetric.Stronger limitedSymmetry

By Fact 3.4.1, (pp' and q) separates the two where p and q fail.

def Eval.Projection.edges :

List (Account × Account)

The comparisons the library proves, (a, b) when a is stronger than b.

Equations

One or more equations did not get rendered due to their size.

Instances For

theorem Eval.Projection.edges_sound (e : Account × Account) :

e ∈ edges → e.1.Stronger e.2

def Eval.Projection.cuts :

List (Account × Account)

The non-comparisons the library proves, (a, b) when a is not stronger than b.

Equations

One or more equations did not get rendered due to their size.

Instances For

theorem Eval.Projection.cuts_sound (c : Account × Account) :

c ∈ cuts → ¬c.1.Stronger c.2