Documentation

Foundation.Modal.Kripke.Geach.Systems

source
instance LO.Modal.Hilbert.KD.Kripke.sound :
Sound (Hilbert.KD ℕ) Kripke.SerialFrameClass
source
instance LO.Modal.Hilbert.KD.consistent :
System.Consistent (Hilbert.KD ℕ)
source
instance LO.Modal.Hilbert.KT.Kripke.sound :
Sound (Hilbert.KT ℕ) Kripke.ReflexiveFrameClass
source
instance LO.Modal.Hilbert.KT.consistent :
System.Consistent (Hilbert.KT ℕ)
source
instance LO.Modal.Hilbert.KT.Kripke.complete :
Complete (Hilbert.KT ℕ) Kripke.ReflexiveFrameClass
source
instance LO.Modal.Hilbert.KB.Kripke.sound :
Sound (Hilbert.KB ℕ) Kripke.SymmetricFrameClass
source
instance LO.Modal.Hilbert.KB.consistent :
System.Consistent (Hilbert.KB ℕ)
source
instance LO.Modal.Hilbert.KB.Kripke.complete :
Complete (Hilbert.KB ℕ) Kripke.SymmetricFrameClass
source
instance LO.Modal.Hilbert.KTB.Kripke.sound :
Sound (Hilbert.KTB ℕ) Kripke.ReflexiveSymmetricFrameClass
source
instance LO.Modal.Hilbert.KTB.consistent :
System.Consistent (Hilbert.KTB ℕ)
source
instance LO.Modal.Hilbert.KTB.Kripke.complete :
Complete (Hilbert.KTB ℕ) Kripke.ReflexiveSymmetricFrameClass
source
instance LO.Modal.Hilbert.K4.Kripke.sound :
Sound (Hilbert.K4 ℕ) Kripke.TransitiveFrameClass
source
instance LO.Modal.Hilbert.K4.consistent :
System.Consistent (Hilbert.K4 ℕ)
source
instance LO.Modal.Hilbert.K4.Kripke.complete :
Complete (Hilbert.K4 ℕ) Kripke.TransitiveFrameClass
source
instance LO.Modal.Hilbert.K5.Kripke.sound :
Sound (Hilbert.K5 ℕ) Kripke.EuclideanFrameClass
source
instance LO.Modal.Hilbert.K5.consistent :
System.Consistent (Hilbert.K5 ℕ)
source
instance LO.Modal.Hilbert.K5.Kripke.complete :
Complete (Hilbert.K5 ℕ) Kripke.EuclideanFrameClass
source
instance LO.Modal.Hilbert.S4.Kripke.sound :
Sound (Hilbert.S4 ℕ) Kripke.ReflexiveTransitiveFrameClass
source
instance LO.Modal.Hilbert.S4.consistent :
System.Consistent (Hilbert.S4 ℕ)
source
instance LO.Modal.Hilbert.S4.Kripke.complete :
Complete (Hilbert.S4 ℕ) Kripke.ReflexiveTransitiveFrameClass
source
instance LO.Modal.Hilbert.S5.Kripke.sound :
Sound (Hilbert.S5 ℕ) Kripke.ReflexiveEuclideanFrameClass
source
instance LO.Modal.Hilbert.S5.consistent :
System.Consistent (Hilbert.S5 ℕ)
source
instance LO.Modal.Hilbert.S5.Kripke.complete :
Complete (Hilbert.S5 ℕ) Kripke.ReflexiveEuclideanFrameClass
source
instance LO.Modal.Hilbert.KT4B.Kripke.sound :
Sound (Hilbert.KT4B ℕ) Kripke.ReflexiveTransitiveSymmetricFrameClass
source
instance LO.Modal.Hilbert.KT4B.consistent :
System.Consistent (Hilbert.KT4B ℕ)
source
instance LO.Modal.Hilbert.KT4B.Kripke.complete :
Complete (Hilbert.KT4B ℕ) Kripke.ReflexiveTransitiveSymmetricFrameClass
source
instance LO.Modal.Hilbert.KD45.Kripke.sound :
Sound (Hilbert.KD45 ℕ) Kripke.SerialTransitiveEuclideanFrameClass
source
instance LO.Modal.Hilbert.KD45.consistent :
System.Consistent (Hilbert.KD45 ℕ)
source
instance LO.Modal.Hilbert.KD45.Kripke.complete :
Complete (Hilbert.KD45 ℕ) Kripke.SerialTransitiveEuclideanFrameClass
source
instance LO.Modal.Hilbert.K45.Kripke.sound :
Sound (Hilbert.K45 ℕ) Kripke.TransitiveEuclideanFrameClass
source
instance LO.Modal.Hilbert.K45.consistent :
System.Consistent (Hilbert.K45 ℕ)
source
instance LO.Modal.Hilbert.K45.Kripke.complete :
Complete (Hilbert.K45 ℕ) Kripke.TransitiveEuclideanFrameClass
source
instance LO.Modal.Hilbert.KB4.Kripke.sound :
Sound (Hilbert.KB4 ℕ) Kripke.SymmetricTransitiveFrameClass
source
instance LO.Modal.Hilbert.KB4.consistent :
System.Consistent (Hilbert.KB4 ℕ)
source
instance LO.Modal.Hilbert.KB4.Kripke.complete :
Complete (Hilbert.KB4 ℕ) Kripke.SymmetricTransitiveFrameClass
source
instance LO.Modal.Hilbert.KB5.Kripke.sound :
Sound (Hilbert.KB5 ℕ) Kripke.SymmetricEuclideanFrameClass
source
instance LO.Modal.Hilbert.KB5.consistent :
System.Consistent (Hilbert.KB5 ℕ)
source
instance LO.Modal.Hilbert.KB5.Kripke.complete :
Complete (Hilbert.KB5 ℕ) Kripke.SymmetricEuclideanFrameClass
source
instance LO.Modal.Hilbert.KDB.Kripke.sound :
Sound (Hilbert.KDB ℕ) Kripke.SerialSymmetricFrameClass
source
instance LO.Modal.Hilbert.KDB.consistent :
System.Consistent (Hilbert.KDB ℕ)
source
instance LO.Modal.Hilbert.KDB.Kripke.complete :
Complete (Hilbert.KDB ℕ) Kripke.SerialSymmetricFrameClass
source
instance LO.Modal.Hilbert.KD4.Kripke.sound :
Sound (Hilbert.KD4 ℕ) Kripke.SerialTransitiveFrameClass
source
instance LO.Modal.Hilbert.KD4.consistent :
System.Consistent (Hilbert.KD4 ℕ)
source
instance LO.Modal.Hilbert.KD4.Kripke.complete :
Complete (Hilbert.KD4 ℕ) Kripke.SerialTransitiveFrameClass
source
instance LO.Modal.Hilbert.KD5.Kripke.sound :
Sound (Hilbert.KD5 ℕ) Kripke.SerialEuclideanFrameClass
source
instance LO.Modal.Hilbert.KD5.consistent :
System.Consistent (Hilbert.KD5 ℕ)
source
instance LO.Modal.Hilbert.KD5.Kripke.complete :
Complete (Hilbert.KD5 ℕ) Kripke.SerialEuclideanFrameClass