Documentation

Linglib.Semantics.Presupposition.Formula

Formulas of the propositional fragment #

This file defines the formulas on which theories of presupposition projection are compared, the propositional fragment of the language L of Schlenker's Appendix C, which is also the language of Kalomoiros's System 1 (Definition 3.4.1). A formula is built from atoms and triggers by negation and the binary connectives of Connective; a trigger trigger p p' presupposes p and asserts p', and its classical meaning is the conjunction of the two (Formula.truth, C.2).

Each binary connective is interpreted classically (Connective.eval), by the truth table of any trivalent connectives (Connective.table), and by Heim's context change potentials, with Beaver's disjunction (Connective.ccp). The fold Formula.eval evaluates a formula into a trivalent proposition W → SignType under given connectives, the Strong Kleene ones for Formula.strongKleene and Peters' filtering ones for Formula.middleKleene, and Formula.ccp evaluates it into CCP.Partial, sending an atom or a trigger to the update of its trivalent meaning. Where the filtering evaluation is defined it is the classical meaning (Formula.middleKleene_eq_ofProp). The context change potential admits a context iff the filtering evaluation is defined throughout it, and it updates the context to its worlds at which the formula is classically true (Formula.admits_ccp_iff, Formula.ccp_get).

Main definitions #

Implementation notes #

The interpretation of the atoms is a function to Set W, and a trigger's trivalent meaning is the conditional event of its assertion on its presupposition. Schlenker's Expressivity (C.3), that every proposition is denoted by an atom, is not built in: the theories that need it quantify over propositions where the paper quantifies over expressions. The conditional is material, as in the paper, and its Strong Kleene clause is by interdefinability from negation and disjunction.

References #

Connectives #

source
def Presupposition.Connective.eval :
Connective → Prop → Prop → Prop

The classical truth function of a binary connective.

