Documentation

Foundation

return to top

source

Imports

Init
Foundation.Init
Foundation.FirstOrder.Basic
Foundation.FirstOrder.Hauptsatz
Foundation.FirstOrder.Interpretation
Foundation.FirstOrder.Ultraproduct
Foundation.InterpretabilityLogic.Axioms
Foundation.InterpretabilityLogic.Entailment
Foundation.InterpretabilityLogic.LogicSymbol
Foundation.LinearLogic.MLL
Foundation.Logic.Calculus
Foundation.Logic.Decidability
Foundation.Logic.Disjunctive
Foundation.Logic.Entailment
Foundation.Logic.ForcingRelation
Foundation.Logic.LindenbaumAlgebra
Foundation.Logic.LogicSymbol
Foundation.Logic.Semantics
Foundation.Meta.Test
Foundation.Meta.TwoSided
Foundation.Modal.Axioms
Foundation.Modal.ComplementClosedConsistentFinset
Foundation.Modal.Kripke
Foundation.Modal.LogicSymbol
Foundation.Modal.MaximalConsistentSet
Foundation.Modal.ModalCompanion
Foundation.Modal.Tableau
Foundation.Propositional.ConsistentTableau
Foundation.Propositional.Decidable
Foundation.Propositional.Translation
Foundation.ProvabilityLogic.Arithmetic
Foundation.ProvabilityLogic.Realization
Foundation.ProvabilityLogic.SolovaySentences
Foundation.FirstOrder.Arithmetic.Basic
Foundation.FirstOrder.Arithmetic.Definability
Foundation.FirstOrder.Arithmetic.Exponential
Foundation.FirstOrder.Arithmetic.HFS
Foundation.FirstOrder.Arithmetic.Induction
Foundation.FirstOrder.Arithmetic.Schemata
Foundation.FirstOrder.Basic.AesopInit
Foundation.FirstOrder.Basic.BinderNotation
Foundation.FirstOrder.Basic.Calculus
Foundation.FirstOrder.Basic.Calculus2
Foundation.FirstOrder.Basic.Coding
Foundation.FirstOrder.Basic.Definability
Foundation.FirstOrder.Basic.Eq
Foundation.FirstOrder.Basic.Model
Foundation.FirstOrder.Basic.Operator
Foundation.FirstOrder.Basic.Padding
Foundation.FirstOrder.Basic.Soundness
Foundation.FirstOrder.Bootstrapping.Consistency
Foundation.FirstOrder.Bootstrapping.DerivabilityCondition
Foundation.FirstOrder.Bootstrapping.FixedPoint
Foundation.FirstOrder.Bootstrapping.RosserProvability
Foundation.FirstOrder.Bootstrapping.Syntax
Foundation.FirstOrder.Bootstrapping.WitnessComparison
Foundation.FirstOrder.Completeness.Coding
Foundation.FirstOrder.Completeness.Completeness
Foundation.FirstOrder.Completeness.Corollaries
Foundation.FirstOrder.Completeness.SearchTree
Foundation.FirstOrder.Completeness.SubLanguage
Foundation.FirstOrder.Incompleteness.Dense
Foundation.FirstOrder.Incompleteness.Examples
Foundation.FirstOrder.Incompleteness.First
Foundation.FirstOrder.Incompleteness.GödelRosser
Foundation.FirstOrder.Incompleteness.Halting
Foundation.FirstOrder.Incompleteness.Löb
Foundation.FirstOrder.Incompleteness.RestrictedProvability
Foundation.FirstOrder.Incompleteness.Second
Foundation.FirstOrder.Incompleteness.Tarski
Foundation.FirstOrder.Incompleteness.Yablo
Foundation.FirstOrder.Intuitionistic.Deduction
Foundation.FirstOrder.Intuitionistic.Formula
Foundation.FirstOrder.Intuitionistic.Rew
Foundation.FirstOrder.Kripke.Basic
Foundation.FirstOrder.Kripke.Intuitionistic
Foundation.FirstOrder.Kripke.WeakForcing
Foundation.FirstOrder.NegationTranslation.Girard
Foundation.FirstOrder.NegationTranslation.GoedelGentzen
Foundation.FirstOrder.Order.Le
Foundation.FirstOrder.SetTheory.Basic
Foundation.FirstOrder.SetTheory.Function
Foundation.FirstOrder.SetTheory.LoewenheimSkolem
Foundation.FirstOrder.SetTheory.Ordinal
Foundation.FirstOrder.SetTheory.TransitiveModel
Foundation.FirstOrder.SetTheory.Universe
Foundation.FirstOrder.SetTheory.Z
Foundation.FirstOrder.Skolemization.Hull
Foundation.InterpretabilityLogic.Entailment.Basic
Foundation.InterpretabilityLogic.Entailment.CL
Foundation.InterpretabilityLogic.Entailment.IL
Foundation.InterpretabilityLogic.Entailment.ILMinus
Foundation.InterpretabilityLogic.Entailment.ILMinus_J1
Foundation.InterpretabilityLogic.Entailment.ILMinus_J2
Foundation.InterpretabilityLogic.Entailment.ILMinus_J4
Foundation.InterpretabilityLogic.Entailment.ILMinus_J5
Foundation.InterpretabilityLogic.Entailment.ILMinus_M
Foundation.InterpretabilityLogic.Entailment.IL_KW1Zero
Foundation.InterpretabilityLogic.Entailment.IL_KW2
Foundation.InterpretabilityLogic.Entailment.IL_M
Foundation.InterpretabilityLogic.Entailment.IL_M₀
Foundation.InterpretabilityLogic.Entailment.IL_M₀_W
Foundation.InterpretabilityLogic.Entailment.IL_P
Foundation.InterpretabilityLogic.Entailment.IL_R
Foundation.InterpretabilityLogic.Entailment.IL_R_W
Foundation.InterpretabilityLogic.Entailment.IL_Rstar
Foundation.InterpretabilityLogic.Entailment.IL_W
Foundation.InterpretabilityLogic.Entailment.IL_Wstar
Foundation.InterpretabilityLogic.Formula.Basic
Foundation.InterpretabilityLogic.Formula.OfModal
Foundation.InterpretabilityLogic.Formula.Substitution
Foundation.InterpretabilityLogic.Formula.ToModal
Foundation.InterpretabilityLogic.Hilbert.Axiom
Foundation.InterpretabilityLogic.Hilbert.Basic_Minimal
Foundation.InterpretabilityLogic.Logic.Basic
Foundation.InterpretabilityLogic.Veltman.AxiomJ1
Foundation.InterpretabilityLogic.Veltman.AxiomJ2
Foundation.InterpretabilityLogic.Veltman.AxiomJ4
Foundation.InterpretabilityLogic.Veltman.AxiomJ5
Foundation.InterpretabilityLogic.Veltman.AxiomM
Foundation.InterpretabilityLogic.Veltman.AxiomM₀
Foundation.InterpretabilityLogic.Veltman.AxiomP
Foundation.InterpretabilityLogic.Veltman.AxiomR
Foundation.InterpretabilityLogic.Veltman.AxiomW
Foundation.InterpretabilityLogic.Veltman.Basic
Foundation.InterpretabilityLogic.Veltman.Hilbert
Foundation.LinearLogic.FirstOrder.Calculus
Foundation.LinearLogic.FirstOrder.Formula
Foundation.LinearLogic.FirstOrder.Rew
Foundation.Modal.Algebra.Basic
Foundation.Modal.Boxdot.Basic
Foundation.Modal.Boxdot.GLPoint3_GrzPoint3
Foundation.Modal.Boxdot.GL_S
Foundation.Modal.Boxdot.Grz_S
Foundation.Modal.Boxdot.Jerabek
Foundation.Modal.Boxdot.K4_S4
Foundation.Modal.Boxdot.Ver_Triv
Foundation.Modal.Entailment.AxiomGeach
Foundation.Modal.Entailment.Basic
Foundation.Modal.Entailment.DiaDuality
Foundation.Modal.Entailment.E
Foundation.Modal.Entailment.EM
Foundation.Modal.Entailment.EMC
Foundation.Modal.Entailment.EMCN
Foundation.Modal.Entailment.EMK
Foundation.Modal.Entailment.EN
Foundation.Modal.Entailment.END
Foundation.Modal.Entailment.ET
Foundation.Modal.Entailment.ET5
Foundation.Modal.Entailment.ETB
Foundation.Modal.Entailment.GL
Foundation.Modal.Entailment.Grz
Foundation.Modal.Entailment.K
Foundation.Modal.Entailment.K4
Foundation.Modal.Entailment.K4Hen
Foundation.Modal.Entailment.K4Henkin
Foundation.Modal.Entailment.K4Loeb
Foundation.Modal.Entailment.K5
Foundation.Modal.Entailment.KB
Foundation.Modal.Entailment.KD
Foundation.Modal.Entailment.KP
Foundation.Modal.Entailment.KT
Foundation.Modal.Entailment.KTc
Foundation.Modal.Entailment.N
Foundation.Modal.Entailment.S4
Foundation.Modal.Entailment.S5
Foundation.Modal.Entailment.S5Grz
Foundation.Modal.Entailment.Triv
Foundation.Modal.Entailment.Ver
Foundation.Modal.Formula.Basic
Foundation.Modal.Formula.Complement
Foundation.Modal.Formula.NNFormula
Foundation.Modal.Hilbert.Axiom
Foundation.Modal.Hilbert.GL_K4Loeb_K4Henkin_K4Hen
Foundation.Modal.Hilbert.NNFormula
Foundation.Modal.Hilbert.WithRE_Normal
Foundation.Modal.Kripke.Algebra
Foundation.Modal.Kripke.Antisymmetric
Foundation.Modal.Kripke.Asymmetric
Foundation.Modal.Kripke.AxiomFourN
Foundation.Modal.Kripke.AxiomGeach
Foundation.Modal.Kripke.AxiomGrz
Foundation.Modal.Kripke.AxiomH
Foundation.Modal.Kripke.AxiomI
Foundation.Modal.Kripke.AxiomL
Foundation.Modal.Kripke.AxiomMcK
Foundation.Modal.Kripke.AxiomMk
Foundation.Modal.Kripke.AxiomPoint3
Foundation.Modal.Kripke.AxiomPoint4
Foundation.Modal.Kripke.AxiomVer
Foundation.Modal.Kripke.AxiomWeakPoint2
Foundation.Modal.Kripke.AxiomWeakPoint3
Foundation.Modal.Kripke.Balloon
Foundation.Modal.Kripke.Basic
Foundation.Modal.Kripke.Closure
Foundation.Modal.Kripke.Cluster
Foundation.Modal.Kripke.Completeness
Foundation.Modal.Kripke.ComplexityLimited
Foundation.Modal.Kripke.ExtendRoot
Foundation.Modal.Kripke.Filtration
Foundation.Modal.Kripke.Hilbert
Foundation.Modal.Kripke.Irreflexive
Foundation.Modal.Kripke.Irreflexivize
Foundation.Modal.Kripke.LinearFrame
Foundation.Modal.Kripke.NNFormula
Foundation.Modal.Kripke.Preservation
Foundation.Modal.Kripke.Rank
Foundation.Modal.Kripke.Rooted
Foundation.Modal.Kripke.Terminated
Foundation.Modal.Kripke.Tree
Foundation.Modal.Kripke.Undefinability
Foundation.Modal.Logic.Basic
Foundation.Modal.Logic.Global
Foundation.Modal.Logic.SumNormal
Foundation.Modal.Logic.SumQuasiNormal
Foundation.Modal.Maximal.Basic
Foundation.Modal.Maximal.Makinson
Foundation.Modal.Maximal.Unprovability
Foundation.Modal.ModalCompanion.Corsi
Foundation.Modal.ModalCompanion.Standard
Foundation.Modal.Modality.Basic
Foundation.Modal.Modality.S5
Foundation.Modal.Neighborhood.AxiomC
Foundation.Modal.Neighborhood.AxiomGeach
Foundation.Modal.Neighborhood.AxiomK
Foundation.Modal.Neighborhood.AxiomM
Foundation.Modal.Neighborhood.AxiomN
Foundation.Modal.Neighborhood.AxiomP
Foundation.Modal.Neighborhood.Basic
Foundation.Modal.Neighborhood.Completeness
Foundation.Modal.Neighborhood.Filtration
Foundation.Modal.Neighborhood.Hilbert
Foundation.Modal.Neighborhood.IntersectionClosure
Foundation.Modal.Neighborhood.Supplementation
Foundation.Modal.PLoN.Basic
Foundation.Modal.PLoN.Completeness
Foundation.Modal.PLoN.Hilbert
Foundation.Modal.PLoN.Logic
Foundation.Modal.VanBentham.StandardTranslation
Foundation.Propositional.ClassicalSemantics.Basic
Foundation.Propositional.ClassicalSemantics.Hilbert
Foundation.Propositional.ClassicalSemantics.NNFormula
Foundation.Propositional.ClassicalSemantics.Tait
Foundation.Propositional.ClassicalSemantics.ZeroSubst
Foundation.Propositional.Entailment.AxiomDNE
Foundation.Propositional.Entailment.AxiomEFQ
Foundation.Propositional.Entailment.AxiomElimContra
Foundation.Propositional.Entailment.AxiomLEM
Foundation.Propositional.Entailment.AxiomPeirce
Foundation.Propositional.Entailment.Corsi
Foundation.Propositional.Entailment.KC
Foundation.Propositional.Entailment.KrieselPutnam
Foundation.Propositional.Entailment.LC
Foundation.Propositional.Entailment.Scott
Foundation.Propositional.FMT.AxiomSer
Foundation.Propositional.FMT.Basic
Foundation.Propositional.FMT.Completeness
Foundation.Propositional.FMT.Hilbert
Foundation.Propositional.FMT.Logic
Foundation.Propositional.Formula.Basic
Foundation.Propositional.Formula.NNFormula
Foundation.Propositional.Heyting.Semantics
Foundation.Propositional.Hilbert.Axiom
Foundation.Propositional.Hilbert.F
Foundation.Propositional.Hilbert.F_WF
Foundation.Propositional.Hilbert.Standard
Foundation.Propositional.Hilbert.VF
Foundation.Propositional.Hilbert.WF
Foundation.Propositional.Hilbert.WF_VF
Foundation.Propositional.Kripke.AxiomDummett
Foundation.Propositional.Kripke.AxiomKrieselPutnam
Foundation.Propositional.Kripke.AxiomLEM
Foundation.Propositional.Kripke.AxiomWLEM
Foundation.Propositional.Kripke.Basic
Foundation.Propositional.Kripke.Completeness
Foundation.Propositional.Kripke.Filtration
Foundation.Propositional.Kripke.Hilbert
Foundation.Propositional.Kripke.Preservation
Foundation.Propositional.Kripke.Rooted
Foundation.Propositional.Kripke2.AxiomCorfl
Foundation.Propositional.Kripke2.AxiomHrd
Foundation.Propositional.Kripke2.AxiomPSCon
Foundation.Propositional.Kripke2.AxiomRfl
Foundation.Propositional.Kripke2.AxiomSer
Foundation.Propositional.Kripke2.AxiomSym
Foundation.Propositional.Kripke2.AxiomTra
Foundation.Propositional.Kripke2.Basic
Foundation.Propositional.Kripke2.FTheory
Foundation.Propositional.Kripke2.Hilbert
Foundation.Propositional.Kripke2.Logic
Foundation.Propositional.Logic.Basic
Foundation.Propositional.Logic.Letterless_Int_Cl
Foundation.Propositional.Logic.PostComplete
Foundation.Propositional.Logic.Slash
Foundation.Propositional.Tait.Calculus
Foundation.ProvabilityLogic.Classification.LetterlessTrace
Foundation.ProvabilityLogic.Classification.Result
Foundation.ProvabilityLogic.Classification.Trace
Foundation.ProvabilityLogic.GL.Completeness
Foundation.ProvabilityLogic.GL.Soundness
Foundation.ProvabilityLogic.GL.Uniform
Foundation.ProvabilityLogic.GL.Unprovability
Foundation.ProvabilityLogic.Grz.Completeness
Foundation.ProvabilityLogic.N.Soundness
Foundation.ProvabilityLogic.S.Completeness
Foundation.ProvabilityLogic.S.Soundness
Foundation.Semantics.CoherenceSpace.Basic
Foundation.Semantics.CoherenceSpace.StableFunction
Foundation.Syntax.Predicate.Language
Foundation.Syntax.Predicate.Quantifier
Foundation.Syntax.Predicate.Relational
Foundation.Syntax.Predicate.Rew
Foundation.Syntax.Predicate.Term
Foundation.FirstOrder.Arithmetic.Basic.Hierarchy
Foundation.FirstOrder.Arithmetic.Basic.Misc
Foundation.FirstOrder.Arithmetic.Basic.Model
Foundation.FirstOrder.Arithmetic.Basic.Monotone
Foundation.FirstOrder.Arithmetic.Definability.Absoluteness
Foundation.FirstOrder.Arithmetic.Definability.BoundedDefinable
Foundation.FirstOrder.Arithmetic.Definability.Definable
Foundation.FirstOrder.Arithmetic.Definability.Hierarchy
Foundation.FirstOrder.Arithmetic.Exponential.Bit
Foundation.FirstOrder.Arithmetic.Exponential.Exp
Foundation.FirstOrder.Arithmetic.Exponential.Log
Foundation.FirstOrder.Arithmetic.Exponential.PPow2
Foundation.FirstOrder.Arithmetic.Exponential.Pow2
Foundation.FirstOrder.Arithmetic.HFS.Basic
Foundation.FirstOrder.Arithmetic.HFS.Coding
Foundation.FirstOrder.Arithmetic.HFS.Fixpoint
Foundation.FirstOrder.Arithmetic.HFS.PRF
Foundation.FirstOrder.Arithmetic.HFS.Seq
Foundation.FirstOrder.Arithmetic.HFS.Vec
Foundation.FirstOrder.Arithmetic.IOpen.Basic
Foundation.FirstOrder.Arithmetic.Omega1.Basic
Foundation.FirstOrder.Arithmetic.Omega1.Nuon
Foundation.FirstOrder.Arithmetic.PeanoMinus.Basic
Foundation.FirstOrder.Arithmetic.PeanoMinus.Functions
Foundation.FirstOrder.Arithmetic.PeanoMinus.Q
Foundation.FirstOrder.Arithmetic.Q.Basic
Foundation.FirstOrder.Arithmetic.R0.Basic
Foundation.FirstOrder.Arithmetic.R0.Representation
Foundation.FirstOrder.Arithmetic.TA.Basic
Foundation.FirstOrder.Arithmetic.TA.Nonstandard
Foundation.FirstOrder.Basic.Semantics.Elementary
Foundation.FirstOrder.Basic.Semantics.Semantics
Foundation.FirstOrder.Basic.Syntax.Formula
Foundation.FirstOrder.Basic.Syntax.Rew
Foundation.FirstOrder.Basic.Syntax.Theory
Foundation.FirstOrder.Bootstrapping.DerivabilityCondition.D1
Foundation.FirstOrder.Bootstrapping.DerivabilityCondition.D2
Foundation.FirstOrder.Bootstrapping.DerivabilityCondition.D3
Foundation.FirstOrder.Bootstrapping.DerivabilityCondition.EquationalTheory
Foundation.FirstOrder.Bootstrapping.DerivabilityCondition.PeanoMinus
Foundation.FirstOrder.Bootstrapping.ProvabilityAbstraction.Basic
Foundation.FirstOrder.Bootstrapping.ProvabilityAbstraction.Height
Foundation.FirstOrder.Bootstrapping.Syntax.Language
Foundation.FirstOrder.Bootstrapping.Syntax.Theory
Foundation.FirstOrder.SetTheory.Basic.Axioms
Foundation.FirstOrder.SetTheory.Basic.Misc
Foundation.FirstOrder.SetTheory.Basic.Model
Foundation.InterpretabilityLogic.Hilbert.Basic.Basic
Foundation.InterpretabilityLogic.Hilbert.Minimal.Basic
Foundation.InterpretabilityLogic.Veltman.Logic.CL
Foundation.InterpretabilityLogic.Veltman.Logic.IL
Foundation.InterpretabilityLogic.Veltman.Logic.ILMinus
Foundation.InterpretabilityLogic.Veltman.Logic.ILMinus_J1
Foundation.InterpretabilityLogic.Veltman.Logic.ILMinus_J1_J2
Foundation.InterpretabilityLogic.Veltman.Logic.ILMinus_J1_J2_J5
Foundation.InterpretabilityLogic.Veltman.Logic.ILMinus_J1_J4Plus
Foundation.InterpretabilityLogic.Veltman.Logic.ILMinus_J1_J4Plus_J5
Foundation.InterpretabilityLogic.Veltman.Logic.ILMinus_J1_J5
Foundation.InterpretabilityLogic.Veltman.Logic.ILMinus_J2Plus
Foundation.InterpretabilityLogic.Veltman.Logic.ILMinus_J2Plus_J5
Foundation.InterpretabilityLogic.Veltman.Logic.ILMinus_J4Plus
Foundation.InterpretabilityLogic.Veltman.Logic.ILMinus_J4Plus_J5
Foundation.InterpretabilityLogic.Veltman.Logic.ILMinus_J5
Foundation.InterpretabilityLogic.Veltman.Logic.IL_F
Foundation.InterpretabilityLogic.Veltman.Logic.IL_M
Foundation.InterpretabilityLogic.Veltman.Logic.IL_M₀
Foundation.InterpretabilityLogic.Veltman.Logic.IL_M₀_W
Foundation.InterpretabilityLogic.Veltman.Logic.IL_P
Foundation.InterpretabilityLogic.Veltman.Logic.IL_P₀
Foundation.InterpretabilityLogic.Veltman.Logic.IL_R
Foundation.InterpretabilityLogic.Veltman.Logic.IL_R_W
Foundation.InterpretabilityLogic.Veltman.Logic.IL_W
Foundation.Modal.Hilbert.Normal.Basic
Foundation.Modal.Hilbert.WithHenkin.Basic
Foundation.Modal.Hilbert.WithLoeb.Basic
Foundation.Modal.Hilbert.WithRE.Basic
Foundation.Modal.Kripke.Logic.GLPoint3
Foundation.Modal.Kripke.Logic.GrzPoint2
Foundation.Modal.Kripke.Logic.GrzPoint3
Foundation.Modal.Kripke.Logic.K
Foundation.Modal.Kripke.Logic.K4
Foundation.Modal.Kripke.Logic.K45
Foundation.Modal.Kripke.Logic.K4McK
Foundation.Modal.Kripke.Logic.K4Point2
Foundation.Modal.Kripke.Logic.K4Point3
Foundation.Modal.Kripke.Logic.K4n
Foundation.Modal.Kripke.Logic.K5
Foundation.Modal.Kripke.Logic.KB
Foundation.Modal.Kripke.Logic.KB4
Foundation.Modal.Kripke.Logic.KB5
Foundation.Modal.Kripke.Logic.KD
Foundation.Modal.Kripke.Logic.KD4
Foundation.Modal.Kripke.Logic.KD45
Foundation.Modal.Kripke.Logic.KD5
Foundation.Modal.Kripke.Logic.KDB
Foundation.Modal.Kripke.Logic.KHen
Foundation.Modal.Kripke.Logic.KT
Foundation.Modal.Kripke.Logic.KT4B
Foundation.Modal.Kripke.Logic.KTB
Foundation.Modal.Kripke.Logic.KTMk
Foundation.Modal.Kripke.Logic.KTc
Foundation.Modal.Kripke.Logic.S4
Foundation.Modal.Kripke.Logic.S4H
Foundation.Modal.Kripke.Logic.S4McK
Foundation.Modal.Kripke.Logic.S4Point2
Foundation.Modal.Kripke.Logic.S4Point2McK
Foundation.Modal.Kripke.Logic.S4Point3
Foundation.Modal.Kripke.Logic.S4Point3McK
Foundation.Modal.Kripke.Logic.S4Point4
Foundation.Modal.Kripke.Logic.S4Point4McK
Foundation.Modal.Kripke.Logic.S5
Foundation.Modal.Kripke.Logic.S5Grz
Foundation.Modal.Kripke.Logic.Triv
Foundation.Modal.Kripke.Logic.Ver
Foundation.Modal.Logic.GL.Independency
Foundation.Modal.ModalCompanion.Corsi.VF
Foundation.Modal.ModalCompanion.Standard.Basic
Foundation.Modal.ModalCompanion.Standard.Cl
Foundation.Modal.ModalCompanion.Standard.Int
Foundation.Modal.ModalCompanion.Standard.KC
Foundation.Modal.ModalCompanion.Standard.LC
Foundation.Modal.Neighborhood.Logic.E
Foundation.Modal.Neighborhood.Logic.E4
Foundation.Modal.Neighborhood.Logic.E5
Foundation.Modal.Neighborhood.Logic.EB
Foundation.Modal.Neighborhood.Logic.EC
Foundation.Modal.Neighborhood.Logic.ECN
Foundation.Modal.Neighborhood.Logic.ED
Foundation.Modal.Neighborhood.Logic.EK
Foundation.Modal.Neighborhood.Logic.EM
Foundation.Modal.Neighborhood.Logic.EMC
Foundation.Modal.Neighborhood.Logic.EMC4
Foundation.Modal.Neighborhood.Logic.EMCN
Foundation.Modal.Neighborhood.Logic.EMCN4
Foundation.Modal.Neighborhood.Logic.EMK
Foundation.Modal.Neighborhood.Logic.EMN
Foundation.Modal.Neighborhood.Logic.EMNT4
Foundation.Modal.Neighborhood.Logic.EMT
Foundation.Modal.Neighborhood.Logic.EMT4
Foundation.Modal.Neighborhood.Logic.EN
Foundation.Modal.Neighborhood.Logic.EN4
Foundation.Modal.Neighborhood.Logic.END
Foundation.Modal.Neighborhood.Logic.END4
Foundation.Modal.Neighborhood.Logic.ENT4
Foundation.Modal.Neighborhood.Logic.EP
Foundation.Modal.Neighborhood.Logic.ET
Foundation.Modal.Neighborhood.Logic.ET4
Foundation.Modal.Neighborhood.Logic.ET5
Foundation.Modal.Neighborhood.Logic.ETB
Foundation.Modal.PLoN.Logic.N
Foundation.Propositional.Entailment.Cl.Basic
Foundation.Propositional.Entailment.Cl.Łukasiewicz
Foundation.Propositional.Entailment.Corsi.Basic
Foundation.Propositional.Entailment.Corsi.F
Foundation.Propositional.Entailment.Corsi.VF
Foundation.Propositional.Entailment.Corsi.WF
Foundation.Propositional.Entailment.Int.Basic
Foundation.Propositional.Entailment.Int.DNE_of_LEM
Foundation.Propositional.Entailment.Minimal.Basic
Foundation.Propositional.FMT.Logic.VF
Foundation.Propositional.FMT.Logic.VF_Ser
Foundation.Propositional.Hilbert.F.Basic
Foundation.Propositional.Hilbert.F.Deduction
Foundation.Propositional.Hilbert.F.Disjunctive
Foundation.Propositional.Hilbert.Standard.Basic
Foundation.Propositional.Hilbert.Standard.Glivenko
Foundation.Propositional.Hilbert.VF.Basic
Foundation.Propositional.Hilbert.VF.Disjunctive
Foundation.Propositional.Hilbert.WF.Basic
Foundation.Propositional.Kripke.Logic.Cl
Foundation.Propositional.Kripke.Logic.Int
Foundation.Propositional.Kripke.Logic.KC
Foundation.Propositional.Kripke.Logic.KrieselPutnam
Foundation.Propositional.Kripke.Logic.LC
Foundation.Propositional.Kripke2.Logic.F
Foundation.Propositional.Kripke2.Logic.F_Rfl
Foundation.Propositional.Kripke2.Logic.F_Rfl_Sym
Foundation.Propositional.Kripke2.Logic.F_Rfl_Tra1
Foundation.Propositional.Kripke2.Logic.F_Rfl_Tra1_Hrd
Foundation.Propositional.Kripke2.Logic.F_Ser
Foundation.Propositional.Kripke2.Logic.F_Sym
Foundation.Propositional.Kripke2.Logic.F_Tra1
Foundation.Propositional.Kripke2.Logic.F_Tra1_Hrd
Foundation.Propositional.Neighborhood.NB.Basic
Foundation.Propositional.Neighborhood.NB.Hilbert
Foundation.Propositional.Neighborhood.NB.Logic
Foundation.Semantics.Algebra.Modal.Basic
Foundation.Semantics.Algebra.Modal.Magari
Foundation.FirstOrder.Bootstrapping.Syntax.Formula.Basic
Foundation.FirstOrder.Bootstrapping.Syntax.Formula.Coding
Foundation.FirstOrder.Bootstrapping.Syntax.Formula.Functions
Foundation.FirstOrder.Bootstrapping.Syntax.Formula.Iteration
Foundation.FirstOrder.Bootstrapping.Syntax.Formula.Typed
Foundation.FirstOrder.Bootstrapping.Syntax.Proof.Basic
Foundation.FirstOrder.Bootstrapping.Syntax.Proof.Coding
Foundation.FirstOrder.Bootstrapping.Syntax.Proof.Typed
Foundation.FirstOrder.Bootstrapping.Syntax.Term.Basic
Foundation.FirstOrder.Bootstrapping.Syntax.Term.Coding
Foundation.FirstOrder.Bootstrapping.Syntax.Term.Functions
Foundation.FirstOrder.Bootstrapping.Syntax.Term.Typed
Foundation.Modal.Kripke.Logic.GL.Completeness
Foundation.Modal.Kripke.Logic.GL.MDP
Foundation.Modal.Kripke.Logic.GL.Soundness
Foundation.Modal.Kripke.Logic.GL.Tree
Foundation.Modal.Kripke.Logic.GL.Unnecessitation
Foundation.Modal.Kripke.Logic.Grz.Completeness
Foundation.Modal.Kripke.Logic.Grz.Soundness
Foundation.Modal.Neighborhood.Logic.Incomparability.ED_EP
Foundation.Propositional.Neighborhood.NB.Logic.WF

Imported by