Documentation

Foundation.Modal.Geach

structure GeachTaple :
Instances For
    def GeachConfluent {α : Type u_1} (t : GeachTaple) (R : Rel α α) :
    Equations
    • GeachConfluent t R = ∀ {x y z : α}, R.iterate t.i x y R.iterate t.j x z∃ (u : α), R.iterate t.m y u R.iterate t.n z u
    Instances For
      theorem GeachConfluent.serial_def {α : Type u_1} {R : Rel α α} :
      Serial R GeachConfluent { i := 0, j := 0, m := 1, n := 1 } R
      theorem GeachConfluent.reflexive_def {α : Type u_1} {R : Rel α α} :
      Reflexive R GeachConfluent { i := 0, j := 0, m := 1, n := 0 } R
      theorem GeachConfluent.symmetric_def {α : Type u_1} {R : Rel α α} :
      Symmetric R GeachConfluent { i := 0, j := 1, m := 0, n := 1 } R
      theorem GeachConfluent.transitive_def {α : Type u_1} {R : Rel α α} :
      Transitive R GeachConfluent { i := 0, j := 2, m := 1, n := 0 } R
      theorem GeachConfluent.euclidean_def {α : Type u_1} {R : Rel α α} :
      Euclidean R GeachConfluent { i := 1, j := 1, m := 0, n := 1 } R
      theorem GeachConfluent.confluent_def {α : Type u_1} {R : Rel α α} :
      Confluent R GeachConfluent { i := 1, j := 1, m := 1, n := 1 } R
      theorem GeachConfluent.extensive_def {α : Type u_1} {R : Rel α α} :
      Extensive R GeachConfluent { i := 0, j := 1, m := 0, n := 0 } R
      theorem GeachConfluent.functional_def {α : Type u_1} {R : Rel α α} :
      Functional R GeachConfluent { i := 1, j := 1, m := 0, n := 0 } R
      theorem GeachConfluent.dense_def {α : Type u_1} {R : Rel α α} :
      Dense R GeachConfluent { i := 0, j := 1, m := 2, n := 0 } R
      @[simp]
      theorem GeachConfluent.satisfies_eq {α : Type u_1} {t : GeachTaple} :
      GeachConfluent t fun (x x_1 : α) => x = x_1
      @[simp]
      theorem MultiGeachConfluent.iff_nil :
      ∀ {α : Type u_1} {R : Rel α α}, MultiGeachConfluent [] R
      @[simp]
      theorem MultiGeachConfluent.iff_singleton {t : GeachTaple} :
      ∀ {α : Type u_1} {R : Rel α α}, MultiGeachConfluent [t] R GeachConfluent t R
      theorem MultiGeachConfluent.iff_cons {ts : List GeachTaple} {t : GeachTaple} :
      ∀ {α : Type u_1} {R : Rel α α}, ts [](MultiGeachConfluent (t :: ts) R GeachConfluent t R MultiGeachConfluent ts R)
      @[simp]
      theorem MultiGeachConfluent.satisfies_eq {α : Type u_1} {ts : List GeachTaple} :
      MultiGeachConfluent ts fun (x x_1 : α) => x = x_1
      @[reducible, inline]
      Equations
      Instances For
        @[reducible, inline]
        Equations
        Instances For
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            theorem LO.Axioms.Geach.T_def {F : Type u_1} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] :
            𝗴𝗲({ i := 0, j := 0, m := 1, n := 0 }) = 𝗧
            theorem LO.Axioms.Geach.B_def {F : Type u_1} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] :
            𝗴𝗲({ i := 0, j := 1, m := 0, n := 1 }) = 𝗕
            theorem LO.Axioms.Geach.D_def {F : Type u_1} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] :
            𝗴𝗲({ i := 0, j := 0, m := 1, n := 1 }) = 𝗗
            theorem LO.Axioms.Geach.Four_def {F : Type u_1} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] :
            𝗴𝗲({ i := 0, j := 2, m := 1, n := 0 }) = 𝟰
            theorem LO.Axioms.Geach.Five_def {F : Type u_1} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] :
            𝗴𝗲({ i := 1, j := 1, m := 0, n := 1 }) = 𝟱
            theorem LO.Axioms.Geach.Dot2_def {F : Type u_1} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] :
            𝗴𝗲({ i := 1, j := 1, m := 1, n := 1 }) = .𝟮
            Equations
            • LO.Axioms.instIsGeachSet = { taple := { i := 0, j := 0, m := 1, n := 0 }, char := }
            Equations
            • LO.Axioms.instIsGeachSet_1 = { taple := { i := 0, j := 1, m := 0, n := 1 }, char := }
            Equations
            • LO.Axioms.instIsGeachSet_2 = { taple := { i := 0, j := 0, m := 1, n := 1 }, char := }
            Equations
            • LO.Axioms.instIsGeachSet_3 = { taple := { i := 0, j := 2, m := 1, n := 0 }, char := }
            Equations
            • LO.Axioms.instIsGeachSet_4 = { taple := { i := 1, j := 1, m := 0, n := 1 }, char := }
            Equations
            • LO.Axioms.instIsGeachSet_5 = { taple := { i := 1, j := 1, m := 1, n := 1 }, char := }
            Equations
            • LO.Axioms.instIsGeachSet_6 = { taple := { i := 0, j := 1, m := 2, n := 0 }, char := }
            Equations
            • LO.Axioms.instIsGeachSet_7 = { taple := { i := 1, j := 1, m := 0, n := 0 }, char := }
            Equations
            • LO.Axioms.instIsGeachSet_8 = { taple := { i := 0, j := 1, m := 0, n := 0 }, char := }
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              @[reducible, inline]
              abbrev LO.Modal.Geach {α : Type u_1} (l : List GeachTaple) :
              Equations
              Instances For
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  Instances
                    @[simp]
                    theorem LO.Modal.Hilbert.IsGeach.char {α : Type u_1} {L : LO.Modal.Hilbert α} {ts : List GeachTaple} [self : L.IsGeach ts] :
                    theorem LO.Modal.IsGeach.ax {α : Type u_1} {ts : List GeachTaple} {Λ : LO.Modal.Hilbert α} [geach : Λ.IsGeach ts] :
                    instance LO.Modal.IsGeach.instIsGeachKNilGeachTaple {α : Type u_1} :
                    𝐊.IsGeach []
                    Equations
                    • LO.Modal.IsGeach.instIsGeachKNilGeachTaple = { char := }
                    instance LO.Modal.IsGeach.instIsGeachKDConsGeachTapleMkOfNatNatNil {α : Type u_1} :
                    𝐊𝐃.IsGeach [{ i := 0, j := 0, m := 1, n := 1 }]
                    Equations
                    • LO.Modal.IsGeach.instIsGeachKDConsGeachTapleMkOfNatNatNil = { char := }
                    instance LO.Modal.IsGeach.instIsGeachKTConsGeachTapleMkOfNatNatNil {α : Type u_1} :
                    𝐊𝐓.IsGeach [{ i := 0, j := 0, m := 1, n := 0 }]
                    Equations
                    • LO.Modal.IsGeach.instIsGeachKTConsGeachTapleMkOfNatNatNil = { char := }
                    instance LO.Modal.IsGeach.instIsGeachKTBConsGeachTapleMkOfNatNatNil {α : Type u_1} :
                    𝐊𝐓𝐁.IsGeach [{ i := 0, j := 0, m := 1, n := 0 }, { i := 0, j := 1, m := 0, n := 1 }]
                    Equations
                    • LO.Modal.IsGeach.instIsGeachKTBConsGeachTapleMkOfNatNatNil = { char := }
                    instance LO.Modal.IsGeach.instIsGeachK4ConsGeachTapleMkOfNatNatNil {α : Type u_1} :
                    𝐊𝟒.IsGeach [{ i := 0, j := 2, m := 1, n := 0 }]
                    Equations
                    • LO.Modal.IsGeach.instIsGeachK4ConsGeachTapleMkOfNatNatNil = { char := }
                    instance LO.Modal.IsGeach.instIsGeachS4ConsGeachTapleMkOfNatNatNil {α : Type u_1} :
                    𝐒𝟒.IsGeach [{ i := 0, j := 0, m := 1, n := 0 }, { i := 0, j := 2, m := 1, n := 0 }]
                    Equations
                    • LO.Modal.IsGeach.instIsGeachS4ConsGeachTapleMkOfNatNatNil = { char := }
                    instance LO.Modal.IsGeach.instIsGeachS4Dot2ConsGeachTapleMkOfNatNatNil {α : Type u_1} :
                    𝐒𝟒.𝟐.IsGeach [{ i := 0, j := 0, m := 1, n := 0 }, { i := 0, j := 2, m := 1, n := 0 }, { i := 1, j := 1, m := 1, n := 1 }]
                    Equations
                    • LO.Modal.IsGeach.instIsGeachS4Dot2ConsGeachTapleMkOfNatNatNil = { char := }
                    instance LO.Modal.IsGeach.instIsGeachS5ConsGeachTapleMkOfNatNatNil {α : Type u_1} :
                    𝐒𝟓.IsGeach [{ i := 0, j := 0, m := 1, n := 0 }, { i := 1, j := 1, m := 0, n := 1 }]
                    Equations
                    • LO.Modal.IsGeach.instIsGeachS5ConsGeachTapleMkOfNatNatNil = { char := }
                    instance LO.Modal.IsGeach.instIsGeachKT4BConsGeachTapleMkOfNatNatNil {α : Type u_1} :
                    𝐊𝐓𝟒𝐁.IsGeach [{ i := 0, j := 0, m := 1, n := 0 }, { i := 0, j := 2, m := 1, n := 0 }, { i := 0, j := 1, m := 0, n := 1 }]
                    Equations
                    • LO.Modal.IsGeach.instIsGeachKT4BConsGeachTapleMkOfNatNatNil = { char := }
                    instance LO.Modal.IsGeach.instIsGeachTrivConsGeachTapleMkOfNatNatNil {α : Type u_1} :
                    𝐓𝐫𝐢𝐯.IsGeach [{ i := 0, j := 0, m := 1, n := 0 }, { i := 0, j := 1, m := 0, n := 0 }]
                    Equations
                    • LO.Modal.IsGeach.instIsGeachTrivConsGeachTapleMkOfNatNatNil = { char := }