nLab decidability

Contents

Context

Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory

logicset theory (internal logic of)category theorytype theory
propositionsetobjecttype
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
modalityclosure operator, (idempotent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels

semantics

Contents

Idea

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 machines, 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 is 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?.

Decidability of a logical system

A logical system is decidable if there is an algorithm deciding whether a given formula is a theorem of the system.

In this sense, propositional logic and monadic predicate logic? are decidable, whereas first-order logic and higher-order logic are undecidable

Decidability of a theory

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:

  • Peano arithmetic (considered as either a first-order or a second-order theory)
  • the first-order theory of groups

In the context of type theory

Type theory gives rise a number of decision problems, and it is generally desirable that these are solvable.

Type checking

In type theory, Type checking refers to the problem whether the judgment Γa:A\Gamma\vdash a \colon A 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 Hofmann 1995.

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.

Typability

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

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.

For simple type theory, type inhabitation is decidable, whereas it is undecidable for dependent type theory.

References

Last revised on June 6, 2023 at 05:38:18. See the history of this page for a list of all contributions to it.