Documentation

Linglib.Semantics.Polarity.Witnesses

Model witnesses for the licensing-context table #

Each witnessed row of contextProperties carries a model operator realizing its signatures: the classical row via EntailmentSig.SoundFor, the Strawson row via EntailmentSig.StrawsonSoundFor. This converts the table's strawsonSignature/classicalSignature annotations into derived facts about denotations — the licensing analogue of the derive-don't-stipulate rule.

Coverage is incremental (contextWitness? is Option-valued): the witnessed rows are those whose operators exist in the zoo — negation (pnot), the quantifier rows (every_sem/no_sem/few_sem sections, atMost2_student), conditional antecedents (condNecessity), and the four Strawson-only rows (onlyFull, sorryFull, superlativeAssert, sinceFull). The none rows await operators (without, deny, doubt, before, too…to, the comparatives) or concern rows whose content is the licensing mechanism rather than the signature (the FC/mono rows, questions).

GroundedPolarity (in Entailment/Polarity.lean) is subsumed by this table at the polarity quotient but retains external consumers; its retirement is deferred.

source
structure Semantics.Polarity.Licensing.ContextWitness (c : LicensingContext) :
Type (max (u_1 + 1) (u_2 + 1))

A model-theoretic witness for a licensing-context row: an operator (with its definedness/presupposition function) realizing the row's Strawson signature, and its classical signature when one exists.

Instances For

    Classical rows #

    source
    def Semantics.Polarity.Licensing.negationWitness :
    ContextWitness Features.LicensingContext.negation

    Negation: pnot realizes the anti-morphism row.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def Semantics.Polarity.Licensing.universalRestrictorWitness :
      ContextWitness Features.LicensingContext.universalRestrictor

      Universal restrictor: the restrictor section of every_sem is completely anti-additive (toy scope falsifying the unit condition's vacuity).

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        noncomputable def Semantics.Polarity.Licensing.nobodyWitness :
        ContextWitness Features.LicensingContext.nobody

        Nobody: the scope section of no_sem is completely anti-additive.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          noncomputable def Semantics.Polarity.Licensing.fewWitness :
          ContextWitness Features.LicensingContext.few

          Few: the scope section of few_sem is antitone (weak DE — and not anti-additive, matching its .anti row).

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Semantics.Polarity.Licensing.atMostWitness :
            ContextWitness Features.LicensingContext.atMost

            At most n: atMost2_student is antitone; the strictness witness atMost_not_antiAdditive is why this row is .anti, not .antiAdd.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def Semantics.Polarity.Licensing.conditionalAntecedentWitness :
              ContextWitness Features.LicensingContext.conditionalAntecedent

              Conditional antecedents: the antecedent section of condNecessity is classically antitone with the modal base held constant.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For

                Strawson-only rows (classicalSignature = none) #

                source
                def Semantics.Polarity.Licensing.onlyFocusWitness :
                ContextWitness Features.LicensingContext.onlyFocus

                Only: Strawson-.anti with its existence presupposition; classically nothing (onlyFull_not_de).

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  def Semantics.Polarity.Licensing.adversativeWitness :
                  ContextWitness Features.LicensingContext.adversative

                  Adversatives: Strawson-.anti with doxastic factivity; classically nothing (sorryFull_not_de).

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    def Semantics.Polarity.Licensing.sinceTemporalWitness :
                    ContextWitness Features.LicensingContext.sinceTemporal

                    Temporal since: Strawson-.anti with the past-event presupposition.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      def Semantics.Polarity.Licensing.superlativeWitness :
                      ContextWitness Features.LicensingContext.superlative

                      Superlatives: Strawson-.anti in the restriction with the designated-subject presupposition.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For

                        The table #

                        source
                        noncomputable def Semantics.Polarity.Licensing.contextWitness? (c : LicensingContext) :
                        Option (ContextWitness c)

                        The witness table, populated incrementally; none rows are recorded in the module docstring.

                        Equations
                        Instances For