Documentation

Linglib.Phenomena.Presupposition.Studies.TowerDerivation

Presupposition: ContextTower Bridge #

@cite{heim-1983} @cite{karttunen-1973} @cite{schlenker-2009}

End-to-end derivation chain connecting the ContextTower infrastructure to presupposition projection phenomena via @cite{schlenker-2009}'s local context computation.

Derivation Chain #

Core.Context.Tower (ContextTower, push, depth)
    ↓
Core.Context.Shifts (attitudeShift)
    ↓
Theories.Semantics.Presupposition.LocalContext (LocalCtx, depth, filtering)
    ↓
This file: tower depth = local context depth, projection patterns
    ↓
Phenomena.Presupposition.Basic (king example, factive verbs, projection patterns)

Key Results #

  1. Tower depth = local context depth: each embedding operator increments both
  2. Negation preserves projection: tower push for negation doesn't change the context set, only depth — matching negation_preserves_projection
  3. Conditional filtering via tower: the antecedent's assertion enters the local context at tower depth 0, filtering the consequent's presupposition
  4. Belief embedding = attitudeShift: attitude verbs push a shift, creating a tower of depth 1 where OLE triggers project to the attitude holder's beliefs
source
@[reducible, inline]
abbrev Phenomena.Presupposition.Studies.TowerDerivation.PresupCtx :
Type

A presupposition context: simple KContext for tracking embedding depth. World type is KingWorld so we can connect to concrete examples.

