Documentation

Arithmetization.Definability.Hierarchy

Arithmetical Formula Sorted by Arithmetical Hierarchy #

This file defines the $\Sigma_n / \Pi_n / \Delta_n$ formulas of arithmetic of first-order logic.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    @[reducible, inline]
    Equations
    Instances For
      @[reducible, inline]
      Equations
      Instances For
        @[reducible, inline]
        Equations
        Instances For
          @[reducible, inline]
          Equations
          Instances For
            @[reducible, inline]
            Equations
            Instances For
              @[reducible, inline]
              Equations
              Instances For
                Instances For
                  @[simp]
                  theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val_mkDelta {ξ : Type u_1} {n : } {m : } (p : LO.FirstOrder.Arith.HierarchySymbol.Semiformula ξ n { Γ := 𝚺, rank := m }) (q : LO.FirstOrder.Arith.HierarchySymbol.Semiformula ξ n { Γ := 𝚷, rank := m }) :
                  (p.mkDelta q).val = p.val
                  Equations
                  • LO.FirstOrder.Arith.HierarchySymbol.Semiformula.instCoeSemisentenceSigmaZeroSemisentenceORing = { coe := LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val }
                  Equations
                  • LO.FirstOrder.Arith.HierarchySymbol.Semiformula.instCoeSemisentencePiZeroSemisentenceORing = { coe := LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val }
                  Equations
                  • LO.FirstOrder.Arith.HierarchySymbol.Semiformula.instCoeSemisentenceDeltaZeroSemisentenceORing = { coe := LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val }
                  Equations
                  • LO.FirstOrder.Arith.HierarchySymbol.Semiformula.instCoeSemisentenceSigmaOneSemisentenceORing = { coe := LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val }
                  Equations
                  • LO.FirstOrder.Arith.HierarchySymbol.Semiformula.instCoeSemisentencePiOneSemisentenceORing = { coe := LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val }
                  Equations
                  • LO.FirstOrder.Arith.HierarchySymbol.Semiformula.instCoeSemisentenceDeltaOneSemisentenceORing = { coe := LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val }
                  Equations
                  • x.sigma = match x with | p.mkDelta a => p
                  Instances For
                    @[simp]
                    theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.sigma_mkDelta {ξ : Type u_1} {n : } {m : } (p : LO.FirstOrder.Arith.HierarchySymbol.Semiformula ξ n { Γ := 𝚺, rank := m }) (q : LO.FirstOrder.Arith.HierarchySymbol.Semiformula ξ n { Γ := 𝚷, rank := m }) :
                    (p.mkDelta q).sigma = p
                    Equations
                    • x.pi = match x with | a.mkDelta p => p
                    Instances For
                      @[simp]
                      theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.pi_mkDelta {ξ : Type u_1} {n : } {m : } (p : LO.FirstOrder.Arith.HierarchySymbol.Semiformula ξ n { Γ := 𝚺, rank := m }) (q : LO.FirstOrder.Arith.HierarchySymbol.Semiformula ξ n { Γ := 𝚷, rank := m }) :
                      (p.mkDelta q).pi = q
                      theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val_sigma {ξ : Type u_1} {n : } {m : } (p : LO.FirstOrder.Arith.HierarchySymbol.Semiformula ξ n { Γ := 𝚫, rank := m }) :
                      p.sigma.val = p.val
                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        def LO.FirstOrder.Arith.HierarchySymbol.Semiformula.ProperOn {n : } (M : Type u_2) [LO.ORingStruc M] {m : } (p : { Γ := 𝚫, rank := m }.Semisentence n) :
                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              Equations
                              Instances For
                                @[simp]
                                theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.pi_emb {ξ : Type u_1} {n : } {m : } (p : LO.FirstOrder.Arith.HierarchySymbol.Semiformula ξ n { Γ := 𝚫, rank := m }) :
                                p.emb.pi = p.pi.emb
                                @[simp]
                                theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.sigma_emb {ξ : Type u_1} {n : } {m : } (p : LO.FirstOrder.Arith.HierarchySymbol.Semiformula ξ n { Γ := 𝚫, rank := m }) :
                                p.emb.sigma = p.sigma.emb
                                Equations
                                Instances For
                                  theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.sigma_extd_val {ξ : Type u_1} {n : } {m : } (p : LO.FirstOrder.Arith.HierarchySymbol.Semiformula ξ n { Γ := 𝚺, rank := m }) :
                                  p.extd.val = (LO.FirstOrder.Semiformula.lMap LO.FirstOrder.Language.oringEmb) p.val
                                  theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.pi_extd_val {ξ : Type u_1} {n : } {m : } (p : LO.FirstOrder.Arith.HierarchySymbol.Semiformula ξ n { Γ := 𝚷, rank := m }) :
                                  p.extd.val = (LO.FirstOrder.Semiformula.lMap LO.FirstOrder.Language.oringEmb) p.val
                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      @[simp]
                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        Instances For
                                          Equations
                                          • p.negDelta = p.pi.negPi.mkDelta p.sigma.negSigma
                                          Instances For
                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            Instances For
                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For
                                                Equations
                                                • LO.FirstOrder.Arith.HierarchySymbol.Semiformula.instTop = { top := LO.FirstOrder.Arith.HierarchySymbol.Semiformula.verum }
                                                Equations
                                                • LO.FirstOrder.Arith.HierarchySymbol.Semiformula.instBot = { bot := LO.FirstOrder.Arith.HierarchySymbol.Semiformula.falsum }
                                                Equations
                                                • LO.FirstOrder.Arith.HierarchySymbol.Semiformula.instWedge = { wedge := LO.FirstOrder.Arith.HierarchySymbol.Semiformula.and }
                                                Equations
                                                • LO.FirstOrder.Arith.HierarchySymbol.Semiformula.instVee = { vee := LO.FirstOrder.Arith.HierarchySymbol.Semiformula.or }
                                                Equations
                                                • LO.FirstOrder.Arith.HierarchySymbol.Semiformula.instTildeMkDeltaSigmaPiDelta = { tilde := LO.FirstOrder.Arith.HierarchySymbol.Semiformula.negDelta }
                                                Equations
                                                • LO.FirstOrder.Arith.HierarchySymbol.Semiformula.instLogicalConnectiveMkDeltaSigmaPiDelta = LO.LogicalConnective.mk
                                                Equations
                                                • LO.FirstOrder.Arith.HierarchySymbol.Semiformula.instExQuantifierMkSigmaSigmaPiDeltaHAddNatOfNat = { ex := fun {n : } => LO.FirstOrder.Arith.HierarchySymbol.Semiformula.ex }
                                                Equations
                                                • LO.FirstOrder.Arith.HierarchySymbol.Semiformula.instUnivQuantifierMkPiSigmaPiDeltaHAddNatOfNat = { univ := fun {n : } => LO.FirstOrder.Arith.HierarchySymbol.Semiformula.all }
                                                @[simp]
                                                theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.sigma_and {ξ : Type u_1} {n : } {m : } (p : LO.FirstOrder.Arith.HierarchySymbol.Semiformula ξ n { Γ := 𝚫, rank := m }) (q : LO.FirstOrder.Arith.HierarchySymbol.Semiformula ξ n { Γ := 𝚫, rank := m }) :
                                                (p q).sigma = p.sigma q.sigma
                                                @[simp]
                                                theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.pi_and {ξ : Type u_1} {n : } {m : } (p : LO.FirstOrder.Arith.HierarchySymbol.Semiformula ξ n { Γ := 𝚫, rank := m }) (q : LO.FirstOrder.Arith.HierarchySymbol.Semiformula ξ n { Γ := 𝚫, rank := m }) :
                                                (p q).pi = p.pi q.pi
                                                @[simp]
                                                theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.sigma_or {ξ : Type u_1} {n : } {m : } (p : LO.FirstOrder.Arith.HierarchySymbol.Semiformula ξ n { Γ := 𝚫, rank := m }) (q : LO.FirstOrder.Arith.HierarchySymbol.Semiformula ξ n { Γ := 𝚫, rank := m }) :
                                                (p q).sigma = p.sigma q.sigma
                                                @[simp]
                                                theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.pi_or {ξ : Type u_1} {n : } {m : } (p : LO.FirstOrder.Arith.HierarchySymbol.Semiformula ξ n { Γ := 𝚫, rank := m }) (q : LO.FirstOrder.Arith.HierarchySymbol.Semiformula ξ n { Γ := 𝚫, rank := m }) :
                                                (p q).pi = p.pi q.pi
                                                @[simp]
                                                theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val_negSigma {ξ : Type u_1} {n : } {m : } (p : LO.FirstOrder.Arith.HierarchySymbol.Semiformula ξ n { Γ := 𝚺, rank := m }) :
                                                p.negSigma.val = p.val
                                                @[simp]
                                                theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val_negPi {ξ : Type u_1} {n : } {m : } (p : LO.FirstOrder.Arith.HierarchySymbol.Semiformula ξ n { Γ := 𝚷, rank := m }) :
                                                p.negPi.val = p.val
                                                @[simp]
                                                theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.sigma_negDelta {ξ : Type u_1} {n : } {m : } (p : LO.FirstOrder.Arith.HierarchySymbol.Semiformula ξ n { Γ := 𝚫, rank := m }) :
                                                (p).sigma = p.pi.negPi
                                                @[simp]
                                                theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.sigma_negPi {ξ : Type u_1} {n : } {m : } (p : LO.FirstOrder.Arith.HierarchySymbol.Semiformula ξ n { Γ := 𝚫, rank := m }) :
                                                (p).pi = p.sigma.negSigma
                                                @[simp]
                                                theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val_exSigma {ξ : Type u_1} {n : } {m : } (p : LO.FirstOrder.Arith.HierarchySymbol.Semiformula ξ (n + 1) { Γ := 𝚺, rank := m + 1 }) :
                                                p.ex.val = ∃' p.val
                                                @[simp]
                                                theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val_allPi {ξ : Type u_1} {n : } {m : } (p : LO.FirstOrder.Arith.HierarchySymbol.Semiformula ξ (n + 1) { Γ := 𝚷, rank := m + 1 }) :
                                                p.all.val = ∀' p.val
                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                Instances For
                                                  @[simp]
                                                  theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.graphDelta_val {ξ : Type u_1} {m : } {k : } (p : LO.FirstOrder.Arith.HierarchySymbol.Semiformula ξ (k + 1) { Γ := 𝚺, rank := m }) :
                                                  p.graphDelta.val = p.val