Documentation

Foundation

return to top

source

Imports

Init
Foundation.FirstOrder.Kripke
Foundation.FirstOrder.Syntax
Foundation.FirstOrder.Tarski
Foundation.Logic.Calculus
Foundation.Logic.Decidability
Foundation.Logic.Disjunctive
Foundation.Logic.Embedding
Foundation.Logic.Entailment
Foundation.Logic.ForcingRelation
Foundation.Logic.LindenbaumAlgebra
Foundation.Logic.LogicSymbol
Foundation.Logic.Semantics
Foundation.Meta.ClProver
Foundation.Meta.IntProver
Foundation.Meta.Lit
Foundation.Meta.Qq
Foundation.Meta.Test
Foundation.Meta.TwoSided
Foundation.ProvabilityLogic.Example
Foundation.ProvabilityLogic.Formula
Foundation.ProvabilityLogic.Letterless
Foundation.ProvabilityLogic.Logic
Foundation.ProvabilityLogic.Sequent
Foundation.ProvabilityLogic.Trace
Foundation.Vorspiel.AdjunctiveSet
Foundation.Vorspiel.Arithmetic
Foundation.Vorspiel.Computability
Foundation.Vorspiel.ENat
Foundation.Vorspiel.Empty
Foundation.Vorspiel.ExistsUnique
Foundation.Vorspiel.Function
Foundation.Vorspiel.Graph
Foundation.Vorspiel.IsEmpty
Foundation.Vorspiel.Matrix
Foundation.Vorspiel.Multiset
Foundation.Vorspiel.NotationClass
Foundation.Vorspiel.Option
Foundation.Vorspiel.Part
Foundation.Vorspiel.Quotient
Foundation.Vorspiel.Small
Foundation.Vorspiel.String
Foundation.FirstOrder.Arithmetic.Basic
Foundation.FirstOrder.Arithmetic.Definability
Foundation.FirstOrder.Arithmetic.Examples
Foundation.FirstOrder.Arithmetic.Exponential
Foundation.FirstOrder.Arithmetic.HFS
Foundation.FirstOrder.Arithmetic.LE
Foundation.FirstOrder.Arithmetic.Prenex
Foundation.FirstOrder.Arithmetic.Schemata
Foundation.FirstOrder.Incompleteness.Church
Foundation.FirstOrder.Incompleteness.Consistency
Foundation.FirstOrder.Incompleteness.Definability
Foundation.FirstOrder.Incompleteness.Dense
Foundation.FirstOrder.Incompleteness.Examples
Foundation.FirstOrder.Incompleteness.FGH
Foundation.FirstOrder.Incompleteness.First
Foundation.FirstOrder.Incompleteness.Halting
Foundation.FirstOrder.Incompleteness.Jeroslow
Foundation.FirstOrder.Incompleteness.Löb
Foundation.FirstOrder.Incompleteness.RestrictedProvability
Foundation.FirstOrder.Incompleteness.RosserProvability
Foundation.FirstOrder.Incompleteness.Second
Foundation.FirstOrder.Incompleteness.Speedup
Foundation.FirstOrder.Incompleteness.StandardProvability
Foundation.FirstOrder.Incompleteness.Tarski
Foundation.FirstOrder.Incompleteness.WitnessComparison
Foundation.FirstOrder.Kripke.Basic
Foundation.FirstOrder.Kripke.Classical
Foundation.FirstOrder.Kripke.Intuitionistic
Foundation.FirstOrder.LJ.Basic
Foundation.FirstOrder.LJ.GoedelGentzen
Foundation.FirstOrder.LK.Basic
Foundation.FirstOrder.LK.Completeness
Foundation.FirstOrder.LK.CutFree
Foundation.FirstOrder.LK.Eq
Foundation.FirstOrder.LK.ForcingInterpretation
Foundation.FirstOrder.LK.Hauptsatz
Foundation.FirstOrder.LK.Interpretation
Foundation.FirstOrder.LK.Simplified
Foundation.FirstOrder.LK.Soundness
Foundation.FirstOrder.SetTheory.Basic
Foundation.FirstOrder.SetTheory.FunctionSet
Foundation.FirstOrder.SetTheory.LoewenheimSkolem
Foundation.FirstOrder.SetTheory.NaturalNumberRec
Foundation.FirstOrder.SetTheory.Ordinal
Foundation.FirstOrder.SetTheory.Rayo
Foundation.FirstOrder.SetTheory.Recursion
Foundation.FirstOrder.SetTheory.Schemata
Foundation.FirstOrder.SetTheory.TransitiveClosure
Foundation.FirstOrder.SetTheory.TransitiveModel
Foundation.FirstOrder.SetTheory.Universe
Foundation.FirstOrder.Tarski.AesopInit
Foundation.FirstOrder.Tarski.Basic
Foundation.FirstOrder.Tarski.Definability
Foundation.FirstOrder.Tarski.Elementary
Foundation.FirstOrder.Tarski.Eq
Foundation.FirstOrder.Tarski.Model
Foundation.FirstOrder.Tarski.Monotone
Foundation.FirstOrder.Tarski.Operator
Foundation.FirstOrder.Tarski.Skolemization
Foundation.FirstOrder.Tarski.Ultraproduct
Foundation.Propositional.Boolean.Basic
Foundation.Propositional.Boolean.NNFormula
Foundation.Propositional.Boolean.Tait
Foundation.Propositional.Dialectica.Basic
Foundation.Propositional.Entailment.Cl
Foundation.Propositional.Entailment.Int
Foundation.Propositional.Entailment.Minimal
Foundation.Propositional.Formula.Basic
Foundation.Propositional.Formula.NNFormula
Foundation.Propositional.Heyting.Semantics
Foundation.Propositional.Hilbert.Basic
Foundation.Propositional.LK.Basic
Foundation.Propositional.Logic.Basic
Foundation.ProvabilityLogic.A.Basic
Foundation.ProvabilityLogic.Arithmetic.Interpret
Foundation.ProvabilityLogic.Arithmetic.ModifiedSolovaySentences
Foundation.ProvabilityLogic.Arithmetic.SolovaySentences
Foundation.ProvabilityLogic.Arithmetic.StrongInterpret
Foundation.ProvabilityLogic.Classification.AD
Foundation.ProvabilityLogic.Classification.DS
Foundation.ProvabilityLogic.Classification.General
Foundation.ProvabilityLogic.Classification.Letterless
Foundation.ProvabilityLogic.Classification.Truth
Foundation.ProvabilityLogic.D.Basic
Foundation.ProvabilityLogic.D.NotCIP
Foundation.ProvabilityLogic.GL.Arithmetic
Foundation.ProvabilityLogic.GL.Basic
Foundation.ProvabilityLogic.GL.CIP
Foundation.ProvabilityLogic.GL.FiniteLocalReflection
Foundation.ProvabilityLogic.GL.Fixedpoint
Foundation.ProvabilityLogic.GL.Letterless
Foundation.ProvabilityLogic.GLAlpha.Basic
Foundation.ProvabilityLogic.GLBeta.Basic
Foundation.ProvabilityLogic.GLPlusBoxBot.Arithmetic
Foundation.ProvabilityLogic.GLPlusBoxBot.Basic
Foundation.ProvabilityLogic.Grz.Arithmetic
Foundation.ProvabilityLogic.Grz.Basic
Foundation.ProvabilityLogic.Grz.Boxdot
Foundation.ProvabilityLogic.Kripke.AlmostDefiningFormula
Foundation.ProvabilityLogic.Kripke.Basic
Foundation.ProvabilityLogic.Kripke.Bisimulation
Foundation.ProvabilityLogic.Kripke.Cone
Foundation.ProvabilityLogic.Kripke.DefiningFormula
Foundation.ProvabilityLogic.Kripke.FiniteLineModel
Foundation.ProvabilityLogic.Kripke.Graft
Foundation.ProvabilityLogic.Kripke.Rank
Foundation.ProvabilityLogic.Kripke.RootExtension
Foundation.ProvabilityLogic.Kripke.RootedModel
Foundation.ProvabilityLogic.Kripke.Tail
Foundation.ProvabilityLogic.Kripke.Unravelling
Foundation.ProvabilityLogic.S.Arithmetic
Foundation.ProvabilityLogic.S.Basic
Foundation.ProvabilityLogic.S.Boxdot
Foundation.ProvabilityLogic.S.CIP
Foundation.SecondOrder.Arithmetic.ACA0
Foundation.SecondOrder.Arithmetic.Z2
Foundation.SecondOrder.LK.Basic
Foundation.SecondOrder.LK.RestrictedComprehension
Foundation.SecondOrder.Syntax.BinderNotation
Foundation.SecondOrder.Syntax.Formula
Foundation.SecondOrder.Syntax.Rew
Foundation.SecondOrder.Tarski.Basic
Foundation.Syntax.Predicate.Language
Foundation.Syntax.Predicate.Quantifier
Foundation.Syntax.Predicate.Relational
Foundation.Syntax.Predicate.Rew
Foundation.Syntax.Predicate.Term
Foundation.Vorspiel.Computability.Primrec
Foundation.Vorspiel.Fin.Basic
Foundation.Vorspiel.Fin.Matrix
Foundation.Vorspiel.Finset.Basic
Foundation.Vorspiel.Finset.Card
Foundation.Vorspiel.List.Basic
Foundation.Vorspiel.List.ChainI
Foundation.Vorspiel.List.OAOO
Foundation.Vorspiel.Nat.Basic
Foundation.Vorspiel.Nat.Matrix
Foundation.Vorspiel.Order.Dense
Foundation.Vorspiel.Order.Heyting
Foundation.Vorspiel.Rel.CWF
Foundation.Vorspiel.Rel.WCWF
Foundation.Vorspiel.Set.Basic
Foundation.Vorspiel.Tactic.Disj
Foundation.Vorspiel.Tactic.Primrec
Foundation.FirstOrder.Arithmetic.Basic.Hierarchy
Foundation.FirstOrder.Arithmetic.Basic.Misc
Foundation.FirstOrder.Arithmetic.Basic.Model
Foundation.FirstOrder.Arithmetic.Bootstrapping.FixedPoint
Foundation.FirstOrder.Arithmetic.Bootstrapping.Syntax
Foundation.FirstOrder.Arithmetic.Collection.Basic
Foundation.FirstOrder.Arithmetic.Collection.Equiv
Foundation.FirstOrder.Arithmetic.Definability.Absoluteness
Foundation.FirstOrder.Arithmetic.Definability.BoundedDefinable
Foundation.FirstOrder.Arithmetic.Definability.Definable
Foundation.FirstOrder.Arithmetic.Definability.Hierarchy
Foundation.FirstOrder.Arithmetic.Definability.PrenexDefinable
Foundation.FirstOrder.Arithmetic.EA.Basic
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.Superexp
Foundation.FirstOrder.Arithmetic.HFS.Vec
Foundation.FirstOrder.Arithmetic.IDelta.Basic
Foundation.FirstOrder.Arithmetic.IOpen.Basic
Foundation.FirstOrder.Arithmetic.ISigma1.Prenex
Foundation.FirstOrder.Arithmetic.Induction.Basic
Foundation.FirstOrder.Arithmetic.Induction.Equiv
Foundation.FirstOrder.Arithmetic.LeastNumber.Basic
Foundation.FirstOrder.Arithmetic.Omega1.Basic
Foundation.FirstOrder.Arithmetic.Omega1.Nuon
Foundation.FirstOrder.Arithmetic.PA.Prenex
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.Independence
Foundation.FirstOrder.Arithmetic.R0.Representation
Foundation.FirstOrder.Arithmetic.Schema.DeltaInduction
Foundation.FirstOrder.Arithmetic.TA.Basic
Foundation.FirstOrder.Arithmetic.TA.Nonstandard
Foundation.FirstOrder.Incompleteness.ProvabilityAbstraction.Basic
Foundation.FirstOrder.Incompleteness.ProvabilityAbstraction.FiniteLocalReflection
Foundation.FirstOrder.Incompleteness.ProvabilityAbstraction.Height
Foundation.FirstOrder.Incompleteness.ProvabilityAbstraction.Reflection
Foundation.FirstOrder.Incompleteness.ProvabilityAbstraction.Refutability
Foundation.FirstOrder.Incompleteness.Reflection.IteratedConsistency
Foundation.FirstOrder.Incompleteness.Reflection.Local
Foundation.FirstOrder.Incompleteness.Reflection.SigmaReflection
Foundation.FirstOrder.Incompleteness.Reflection.Unboundedness
Foundation.FirstOrder.Incompleteness.Reflection.Uniform
Foundation.FirstOrder.LK.Completeness.CanonicalModel
Foundation.FirstOrder.LK.Completeness.CountableSublanguage
Foundation.FirstOrder.LK.Completeness.CounterModel
Foundation.FirstOrder.SetTheory.BST.BST
Foundation.FirstOrder.SetTheory.BST.Basic
Foundation.FirstOrder.SetTheory.BST.Model
Foundation.FirstOrder.SetTheory.Basic.Hierarchy
Foundation.FirstOrder.SetTheory.Basic.Misc
Foundation.FirstOrder.SetTheory.Basic.Model
Foundation.FirstOrder.SetTheory.Definability.Definable
Foundation.FirstOrder.SetTheory.Definability.Hierarchy
Foundation.FirstOrder.SetTheory.Recursion.Blueprint
Foundation.FirstOrder.SetTheory.Recursion.Seq
Foundation.FirstOrder.SetTheory.Z.Basic
Foundation.FirstOrder.SetTheory.Z.Model
Foundation.FirstOrder.SetTheory.Z.Z
Foundation.FirstOrder.SetTheory.ZF.Basic
Foundation.FirstOrder.SetTheory.ZF.Model
Foundation.FirstOrder.SetTheory.ZF.ZF
Foundation.FirstOrder.Syntax.Classical.BinderNotation
Foundation.FirstOrder.Syntax.Classical.Bounding
Foundation.FirstOrder.Syntax.Classical.BoundingHierarchy
Foundation.FirstOrder.Syntax.Classical.Coding
Foundation.FirstOrder.Syntax.Classical.Eq
Foundation.FirstOrder.Syntax.Classical.Formula
Foundation.FirstOrder.Syntax.Classical.Operator
Foundation.FirstOrder.Syntax.Classical.Padding
Foundation.FirstOrder.Syntax.Classical.Polarity
Foundation.FirstOrder.Syntax.Classical.PrimrecCoding
Foundation.FirstOrder.Syntax.Classical.Rew
Foundation.FirstOrder.Syntax.Intuitionistic.Formula
Foundation.FirstOrder.Syntax.Intuitionistic.Rew
Foundation.FirstOrder.Tarski.HierarchicalDefinability.Absoluteness
Foundation.FirstOrder.Tarski.HierarchicalDefinability.Basic
Foundation.FirstOrder.Tarski.HierarchicalDefinability.Hierarchy
Foundation.ProvabilityLogic.A.Gentzen.Basic
Foundation.ProvabilityLogic.A.Gentzen.Kripke
Foundation.ProvabilityLogic.D.Gentzen.Basic
Foundation.ProvabilityLogic.D.Gentzen.Kripke
Foundation.ProvabilityLogic.GL.Gentzen.Basic
Foundation.ProvabilityLogic.GL.Gentzen.Kripke
Foundation.ProvabilityLogic.GL.Gentzen.Maehara
Foundation.ProvabilityLogic.Grz.Gentzen.Basic
Foundation.ProvabilityLogic.Grz.Gentzen.Kripke
Foundation.ProvabilityLogic.S.Gentzen.Basic
Foundation.ProvabilityLogic.S.Gentzen.Kripke
Foundation.Vorspiel.Order.BooleanAlgebra.Basic
Foundation.Vorspiel.Order.BooleanAlgebra.Extension
Foundation.Vorspiel.Order.BooleanAlgebra.Iso
Foundation.Vorspiel.Tactic.Primrec.Init
Foundation.FirstOrder.Arithmetic.Bootstrapping.DerivabilityCondition.D1
Foundation.FirstOrder.Arithmetic.Bootstrapping.DerivabilityCondition.D2
Foundation.FirstOrder.Arithmetic.Bootstrapping.DerivabilityCondition.D3
Foundation.FirstOrder.Arithmetic.Bootstrapping.DerivabilityCondition.EquationalTheory
Foundation.FirstOrder.Arithmetic.Bootstrapping.DerivabilityCondition.PeanoMinus
Foundation.FirstOrder.Arithmetic.Bootstrapping.PartialTruth.Bounded
Foundation.FirstOrder.Arithmetic.Bootstrapping.PartialTruth.General
Foundation.FirstOrder.Arithmetic.Bootstrapping.PartialTruth.TermVal
Foundation.FirstOrder.Arithmetic.Bootstrapping.Syntax.CraigTrick
Foundation.FirstOrder.Arithmetic.Bootstrapping.Syntax.Language
Foundation.FirstOrder.Arithmetic.Bootstrapping.Syntax.Theory
Foundation.FirstOrder.Arithmetic.Bootstrapping.Syntax.Formula.Basic
Foundation.FirstOrder.Arithmetic.Bootstrapping.Syntax.Formula.Bounded
Foundation.FirstOrder.Arithmetic.Bootstrapping.Syntax.Formula.Coding
Foundation.FirstOrder.Arithmetic.Bootstrapping.Syntax.Formula.Functions
Foundation.FirstOrder.Arithmetic.Bootstrapping.Syntax.Formula.Hierarchy
Foundation.FirstOrder.Arithmetic.Bootstrapping.Syntax.Formula.Iteration
Foundation.FirstOrder.Arithmetic.Bootstrapping.Syntax.Formula.Typed
Foundation.FirstOrder.Arithmetic.Bootstrapping.Syntax.Proof.Basic
Foundation.FirstOrder.Arithmetic.Bootstrapping.Syntax.Proof.Coding
Foundation.FirstOrder.Arithmetic.Bootstrapping.Syntax.Proof.Typed
Foundation.FirstOrder.Arithmetic.Bootstrapping.Syntax.Term.Basic
Foundation.FirstOrder.Arithmetic.Bootstrapping.Syntax.Term.Coding
Foundation.FirstOrder.Arithmetic.Bootstrapping.Syntax.Term.Functions
Foundation.FirstOrder.Arithmetic.Bootstrapping.Syntax.Term.Typed

Imported by