Equations
Instances For
    source
    def Phenomena.Presupposition.Studies.TowerDerivation.speechCtx :
    PresupCtx

    Speech-act context: the world where the king exists.

    Equations
    Instances For
      source
      def Phenomena.Presupposition.Studies.TowerDerivation.rootTower :
      Core.Context.ContextTower PresupCtx

      Root tower: no embedding, depth 0.

      Equations
      Instances For
        source
        def Phenomena.Presupposition.Studies.TowerDerivation.initialLC :
        Semantics.Presupposition.LocalContext.LocalCtx KingWorld

        Initial local context at depth 0.

        Equations
        Instances For
          source
          theorem Phenomena.Presupposition.Studies.TowerDerivation.root_depths_agree :
          rootTower.depth = initialLC.depth

          Tower depth and local context depth agree at the root.

          source
          def Phenomena.Presupposition.Studies.TowerDerivation.negationShift :
          Core.Context.ContextShift PresupCtx

          A negation shift: preserves the context, increments depth. This mirrors localCtxNegation which preserves the context set but increments depth.

          Negation doesn't change what world we're evaluating in — it just wraps the embedded proposition. The tower models this as a no-op shift (like identityShift) with a depth increment.

          Equations
          Instances For
            source
            def Phenomena.Presupposition.Studies.TowerDerivation.negTower :
            Core.Context.ContextTower PresupCtx

            Tower after one negation.

            Equations
            Instances For
              source
              def Phenomena.Presupposition.Studies.TowerDerivation.negLC :
              Semantics.Presupposition.LocalContext.LocalCtx KingWorld

              Local context after one negation.

              Equations
              Instances For
                source
                theorem Phenomena.Presupposition.Studies.TowerDerivation.neg_tower_depth :
                negTower.depth = 1

                After negation, tower depth = 1.

                source
                theorem Phenomena.Presupposition.Studies.TowerDerivation.neg_lc_depth :
                negLC.depth = 1

                After negation, local context depth = 1.

                source
                theorem Phenomena.Presupposition.Studies.TowerDerivation.neg_depths_agree :
                negTower.depth = negLC.depth

                Tower depth and local context depth agree after negation.

                source
                def Phenomena.Presupposition.Studies.TowerDerivation.doubleNegTower :
                Core.Context.ContextTower PresupCtx

                Double negation: tower depth = 2 = local context depth.

                Equations
                Instances For
                  source
                  def Phenomena.Presupposition.Studies.TowerDerivation.doubleNegLC :
                  Semantics.Presupposition.LocalContext.LocalCtx KingWorld
                  Equations
                  Instances For
                    source
                    theorem Phenomena.Presupposition.Studies.TowerDerivation.double_neg_depths_agree :
                    doubleNegTower.depth = doubleNegLC.depth
                    source
                    theorem Phenomena.Presupposition.Studies.TowerDerivation.negation_preserves_context :
                    negTower.innermost = rootTower.innermost

                    Under negation, the innermost context is unchanged (identity shift). This is the tower-theoretic reason negation preserves presuppositions: the evaluation context doesn't change, only the polarity flips.

                    source
                    theorem Phenomena.Presupposition.Studies.TowerDerivation.negation_preserves_presup_phenomenon :
                    negationPattern.projects = true

                    This parallels the phenomenon: negation doesn't filter presuppositions.

                    source
                    def Phenomena.Presupposition.Studies.TowerDerivation.beliefTowerConcrete :
                    Core.Context.ContextTower PresupCtx

                    "John believes that..." pushes an attitude shift. The tower has depth 1, matching the local context depth under one belief embedding.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      theorem Phenomena.Presupposition.Studies.TowerDerivation.belief_tower_depth :
                      beliefTowerConcrete.depth = 1

                      The belief tower has depth 1.

                      source
                      theorem Phenomena.Presupposition.Studies.TowerDerivation.belief_shifts_world :
                      beliefTowerConcrete.innermost.world = KingWorld.noKing

                      Under belief embedding, the world coordinate shifts to the attitude holder's belief world. This is why presuppositions of the complement can project to the attitude holder's beliefs rather than the speaker's.

                      source
                      theorem Phenomena.Presupposition.Studies.TowerDerivation.belief_origin_preserved :
                      beliefTowerConcrete.origin.world = KingWorld.kingExists

                      The origin world is preserved — the speaker's actual world is still accessible. This matters for OLE=no triggers (expressives) which project to the speaker, not the attitude holder.

                      source
                      theorem Phenomena.Presupposition.Studies.TowerDerivation.belief_depth_matches_generic :
                      beliefTowerConcrete.depth = (Semantics.Presupposition.LocalContext.beliefTower speechCtx (Core.Context.attitudeShift () KingWorld.noKing)).depth

                      The concrete belief tower depth matches the generic beliefTower construction from LocalContext.lean. Both have depth 1.

                      source
                      theorem Phenomena.Presupposition.Studies.TowerDerivation.conditional_is_depth_zero :
                      rootTower.depth = 0

                      The conditional "If the king exists, the king is bald" is modeled as:

                      • Antecedent evaluated at depth 0 (origin)
                      • Consequent evaluated at depth 0 with updated context

                      The tower structure is flat (depth 0) because conditionals don't push a new shift — they update the local context. This matches the data: conditionals filter presuppositions, unlike negation which projects them.

                      source
                      theorem Phenomena.Presupposition.Studies.TowerDerivation.conditional_filters_phenomenon :
                      conditionalPattern.projects = false

                      Conditional filtering matches the projection pattern data.

                      source
                      theorem Phenomena.Presupposition.Studies.TowerDerivation.negation_projects_phenomenon :
                      negationPattern.projects = true

                      Negation projects (depth change, no context change).

                      source
                      theorem Phenomena.Presupposition.Studies.TowerDerivation.king_example_filtered :
                      ifKingThenBald.presup = fun (x : KingWorld) => true

                      The king example's presupposition is indeed filtered.

                      source
                      theorem Phenomena.Presupposition.Studies.TowerDerivation.projection_pattern_summary :
                      negationPattern.projects = true ∧ conditionalPattern.projects = false ∧ conjunctionPattern.projects = false ∧ disjunctionPattern.projects = false

                      The connective-specific projection patterns from Basic.lean correspond to different tower/local-context operations:

                      ConnectiveTower operationProjects?
                      Negationpush identity (depth +1)yes
                      Conditionalupdate context setno
                      Conjunctionupdate context set (L→R)no
                      Disjunctionupdate with ¬Pno

                      The key insight: projecting connectives (negation) push shifts that don't change the context set. Filtering connectives (conditional, conjunction) update the context set, potentially satisfying presuppositions of later material.