Documentation

Foundation.Modal.Hilbert.Geach

source
@[reducible, inline]
abbrev LO.Modal.Hilbert.Geach (α : Type u_1) (l : List GeachConfluent.Taple) :
LO.Modal.Hilbert α
Equations
Instances For
    source
    @[reducible, inline]
    abbrev LO.Modal.Hilbert.IsGeach {α : Type u_1} (L : LO.Modal.Hilbert α) (ts : List GeachConfluent.Taple) :
    Prop
    Equations
    Instances For
      source
      theorem LO.Modal.Hilbert.IsGeach.ax {α : Type u_1} {ts : List GeachConfluent.Taple} {H : LO.Modal.Hilbert α} (geach : H.IsGeach ts) :
      H.axioms = 𝗞 ∪ 𝗚𝗲(ts)