Documentation

Linglib.Phenomena.Presupposition.Studies.Yagi2025

source
inductive Phenomena.Presupposition.Studies.Yagi2025.W :
Type

Possible states for the Buganda scenario.

  • kingOpens : W
  • kingDoesnt : W
  • presidentConducts : W
  • presidentDoesnt : W
Instances For
    source
    instance Phenomena.Presupposition.Studies.Yagi2025.instDecidableEqW :
    DecidableEq W
    Equations
    source
    instance Phenomena.Presupposition.Studies.Yagi2025.instReprW :
    Repr W
    Equations
    source
    def Phenomena.Presupposition.Studies.Yagi2025.instReprW.repr :
    W → ℕ → Std.Format
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      instance Phenomena.Presupposition.Studies.Yagi2025.instInhabitedW :
      Inhabited W
      Equations
      source
      def Phenomena.Presupposition.Studies.Yagi2025.instInhabitedW.default :
      W
      Equations
      Instances For
        source
        instance Phenomena.Presupposition.Studies.Yagi2025.instFiniteWorldsW :
        Core.Proposition.FiniteWorlds W
        Equations
        • One or more equations did not get rendered due to their size.
        source
        def Phenomena.Presupposition.Studies.Yagi2025.hasKing :
        BProp W

        Presupposition p: the nation has a king.

        Equations
        Instances For
          source
          def Phenomena.Presupposition.Studies.Yagi2025.hasPresident :
          BProp W

          Presupposition q: the nation has a president.

          Equations
          Instances For
            source
            theorem Phenomena.Presupposition.Studies.Yagi2025.presups_conflict (w : W) :
            ¬(hasKing w = true ∧ hasPresident w = true)

            p ∧ q = ⊥: the presuppositions conflict.

            source
            def Phenomena.Presupposition.Studies.Yagi2025.kingOpensParl :
            Core.Presupposition.PrProp W

            φ_p: "The King is opening parliament" — presupposes hasKing.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def Phenomena.Presupposition.Studies.Yagi2025.presConductsCeremony :
              Core.Presupposition.PrProp W

              ψ_q: "The President is conducting the ceremony" — presupposes hasPresident.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                def Phenomena.Presupposition.Studies.Yagi2025.expectedPresup :
                BProp W

                The expected presupposition: the nation has some head of state.

                Equations
                Instances For
                  source
                  theorem Phenomena.Presupposition.Studies.Yagi2025.presup_universal (w : W) :
                  expectedPresup w = true

                  Observation (2a): the presupposition p ∨ q holds at every world.

                  source
                  theorem Phenomena.Presupposition.Studies.Yagi2025.can_be_false :
                  expectedPresup W.kingDoesnt = true ∧ kingOpensParl.assertion W.kingDoesnt = false ∧ presConductsCeremony.assertion W.kingDoesnt = false

                  Observation (2b): the disjunction can be false. At kingDoesnt the presupposition is satisfied but both disjuncts fail.

                  source
                  def Phenomena.Presupposition.Studies.Yagi2025.skDisj :
                  Core.Duality.Prop3 W

                  Strong Kleene disjunction of the two presuppositional propositions.

                  Equations
                  Instances For
                    source
                    theorem Phenomena.Presupposition.Studies.Yagi2025.strong_kleene_never_false (w : W) :
                    skDisj w ≠ Core.Duality.Truth3.false

                    Strong Kleene never produces false for this disjunction. Because presuppositions conflict, at least one disjunct is always undefined, so the table never reaches the 0 ∨ 0 = 0 row.

                    source
                    def Phenomena.Presupposition.Studies.Yagi2025.classicalDisj :
                    Core.Presupposition.PrProp W

                    Classical disjunction requires both presuppositions: presup = p ∧ q.

                    Equations
                    Instances For
                      source
                      theorem Phenomena.Presupposition.Studies.Yagi2025.classical_never_defined (w : W) :
                      classicalDisj.presup w = false

                      PrProp.or is never defined when presuppositions conflict.

                      source
                      def Phenomena.Presupposition.Studies.Yagi2025.filterDisj :
                      Core.Presupposition.PrProp W

                      Filtering disjunction (Heim/Schlenker-style symmetric filtering).

                      Equations
                      Instances For
                        source
                        theorem Phenomena.Presupposition.Studies.Yagi2025.filter_wrong_at_kingOpens :
                        filterDisj.presup W.kingOpens = false

                        orFilter predicts presupposition failure at kingOpens, where the disjunction should clearly be true. The filtering condition demands the second presupposition hold when the first assertion is true.

                        source
                        theorem Phenomena.Presupposition.Studies.Yagi2025.expected_satisfied_at_kingOpens :
                        expectedPresup W.kingOpens = true

                        But the expected presupposition IS satisfied there.

                        source
                        def Phenomena.Presupposition.Studies.Yagi2025.flexDisj :
                        Core.Presupposition.PrProp W

                        The flexible accommodation disjunction.

                        Equations
                        Instances For
                          source
                          theorem Phenomena.Presupposition.Studies.Yagi2025.flex_correct_presup :
                          flexDisj.presup = expectedPresup

                          Flexible accommodation gives the correct presupposition p ∨ q.

                          source
                          theorem Phenomena.Presupposition.Studies.Yagi2025.flex_truth_table :
                          flexDisj.eval W.kingOpens = Core.Duality.Truth3.true ∧ flexDisj.eval W.kingDoesnt = Core.Duality.Truth3.false ∧ flexDisj.eval W.presidentConducts = Core.Duality.Truth3.true ∧ flexDisj.eval W.presidentDoesnt = Core.Duality.Truth3.false

                          Complete truth table: flexible accommodation predicts the right value at every world.

                          source
                          theorem Phenomena.Presupposition.Studies.Yagi2025.flex_always_defined (w : W) :
                          flexDisj.eval w ≠ Core.Duality.Truth3.indet

                          Flexible accommodation is always defined (never undefined).

                          source
                          def Phenomena.Presupposition.Studies.Yagi2025.metaAssertDisj :
                          Core.Duality.Prop3 W

                          Weak Kleene disjunction with meta-assertion on each disjunct.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            source
                            theorem Phenomena.Presupposition.Studies.Yagi2025.metaAssert_allows_falsity :
                            metaAssertDisj W.kingDoesnt = Core.Duality.Truth3.false

                            Meta-assertion allows falsity (unlike Strong Kleene).

                            source
                            theorem Phenomena.Presupposition.Studies.Yagi2025.metaAssert_loses_presup :
                            metaAssertDisj W.kingDoesnt = Core.Duality.Truth3.false

                            But meta-assertion loses the presupposition: the disjunction is false even when neither presupposition holds (if we had such a world). More concretely, 𝒜φ_p ∨_s ψ_q presupposes only ¬𝒜ψ_q → p (Yagi (11)), not the expected p ∨ q.