Equations
Instances For
    source
    def Presupposition.Connective.table (C : Trivalent.Connectives) :
    Connective → SignType → SignType → SignType

    The truth table that the trivalent connectives C give a binary connective.

    Equations
    Instances For
      source
      noncomputable def Presupposition.Connective.ccp {W : Type u_2} :
      Connective → DynamicSemantics.CCP.Partial W → DynamicSemantics.CCP.Partial W → DynamicSemantics.CCP.Partial W

      The dynamic connectives are [Hei83]'s conjunction and conditional and [Bea01]'s disjunction.

      Equations
      Instances For

        Formulas #

        source
        inductive Presupposition.Formula (Atom : Type u_3) :
        Type u_3

        The propositional fragment of L (C.1), in which a trigger trigger p p' presupposes p and asserts p'.

        Instances For
          source
          @[instance_reducible]
          instance Presupposition.instDecidableEqFormula {Atom✝ : Type u_3} [DecidableEq Atom✝] :
          DecidableEq (Formula Atom✝)
          Equations
          source
          def Presupposition.instDecidableEqFormula.decEq {Atom✝ : Type u_3} [DecidableEq Atom✝] (x✝ x✝¹ : Formula Atom✝) :
          Decidable (x✝ = x✝¹)
          Equations
          Instances For
            source
            def Presupposition.Formula.truth {Atom : Type u_1} {W : Type u_2} (I : Atom → Set W) :
            Formula Atom → Set W

            The classical meaning (C.2) reads a trigger as the conjunction of its two parts.

            Equations
            Instances For
              source
              noncomputable def Presupposition.Formula.eval {Atom : Type u_1} {W : Type u_2} (I : Atom → Set W) (C : Trivalent.Connectives) :
              Formula Atom → W → SignType

              The evaluation by the trivalent connectives C, in which an atom is classical and a trigger is defined where its presupposition holds.

              Equations
              Instances For
                source
                @[reducible, inline]
                noncomputable abbrev Presupposition.Formula.strongKleene {Atom : Type u_1} {W : Type u_2} (I : Atom → Set W) :
                Formula Atom → W → SignType

                The Strong Kleene evaluation.

                Equations
                Instances For
                  source
                  @[reducible, inline]
                  noncomputable abbrev Presupposition.Formula.middleKleene {Atom : Type u_1} {W : Type u_2} (I : Atom → Set W) :
                  Formula Atom → W → SignType

                  The evaluation by [Pet79]'s filtering connectives, the Middle Kleene tables.

                  Equations
                  Instances For
                    source
                    noncomputable def Presupposition.Formula.ccp {Atom : Type u_1} {W : Type u_2} (I : Atom → Set W) :
                    Formula Atom → DynamicSemantics.CCP.Partial W

                    The context change potential of a formula updates an atom or a trigger by its trivalent meaning, so a trigger is defined in a context that entails its presupposition.

                    Equations
                    Instances For
                      source
                      def Presupposition.Formula.accommodate {Atom : Type u_1} :
                      Formula Atom → Formula Atom

                      [Hei83]'s local accommodation: the presupposition of each trigger joins its assertion where the trigger is.

                      Equations
                      Instances For
                        source
                        @[simp]
                        theorem Presupposition.Formula.truth_accommodate {Atom : Type u_1} {W : Type u_2} (I : Atom → Set W) (F : Formula Atom) :
                        truth I F.accommodate = truth I F

                        Local accommodation keeps the classical meaning.

                        source
                        theorem Presupposition.Formula.middleKleene_bin_ne_zero_iff {Atom : Type u_1} {W : Type u_2} (I : Atom → Set W) {w : W} {c : Connective} {F G : Formula Atom} (hF : middleKleene I F w ≠ 0 → middleKleene I F w = SignType.ofProp (w ∈ truth I F)) :
                        middleKleene I (bin c F G) w ≠ 0 ↔ middleKleene I F w ≠ 0 ∧ (w ∈ Connective.localContext Set.univ (truth I F) c → middleKleene I G w ≠ 0)

                        The filtering evaluation of a binary formula is defined where the first argument's is, and the second's wherever the world is in the second argument's local context ([Kar74a]).

                        source
                        theorem Presupposition.Formula.middleKleene_eq_ofProp {Atom : Type u_1} {W : Type u_2} (I : Atom → Set W) {w : W} {F : Formula Atom} (h : middleKleene I F w ≠ 0) :
                        middleKleene I F w = SignType.ofProp (w ∈ truth I F)

                        Where the filtering evaluation is defined, it is the classical meaning.

                        source
                        theorem Presupposition.Formula.middleKleene_bin_ne_zero {Atom : Type u_1} {W : Type u_2} (I : Atom → Set W) {w : W} {c : Connective} {F G : Formula Atom} :
                        middleKleene I (bin c F G) w ≠ 0 ↔ middleKleene I F w ≠ 0 ∧ (w ∈ Connective.localContext Set.univ (truth I F) c → middleKleene I G w ≠ 0)

                        The filtering evaluation of a binary formula is defined where the first argument's is, and the second's wherever the world is in the second argument's local context.

                        source
                        theorem Presupposition.Formula.nonempty_atom {Atom : Type u_1} :
                        ∀ (a : Formula Atom), Nonempty Atom

                        Every formula contains an atom or a trigger.

                        source
                        theorem Presupposition.Formula.subset_support_middleKleene_bin_iff {Atom : Type u_1} {W : Type u_2} (I : Atom → Set W) {c : Connective} {F G : Formula Atom} {C : Set W} :
                        C ⊆ Function.support (middleKleene I (bin c F G)) ↔ C ⊆ Function.support (middleKleene I F) ∧ Connective.localContext C (truth I F) c ⊆ Function.support (middleKleene I G)

                        A context admits a binary formula when it admits the first argument and the second argument's local context admits the second.

                        source
                        theorem Presupposition.Formula.admits_ccp_iff {Atom : Type u_1} {W : Type u_2} (I : Atom → Set W) {F : Formula Atom} {C : Set W} :
                        DynamicSemantics.PartialUpdate.Admits (ccp I F) C ↔ C ⊆ Function.support (middleKleene I F)

                        The context change potential of a formula admits a context iff the filtering evaluation is defined throughout the context.

                        source
                        theorem Presupposition.Formula.ccp_get {Atom : Type u_1} {W : Type u_2} (I : Atom → Set W) {F : Formula Atom} {C : Set W} (h : DynamicSemantics.PartialUpdate.Admits (ccp I F) C) :
                        (ccp I F C).get h = C ∩ truth I F

                        The context change potential updates a context to its worlds at which the formula is classically true.