@[reducible, inline]

abbrev LO.Modal.Hilbert.Geach (α : Type u_1) (l : List GeachConfluent.Taple) : Hilbert α

Equations

• LO.Modal.Hilbert.Geach α l = LO.Modal.Hilbert.ExtK 𝗚𝗲(l)

@[reducible, inline]

abbrev LO.Modal.Hilbert.IsGeach {α : Type u_1} (L : Hilbert α) (ts : List GeachConfluent.Taple) : Prop

Equations

• L.IsGeach ts = (L = LO.Modal.Hilbert.Geach α ts)

theorem LO.Modal.Hilbert.IsGeach.ax {α : Type u_1} {ts : List GeachConfluent.Taple} {H : Hilbert α} (geach : H.IsGeach ts) : H.axioms = 𝗞 ∪ 𝗚𝗲(ts)