Documentation

LeanPool.MatchingLogic.SortedProof

MatchingLogic.SortedProof #

Free variables, at a sort #

source
def MatchingLogic.Sorted.MFV {S : MSignature} {Var : Type} {s : S.Srt} :
MPattern S Var s → Set (S.Srt × Var)

The free variables of a many-sorted pattern, paired with the sort at which they occur.

Equations
Instances For

    Application contexts, at sorts #

    source
    inductive MatchingLogic.Sorted.MAppCtx (S : MSignature) (Var : Type) :
    S.Srt → S.Srt → Type

    C ::= □ | σ(φ₁, …, C, …, φₙ), tracking both the hole's sort and the context's result sort.

    Instances For
      source
      @[irreducible]
      def MatchingLogic.Sorted.MAppCtx.plug {S : MSignature} {Var : Type} {sh st : S.Srt} :
      MAppCtx S Var sh st → MPattern S Var sh → MPattern S Var st

      C[φ].

      Equations
      Instances For

        Variable-for-variable substitution, at a sort #

        source
        def MatchingLogic.Sorted.msubstVar {S : MSignature} {Var : Type} [DecidableEq S.Srt] [DecidableEq Var] (s' : S.Srt) (x y : Var) {s : S.Srt} :
        MPattern S Var s → MPattern S Var s

        φ[y/x] where x and y are variables of sort s'. As in the one-sorted development, substitution is variable-for-variable only and capture-avoidance is a side condition rather than a renaming.

        Equations
        Instances For
          source
          def MatchingLogic.Sorted.MCaptureFree {S : MSignature} {Var : Type} (s' : S.Srt) (x y : Var) {s : S.Srt} :
          MPattern S Var s → Prop

          Capture-avoidance for msubstVar, with the same three alternatives as the one-sorted CaptureFree: the substitution stops here, or it changes nothing here, or this binder cannot capture y. The middle alternative is the one an audit had to restore in the one-sorted case.

          Equations
          Instances For

            Figure 2, many-sorted #

            source
            def MatchingLogic.Sorted.substPF {S : MSignature} {Var : Type} {s : S.Srt} (θ : ℕ → MPattern S Var s) :
            PForm → MPattern S Var s

            Propositional tautology instances, at a sort.

            Equations
            Instances For
              source
              inductive MatchingLogic.Sorted.MProvable {S : MSignature} {Var : Type} [DecidableEq S.Srt] [DecidableEq Var] {sΓ : S.Srt} (Γ : Set (MPattern S Var sΓ)) {s : S.Srt} :
              MPattern S Var s → Prop

              Γ ⊢ φ for a many-sorted theory Γ, all of whose members have sort sΓ. The rules are those of Figure 2, taken "at each symbol and each argument position", with the premise at the sort of that position and the conclusion at the symbol's result sort.

              Instances For

                Sort feeding #

                source
                def MatchingLogic.Sorted.Feeds (S : MSignature) (s t : S.Srt) :
                Prop

                s feeds t: s = t, or some symbol has an argument of sort s and result sort t (paper, Section 8).

                Equations
                Instances For
                  source
                  @[reducible, inline]
                  abbrev MatchingLogic.Sorted.FeedsStar (S : MSignature) :
                  S.Srt → S.Srt → Prop

                  ⇒, the reflexive transitive closure of Feeds.

                  Equations
                  Instances For
                    source
                    theorem MatchingLogic.Sorted.feedsStar_a_only_a (t : Srt3) :
                    FeedsStar S3 Srt3.a t → t = Srt3.a

                    In S3, sort a feeds only itself, because no symbol has an argument of sort a. This is the structural fact the whole argument rests on.

                    Many-sorted soundness, assumed as the paper does #

                    source
                    def MatchingLogic.Sorted.MSoundness (S : MSignature) (Var : Type) [DecidableEq S.Srt] [DecidableEq Var] :
                    Prop

                    (S) at many sorts. The paper cites this to [3, Thm. 13] rather than proving it; our one-sorted soundness is proved, this is not.

                    NARROWER THAN THE PAPER, deliberately: this quantifies only over HOMOGENEOUS theories, whereas the paper's many-sorted theories may mix sorts. That is exactly sufficient for Proposition 30, whose Γ is a singleton at sort a, and it keeps the induction below stated in terms of a single sΓ. An audit flagged the narrowing, so it is recorded here rather than silent.

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

                      Proposition 30, third claim #

                      source
                      theorem MatchingLogic.Sorted.mprovable_empty_of_not_feeds {S : MSignature} {Var : Type} [DecidableEq S.Srt] [DecidableEq Var] {sΓ s : S.Srt} (Γ : Set (MPattern S Var sΓ)) (φ : MPattern S Var s) (hfeed : ¬FeedsStar S sΓ s) (h : MProvable Γ φ) :
                      MProvable ∅ φ

                      Every line of a derivation whose sort does not feed back to sΓ is derivable from the axioms alone: a hypothesis line has sort sΓ, and no rule carries an sΓ premise into a conclusion of a sort that sΓ does not feed.

                      source
                      theorem MatchingLogic.Sorted.Γ3_not_derives_φ3 {Var : Type} [DecidableEq Var] (hS : MSoundness S3 Var) (x y : Var) (hxy : x ≠ y) :
                      ¬MProvable (Γ3 x y) (φ3 x y)

                      Proposition 30, third claim. Γ ⊬ φ.

                      φ has sort c, and a feeds only a, so any derivation of φ from Γ would be a derivation from no hypotheses; soundness would then make φ valid, and it is not — take M_b = {r, s} with g_M(r) ≠ g_M(s).

                      source
                      theorem MatchingLogic.Sorted.no_faithful_translation {Var : Type} [DecidableEq Var] (hS : MSoundness S3 Var) (x y : Var) (hxy : x ≠ y) :
                      ¬∃ (T : Signature) (tΓ : MPattern S3 Var Srt3.a → Pattern T Var) (tφ : MPattern S3 Var Srt3.c → Pattern T Var), StrongLocalCompleteness T Var ∧ (∀ γ ∈ Γ3 x y, Closed (tΓ γ)) ∧ Closed (tφ (φ3 x y)) ∧ (MGlobalCons (Γ3 x y) (φ3 x y) → GlobalCons (tΓ '' Γ3 x y) (tφ (φ3 x y))) ∧ (Provable (tΓ '' Γ3 x y) (tφ (φ3 x y)) → MProvable (Γ3 x y) (φ3 x y))

                      Corollary 31, at the Proposition 30 data.

                      The paper states Corollary 31 in general: "There is no translation from many-sorted definedness-free matching logic into any one-sorted definedness-free matching logic that preserves global consequence and reflects derivability." Its proof is one line — preservation, then Corollary 15 in the target, then reflection would give Γ ⊢ φ.

                      What is stated here is the counterexample instance, not the general statement: there is no target signature and pair of translations that works for the Proposition 30 data. A full rendering would define a translation on the whole source language and state preservation and reflection generally; this is the lemma that instance argument needs, and the general form is future work.

                      Three hypotheses are load-bearing and were all missing from a first draft of this statement, which an audit showed to be concretely FALSE without them:

                      • hxy : x ≠ y — without it φ3 collapses to a derivable pattern, and the existential body is inhabited;
                      • StrongLocalCompleteness T Var — (L) must hold in the target, since the paper's proof applies Corollary 15 there. A first draft required it of an unrelated fixed signature;
                      • closedness of the translated patterns, which global_completeness requires.