|logic||category theory||type theory|
|true||terminal object/(-2)-truncated object||h-level 0-type/unit type|
|false||initial object||empty type|
|proposition||(-1)-truncated object||h-proposition, mere proposition|
|cut rule||composition of classifying morphisms / pullback of display maps||substitution|
|cut elimination for implication||counit for hom-tensor adjunction||beta reduction|
|introduction rule for implication||unit for hom-tensor adjunction||eta conversion|
|logical conjunction||product||product type|
|disjunction||coproduct ((-1)-truncation of)||sum type (bracket type of)|
|implication||internal hom||function type|
|negation||internal hom into initial object||function type into empty type|
|universal quantification||dependent product||dependent product type|
|existential quantification||dependent sum ((-1)-truncation of)||dependent sum type (bracket type of)|
|equivalence||path space object||identity type|
|equivalence class||quotient||quotient type|
|induction||colimit||inductive type, W-type, M-type|
|higher induction||higher colimit||higher inductive type|
|completely presented set||discrete object/0-truncated object||h-level 2-type/preset/h-set|
|set||internal 0-groupoid||Bishop set/setoid|
|universe||object classifier||type of types|
|modality||closure operator, (idemponent) monad||modal type theory, monad (in computer science)|
|linear logic||(symmetric, closed) monoidal category||linear type theory/quantum computation|
|proof net||string diagram||quantum circuit|
|(absence of) contraction rule||(absence of) diagonal||no-cloning theorem|
|synthetic mathematics||domain specific embedded programming language|
In logic, decidable refers to the question of whether there is an effective method for deciding membership in a set of formulas (or judgments in type theory). Here we take an effective method to be given by any of the equivalent formal characterizations (general recursion?, Turing machine?s, lambda calculus) that according to the Church-Turing thesis capture the informal notion.
Sometimes decidable is also used in another sense, namely that of independent statement?, according to which a logical theory decides a formula if it proves the formula or its negation (see at decidable proposition), and according to which a formula is undecidable (independent) if the theory in question proves neither the formula nor its negation. This is the sense in which the continuum hypothesis in undecidable from the axioms of ZFC and in which the consistency statement? of a sufficiently strong, recursively enumerated theory is undecidable in (independent of) that theory, according to Gödel’s second incompleteness theorem?. To avoid confusion, the preferred term to use here is independent?.
A logical system is decidable if there is an algorithm deciding whether a given formula is a theorem of the system.
A theory is a set of formulas closed under logical consequence (in some logical system, usually first order logic with a given signature). A theory is decidable if there is an algorithm (effective method) deciding whether a formula is a member of the theory of not. In the usual case where the theory is presented from a list of axioms, the question is whether the formula is deducible from the axioms.
Examples of decidable theories include:
Examples of undecidable theories include:
Type theory gives rise a number of decision problems, and it is generally desirable that these are solvable.
Type checking? refers to the problem whether the judgment is derivable in a given type theory. For instance, intensional type theory has decidable type checking, but extensional type theory, which adds the rule of equality reflection?, does not. For an exposition of this result, see the thesis of Hofmann.
In more expressive type theories, we can also ask whether judgmental equality (also called computational or definitional equality) is decidable. Since deciding the judgmental equality is often a prerequisite for deciding type checking, systems with decidable type checking often have decidable judgmental equality.
Typeability? refers to the problem of deciding for a given term whether it inhabits some type. Simple type theory has decidable typeability, and the programming language ML?, which features a weak form of polymorphism, let polymorphism?, also has decidable typeability.
dependent type theory has undecidable typeability.
Type inhabitation? refers to the problem of deciding for a given type whether there is a term that inhabits it. Under the propositions-as-types correspondence, this incorporates the question of the decidability of the corresponding logic since a proposition is provable if and only if the the type of its proofs is inhabited.
Wikipedia, Decidablility (logic)
Martin Hofmann, Extensional concepts in intensional type theory, Ph.D. dissertation, University of Edinburgh (1995). (link)