For questions about words, phrases and definitions that are specific to proof assistants.
Sites with related glossaries
nLab
Stanford Encyclopedia of Philosophy
ProofWiki
Algebraic Theory: An algebraic theory is a concept in universal algebra that describes a specific type of algebraic gadget, such as groups or rings. An individual group or ring is a model of the appropriate theory. Roughly speaking, an algebraic theory consists of a specification of operations and laws that these operations must satisfy. (from nLab)
Consistency: A system of formal logic is consistent if false is not deducible in the system. (from nLab)
Deductive System: Calculus of axioms and inference rules defining derivable judgments. Used in the presentation of logics and programming languages. ("From Logical and Meta-Logical Frameworks" by Frank Pfenning)
Formal Proof: A formal proof is whatever is called a ‘proof’ in a formal system; a formal system for mathematics then gives rules for producing a proof in the above sense. Typically, a formal system is inductively defined, and hence its proofs are fully circumscribed; this is the case for deductive systems such as natural deduction, sequent calculus, and Hilbert systems. Gödel's theorem suggests, however, that no such system can encapsulate all of mathematics. (from nLab)
Judgment: In formal logic, a judgment, or judgement, is a “meta-proposition”; that is, a proposition belonging to the meta-language (the deductive system or logical framework) rather than to the object language. (From nLab)
Inaccessible Cardinal: An inaccessible cardinal is a cardinal number κ which cannot be “accessed” from smaller cardinals using only the basic operations on cardinals. It follows that the collection of sets smaller than κ satisfies the axioms of set theory. (from nLab)
Inconsistency: A system in formal logic is called inconsistent if it admits a proof of a contradiction (that is, usually, a proof of false, or an inhabitant of the empty type). (from nLab)
Inhabited type: A set or type is inhabited if it contains an element or term. (from nLab)
Logical Framework: Meta-language for the formalization of deductive systems. ("From Logical and Meta-Logical Frameworks" by Frank Pfenning)
Martin-Löf dependent type theory: Per Martin-Löf‘s dependent type theory, also known as intuitionistic type theory (Martin-Löf 75), or constructive type theory is a specific form of type theory developed to support constructive mathematics. (from nLab)
Metalanguage: In formal logic, a metalanguage is a language (formal or informal) in which the symbols and rules for manipulating another (formal) language – the object language – are themselves formulated. That is, the metalanguage is the language used when talking about the object language. (From nLab)
Meta-Logical Framework: Meta-language for reasoning about deductive systems. ("From Logical and Meta-Logical Frameworks" by Frank Pfenning)
Model: In model theory, a model of a theory is a realization of the types, operations, relations, and axioms of that theory. In ordinary model theory one usually studies mainly models in sets, but in categorical logic we study models in other categories, especially in topoi. (From nLab)
Normal Form: In a rewriting system, a term is said to be of normal form if it does not admit any further rewrites. (from nLab)
Object language: See Metalanguage.
Propositions as Types: In type theory, the paradigm of propositions as types says that propositions and types are essentially the same. A proposition is identified with the type (collection) of all its proofs, and a type is identified with the proposition that it has a term (so that each of its terms is in turn a proof of the corresponding proposition). (from nLab)
Singleton: Given a set X and an element a of X, the singleton {a} is that subset of X whose only element is a. Strictly speaking, we are considering here a singleton subset; we could also consider a singleton list or 1-tuple (a), but this is an equivalent concept. (From nLab)
Trivial: A trivial object is too simple to be simple. (From nLab)
Type Theory: Type theory is a branch of mathematical symbolic logic, which derives its name from the fact that it formalizes not only mathematical terms – such as a variable x, or a function f – and operations on them, but also formalizes the idea that each such term is of some definite type, for instance that the type N of a natural number x:N is different from the type N→N of a function f:N→N between natural numbers. (From nLab)
Universe: A universe is a realm within which (some conceived part, naively and virtually all, of) mathematics may be thought of as taking place. (from nLab)
