Documentation

Foundation.FirstOrder.Basic.Calculus

@[reducible, inline]
Equations
Instances For
    inductive LO.FirstOrder.Derivation {L : Language} (T : Theory L) :
    Sequent LType u_1
    Instances For
      @[reducible, inline]
      Equations
      Instances For
        @[reducible, inline]
        Equations
        Instances For
          @[simp]
          theorem LO.FirstOrder.Derivation.length_axL {L : Language} {T : Theory L} {Δ : Sequent L} {k : } {r : L.Rel k} {v : Fin kSemiterm L 0} :
          length (axL Δ r v) = 0
          @[simp]
          @[simp]
          theorem LO.FirstOrder.Derivation.length_and {L : Language} {T : Theory L} {Δ : Sequent L} {φ ψ : SyntacticFormula L} (dp : T φ :: Δ) (dq : T ψ :: Δ) :
          length (and dp dq) = (length dp length dq).succ
          @[simp]
          theorem LO.FirstOrder.Derivation.length_or {L : Language} {T : Theory L} {Δ : Sequent L} {φ ψ : SyntacticFormula L} (d : T φ :: ψ :: Δ) :
          length (or d) = (length d).succ
          @[simp]
          theorem LO.FirstOrder.Derivation.length_all {L : Language} {T : Theory L} {Δ : Sequent L} {φ : SyntacticSemiformula L (0 + 1)} (d : T Rewriting.free φ :: Rewriting.shifts Δ) :
          length (all d) = (length d).succ
          @[simp]
          theorem LO.FirstOrder.Derivation.length_ex {L : Language} {T : Theory L} {Δ : Sequent L} {t : Semiterm L 0} {φ : SyntacticSemiformula L (Nat.succ 0)} (d : T φ/[t] :: Δ) :
          length (ex t d) = (length d).succ
          @[simp]
          theorem LO.FirstOrder.Derivation.length_wk {L : Language} {T : Theory L} {Δ Γ : Sequent L} (d : T Δ) (h : Δ Γ) :
          length (wk d h) = (length d).succ
          @[simp]
          theorem LO.FirstOrder.Derivation.length_cut {L : Language} {T : Theory L} {Δ : Sequent L} {φ : SyntacticFormula L} (dp : T φ :: Δ) (dn : T φ :: Δ) :
          length (cut dp dn) = (length dp length dn).succ
          unsafe def LO.FirstOrder.Derivation.repr {L : Language} {T : Theory L} [(k : ) → ToString (L.Func k)] [(k : ) → ToString (L.Rel k)] {Δ : Sequent L} :
          T ΔString
          Equations
          Instances For
            unsafe instance LO.FirstOrder.Derivation.instReprDerivationSyntacticFormulaTheory {L : Language} {T : Theory L} {Δ : Sequent L} [(k : ) → ToString (L.Func k)] [(k : ) → ToString (L.Rel k)] :
            Repr (T Δ)
            Equations
            @[reducible, inline]
            abbrev LO.FirstOrder.Derivation.cast {L : Language} {T : Theory L} {Δ Γ : Sequent L} (d : T Δ) (e : Δ = Γ) :
            T Γ
            Equations
            Instances For
              @[simp]
              theorem LO.FirstOrder.Derivation.cast_eq {L : Language} {T : Theory L} {Δ : Sequent L} (d : T Δ) (e : Δ = Δ) :
              @[simp]
              theorem LO.FirstOrder.Derivation.length_cast {L : Language} {T : Theory L} {Δ Γ : Sequent L} (d : T Δ) (e : Δ = Γ) :
              @[simp]
              theorem LO.FirstOrder.Derivation.length_cast' {L : Language} {T : Theory L} {Δ Γ : Sequent L} (d : T Δ) (e : Δ = Γ) :
              length (ed) = length d
              def LO.FirstOrder.Derivation.verum' {L : Language} {T : Theory L} {Δ : Sequent L} (h : Δ) :
              T Δ
              Equations
              Instances For
                def LO.FirstOrder.Derivation.axL' {L : Language} {T : Theory L} {Δ : Sequent L} {k : } (r : L.Rel k) (v : Fin kSemiterm L 0) (h : Semiformula.rel r v Δ) (hn : Semiformula.nrel r v Δ) :
                T Δ
                Equations
                Instances For
                  def LO.FirstOrder.Derivation.all' {L : Language} {T : Theory L} {Δ : Sequent L} {φ : SyntacticSemiformula L (0 + 1)} (h : ∀' φ Δ) (d : T Rewriting.free φ :: Rewriting.shifts Δ) :
                  T Δ
                  Equations
                  Instances For
                    def LO.FirstOrder.Derivation.ex' {L : Language} {T : Theory L} {Δ : Sequent L} {φ : SyntacticSemiformula L (0 + 1)} (h : ∃' φ Δ) (t : Semiterm L 0) (d : T φ/[t] :: Δ) :
                    T Δ
                    Equations
                    Instances For
                      @[simp]
                      @[simp]
                      @[irreducible]
                      def LO.FirstOrder.Derivation.em {L : Language} {T : Theory L} {Δ : Sequent L} {φ : SyntacticFormula L} (hpos : φ Δ) (hneg : φ Δ) :
                      T Δ
                      Equations
                      Instances For
                        Equations
                        • One or more equations did not get rendered due to their size.
                        Equations
                        • One or more equations did not get rendered due to their size.
                        def LO.FirstOrder.Derivation.specialize {L : Language} {T : Theory L} {Γ : Sequent L} {φ : SyntacticSemiformula L 1} (t : SyntacticTerm L) :
                        T (∀' φ) :: ΓT φ/[t] :: Γ
                        Equations
                        Instances For
                          def LO.FirstOrder.Derivation.specializes {L : Language} {T : Theory L} {k : } {φ : SyntacticSemiformula L k} {Γ : Sequent L} (v : Fin kSyntacticTerm L) :
                          T (∀* φ) :: ΓT φ v :: Γ
                          Equations
                          Instances For
                            Equations
                            • =
                            Instances For
                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                def LO.FirstOrder.Derivation.rewrite {L : Language} {T : Theory L} {Δ : List (SyntacticFormula L)} :
                                T Δ(f : SyntacticTerm L) → T List.map (fun (φ : SyntacticSemiformula L 0) => (Rewriting.app (Rew.rewrite f)) φ) Δ
                                Instances For
                                  def LO.FirstOrder.Derivation.map {L : Language} {T : Theory L} {Δ : Sequent L} (d : T Δ) (f : ) :
                                  Equations
                                  Instances For
                                    def LO.FirstOrder.Derivation.trans {L : Language} {T U : Theory L} (F : U ⊢* T) {Γ : Sequent L} :
                                    T ΓU Γ
                                    Instances For
                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Equations
                                      • =
                                      Instances For
                                        Equations
                                        • =
                                        Instances For
                                          Equations
                                          • =
                                          Instances For
                                            theorem LO.FirstOrder.Derivation.inconsistent_lMap {L₁ : Language} {L₂ : Language} {T₁ : Theory L₁} (Φ : L₁.Hom L₂) :
                                            def LO.FirstOrder.Derivation.genelalizeByNewver {L : Language} {T : Theory L} {Δ : Sequent L} {m : } {φ : SyntacticSemiformula L 1} (hp : ¬Semiformula.FVar? φ m) (hΔ : ψΔ, ¬Semiformula.FVar? ψ m) (d : T φ/[Semiterm.fvar m] :: Δ) :
                                            T (∀' φ) :: Δ
                                            Equations
                                            Instances For
                                              def LO.FirstOrder.Derivation.exOfInstances {L : Language} {T : Theory L} {Γ : Sequent L} (v : List (SyntacticTerm L)) (φ : SyntacticSemiformula L 1) (h : T List.map (fun (x : Semiterm L 0) => φ/[x]) v ++ Γ) :
                                              T (∃' φ) :: Γ
                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For
                                                def LO.FirstOrder.Derivation.allNvar {L : Language} {T : Theory L} {Δ : Sequent L} {φ : SyntacticSemiformula L (0 + 1)} (h : ∀' φ Δ) :
                                                T φ/[Semiterm.fvar (newVar Δ)] :: ΔT Δ
                                                Equations
                                                Instances For

                                                  An auxiliary structure to provide systems of provability of sentence.

                                                  Instances For
                                                    @[simp]
                                                    theorem LO.FirstOrder.Theory.alt_thy {L : Language} (T : Theory L) :
                                                    T.alt.thy = T
                                                    @[reducible, inline]
                                                    abbrev LO.FirstOrder.Provable₀ {L : Language} (T : Theory L) (σ : Sentence L) :
                                                    Equations
                                                    Instances For
                                                      @[reducible, inline]
                                                      Equations
                                                      Instances For
                                                        Equations
                                                        • One or more equations did not get rendered due to their size.
                                                        theorem LO.FirstOrder.provable₀_iff {L : Language} {T : Theory L} {σ : Sentence L} :
                                                        T ⊢!. σ T ⊢! σ
                                                        theorem LO.FirstOrder.unprovable₀_iff {L : Language} {T : Theory L} {σ : Sentence L} :
                                                        T ⊬. σ T σ