Documentation

Foundation.Logic.HilbertStyle.Context

structure LO.System.FiniteContext (F : Type u_1) {S : Type u_2} (𝓢 : S) :
Type u_1
Instances For
    instance LO.System.FiniteContext.instCoeList {F : Type u_1} {S : Type u_2} {𝓢 : S} :
    Equations
    • LO.System.FiniteContext.instCoeList = { coe := LO.System.FiniteContext.mk }
    @[reducible, inline]
    abbrev LO.System.FiniteContext.conj {F : Type u_1} [LO.LogicalConnective F] {S : Type u_2} {𝓢 : S} (Γ : LO.System.FiniteContext F 𝓢) :
    F
    Equations
    Instances For
      @[reducible, inline]
      abbrev LO.System.FiniteContext.disj {F : Type u_1} [LO.LogicalConnective F] {S : Type u_2} {𝓢 : S} (Γ : LO.System.FiniteContext F 𝓢) :
      F
      Equations
      Instances For
        Equations
        • LO.System.FiniteContext.instEmptyCollection = { emptyCollection := { ctx := [] } }
        instance LO.System.FiniteContext.instMembership {F : Type u_1} {S : Type u_2} {𝓢 : S} :
        Equations
        instance LO.System.FiniteContext.instHasSubset {F : Type u_1} {S : Type u_2} {𝓢 : S} :
        Equations
        instance LO.System.FiniteContext.instCons {F : Type u_1} {S : Type u_2} {𝓢 : S} :
        Equations
        theorem LO.System.FiniteContext.mem_def {F : Type u_1} {S : Type u_2} {𝓢 : S} {p : F} {Γ : LO.System.FiniteContext F 𝓢} :
        p Γ p Γ.ctx
        @[simp]
        theorem LO.System.FiniteContext.coe_subset_coe_iff {F : Type u_1} {S : Type u_2} {𝓢 : S} {Γ : List F} {Δ : List F} :
        { ctx := Γ } { ctx := Δ } Γ Δ
        @[simp]
        theorem LO.System.FiniteContext.mem_coe_iff {F : Type u_1} {S : Type u_2} {𝓢 : S} {p : F} {Γ : List F} :
        p { ctx := Γ } p Γ
        @[simp]
        theorem LO.System.FiniteContext.not_mem_empty {F : Type u_1} {S : Type u_2} {𝓢 : S} (p : F) :
        p
        instance LO.System.FiniteContext.instCollection {F : Type u_1} {S : Type u_2} {𝓢 : S} :
        Equations
        instance LO.System.FiniteContext.inst {F : Type u_1} [LO.LogicalConnective F] {S : Type u_2} [LO.System F S] (𝓢 : S) :
        Equations
        @[reducible, inline]
        abbrev LO.System.FiniteContext.Prf {F : Type u_1} [LO.LogicalConnective F] {S : Type u_2} [LO.System F S] (𝓢 : S) (Γ : List F) (p : F) :
        Type u_3
        Equations
        Instances For
          @[reducible, inline]
          abbrev LO.System.FiniteContext.Provable {F : Type u_1} [LO.LogicalConnective F] {S : Type u_2} [LO.System F S] (𝓢 : S) (Γ : List F) (p : F) :
          Equations
          Instances For
            @[reducible, inline]
            abbrev LO.System.FiniteContext.Unprovable {F : Type u_1} [LO.LogicalConnective F] {S : Type u_2} [LO.System F S] (𝓢 : S) (Γ : List F) (p : F) :
            Equations
            Instances For
              @[reducible, inline]
              abbrev LO.System.FiniteContext.PrfSet {F : Type u_1} [LO.LogicalConnective F] {S : Type u_2} [LO.System F S] (𝓢 : S) (Γ : List F) (s : Set F) :
              Type (max u_3 u_1)
              Equations
              Instances For
                @[reducible, inline]
                abbrev LO.System.FiniteContext.ProvableSet {F : Type u_1} [LO.LogicalConnective F] {S : Type u_2} [LO.System F S] (𝓢 : S) (Γ : List F) (s : Set F) :
                Equations
                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
                      • 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
                            theorem LO.System.FiniteContext.system_def {F : Type u_1} [LO.LogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} (Γ : LO.System.FiniteContext F 𝓢) (p : F) :
                            (Γ p) = (𝓢 Γ.conj p)
                            def LO.System.FiniteContext.ofDef {F : Type u_1} [LO.LogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} {Γ : List F} {p : F} (b : 𝓢 Γ p) :
                            Γ ⊢[𝓢] p
                            Equations
                            Instances For
                              def LO.System.FiniteContext.toDef {F : Type u_1} [LO.LogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} {Γ : List F} {p : F} (b : Γ ⊢[𝓢] p) :
                              𝓢 Γ p
                              Equations
                              Instances For
                                theorem LO.System.FiniteContext.toₛ! {F : Type u_1} [LO.LogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} {Γ : List F} {p : F} (b : Γ ⊢[𝓢]! p) :
                                𝓢 ⊢! Γ p
                                theorem LO.System.FiniteContext.provable_iff {F : Type u_1} [LO.LogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} {Γ : List F} {p : F} :
                                Γ ⊢[𝓢]! p 𝓢 ⊢! Γ p
                                Equations
                                • One or more equations did not get rendered due to their size.
                                def LO.System.FiniteContext.of {F : Type u_1} [LO.LogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} {Γ : List F} [LO.System.ModusPonens 𝓢] [LO.System.HasAxiomImply₁ 𝓢] {p : F} (b : 𝓢 p) :
                                Γ ⊢[𝓢] p
                                Equations
                                Instances For
                                  def LO.System.FiniteContext.emptyPrf {F : Type u_1} [LO.LogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.ModusPonens 𝓢] [LO.System.HasAxiomVerum 𝓢] {p : F} :
                                  [] ⊢[𝓢] p𝓢 p
                                  Equations
                                  Instances For
                                    Equations
                                    • =
                                    Instances For
                                      Equations
                                      Instances For
                                        Equations
                                        Instances For
                                          Equations
                                          Instances For
                                            Equations
                                            • Γ.instModusPonens = { mdp := fun {p q : F} => LO.System.mdp₁ }
                                            Equations
                                            Equations
                                            Equations
                                            Equations
                                            Equations
                                            Equations
                                            Equations
                                            Equations
                                            Equations
                                            Equations
                                            def LO.System.FiniteContext.mdp' {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} {Γ : List F} {Δ : List F} [LO.System.ModusPonens 𝓢] [LO.System.HasAxiomVerum 𝓢] [LO.System.HasAxiomImply₁ 𝓢] [LO.System.HasAxiomImply₂ 𝓢] [LO.System.HasAxiomAndElim₁ 𝓢] [LO.System.HasAxiomAndElim₂ 𝓢] [LO.System.HasAxiomAndInst 𝓢] {p : F} {q : F} (bΓ : Γ ⊢[𝓢] p q) (bΔ : Δ ⊢[𝓢] p) :
                                            (Γ ++ Δ) ⊢[𝓢] q
                                            Equations
                                            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
                                                  • One or more equations did not get rendered due to their size.
                                                  Equations
                                                  Equations
                                                  • LO.System.FiniteContext.instDeductiveExplosionOfHasAxiomEFQ = inferInstance
                                                  structure LO.System.Context (F : Type u_1) {S : Type u_2} (𝓢 : S) :
                                                  Type u_1
                                                  Instances For
                                                    instance LO.System.Context.instCoeSet {F : Type u_1} {S : Type u_2} {𝓢 : S} :
                                                    Equations
                                                    • LO.System.Context.instCoeSet = { coe := LO.System.Context.mk }
                                                    instance LO.System.Context.instEmptyCollection {F : Type u_1} {S : Type u_2} {𝓢 : S} :
                                                    Equations
                                                    • LO.System.Context.instEmptyCollection = { emptyCollection := { ctx := } }
                                                    instance LO.System.Context.instMembership {F : Type u_1} {S : Type u_2} {𝓢 : S} :
                                                    Equations
                                                    • LO.System.Context.instMembership = { mem := fun (x : F) (x_1 : LO.System.Context F 𝓢) => x x_1.ctx }
                                                    instance LO.System.Context.instHasSubset {F : Type u_1} {S : Type u_2} {𝓢 : S} :
                                                    Equations
                                                    • LO.System.Context.instHasSubset = { Subset := fun (x x_1 : LO.System.Context F 𝓢) => x.ctx x_1.ctx }
                                                    instance LO.System.Context.instCons {F : Type u_1} {S : Type u_2} {𝓢 : S} :
                                                    Equations
                                                    theorem LO.System.Context.mem_def {F : Type u_1} {S : Type u_2} {𝓢 : S} {p : F} {Γ : LO.System.Context F 𝓢} :
                                                    p Γ p Γ.ctx
                                                    @[simp]
                                                    theorem LO.System.Context.coe_subset_coe_iff {F : Type u_1} {S : Type u_2} {𝓢 : S} {Γ : Set F} {Δ : Set F} :
                                                    { ctx := Γ } { ctx := Δ } Γ Δ
                                                    @[simp]
                                                    theorem LO.System.Context.mem_coe_iff {F : Type u_1} {S : Type u_2} {𝓢 : S} {p : F} {Γ : Set F} :
                                                    p { ctx := Γ } p Γ
                                                    @[simp]
                                                    theorem LO.System.Context.not_mem_empty {F : Type u_1} {S : Type u_2} {𝓢 : S} (p : F) :
                                                    p
                                                    instance LO.System.Context.instCollection {F : Type u_1} {S : Type u_2} {𝓢 : S} :
                                                    Equations
                                                    structure LO.System.Context.Proof {F : Type u_1} [LO.LogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} (Γ : LO.System.Context F 𝓢) (p : F) :
                                                    Type (max u_1 u_3)
                                                    • ctx : List F
                                                    • subset : qself.ctx, q Γ
                                                    • prf : self.ctx ⊢[𝓢] p
                                                    Instances For
                                                      theorem LO.System.Context.Proof.subset {F : Type u_1} [LO.LogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} {Γ : LO.System.Context F 𝓢} {p : F} (self : Γ.Proof p) (q : F) :
                                                      q self.ctxq Γ
                                                      instance LO.System.Context.inst {F : Type u_1} [LO.LogicalConnective F] {S : Type u_2} [LO.System F S] (𝓢 : S) :
                                                      Equations
                                                      @[reducible, inline]
                                                      abbrev LO.System.Context.Prf {F : Type u_1} [LO.LogicalConnective F] {S : Type u_2} [LO.System F S] (𝓢 : S) (Γ : Set F) (p : F) :
                                                      Type (max u_1 u_3)
                                                      Equations
                                                      Instances For
                                                        @[reducible, inline]
                                                        abbrev LO.System.Context.Provable {F : Type u_1} [LO.LogicalConnective F] {S : Type u_2} [LO.System F S] (𝓢 : S) (Γ : Set F) (p : F) :
                                                        Equations
                                                        Instances For
                                                          @[reducible, inline]
                                                          abbrev LO.System.Context.Unprovable {F : Type u_1} [LO.LogicalConnective F] {S : Type u_2} [LO.System F S] (𝓢 : S) (Γ : Set F) (p : F) :
                                                          Equations
                                                          Instances For
                                                            @[reducible, inline]
                                                            abbrev LO.System.Context.PrfSet {F : Type u_1} [LO.LogicalConnective F] {S : Type u_2} [LO.System F S] (𝓢 : S) (Γ : Set F) (s : Set F) :
                                                            Type (max u_1 u_3)
                                                            Equations
                                                            Instances For
                                                              @[reducible, inline]
                                                              abbrev LO.System.Context.ProvableSet {F : Type u_1} [LO.LogicalConnective F] {S : Type u_2} [LO.System F S] (𝓢 : S) (Γ : Set F) (s : Set F) :
                                                              Equations
                                                              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
                                                                    • 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
                                                                          theorem LO.System.Context.provable_iff {F : Type u_1} [LO.LogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} {Γ : Set F} {p : F} :
                                                                          Γ *⊢[𝓢]! p ∃ (Δ : List F), (qΔ, q Γ) Δ ⊢[𝓢]! p
                                                                          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.System.Context.deduct {F : Type u_1} [LO.LogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] [DecidableEq F] {p : F} {q : F} {Γ : Set F} :
                                                                          insert p Γ *⊢[𝓢] qΓ *⊢[𝓢] p q
                                                                          Equations
                                                                          • One or more equations did not get rendered due to their size.
                                                                          Instances For
                                                                            def LO.System.Context.deductInv {F : Type u_1} [LO.LogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} {Γ : Set F} :
                                                                            Γ *⊢[𝓢] p qinsert p Γ *⊢[𝓢] q
                                                                            Equations
                                                                            Instances For
                                                                              Equations
                                                                              • One or more equations did not get rendered due to their size.
                                                                              def LO.System.Context.of {F : Type u_1} [LO.LogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {Γ : Set F} {p : F} (b : 𝓢 p) :
                                                                              Γ *⊢[𝓢] p
                                                                              Equations
                                                                              Instances For
                                                                                theorem LO.System.Context.of! {F : Type u_1} [LO.LogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {Γ : Set F} (b : 𝓢 ⊢! p) :
                                                                                Γ *⊢[𝓢]! p
                                                                                def LO.System.Context.mdp {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {q : F} {Γ : Set F} (bpq : Γ *⊢[𝓢] p q) (bp : Γ *⊢[𝓢] p) :
                                                                                Γ *⊢[𝓢] q
                                                                                Equations
                                                                                Instances For
                                                                                  theorem LO.System.Context.by_axm! {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {Γ : Set F} (h : p Γ) :
                                                                                  Γ *⊢[𝓢]! p
                                                                                  def LO.System.Context.emptyPrf {F : Type u_1} [LO.LogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} :
                                                                                  *⊢[𝓢] p𝓢 p
                                                                                  Equations
                                                                                  • One or more equations did not get rendered due to their size.
                                                                                  Instances For
                                                                                    theorem LO.System.Context.emptyPrf! {F : Type u_1} [LO.LogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} :
                                                                                    *⊢[𝓢]! p𝓢 ⊢! p
                                                                                    theorem LO.System.Context.provable_iff_provable {F : Type u_1} [LO.LogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} :
                                                                                    𝓢 ⊢! p *⊢[𝓢]! p
                                                                                    instance LO.System.Context.minimal {F : Type u_1} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] (Γ : LO.System.Context F 𝓢) :
                                                                                    Equations
                                                                                    • Γ.minimal = LO.System.Minimal.mk
                                                                                    Equations
                                                                                    Equations
                                                                                    Equations
                                                                                    • LO.System.Context.instDeductiveExplosionFiniteContextOfHasAxiomEFQ = inferInstance
                                                                                    Equations
                                                                                    • Γ.instIntuitionistic = LO.System.Intuitionistic.mk
                                                                                    Equations
                                                                                    • Γ.instClassical = LO.System.Classical.mk