In this entry, we first give an overview of the most important aspects of intuitionistic type theory—a kind of “extended abstract”. It is meant for a reader who is already somewhat familiar with the theory. Section 2 on the other hand, is meant for a reader who is new to intuitionistic type theory but familiar with traditional logic, including propositional and predicate logic, arithmetic, and set theory. Here we informally introduce several aspects which distinguishes intuitionistic type theory from these traditional theories. In Section 3 we present a basic version of the theory, close to Martin-Löf’s first published version from 1972. The reader who was intrigued by the informality of Section 2 will now see in detail how the theory is built up. Section 4 then presents a number of important extensions of the basic theory. In particular, it emphasizes the central role of inductive (and inductive-recursive) definitions. Section 5 introduces the underlying philosophical ideas including the theory of meaning developed by Martin-Löf. While Section 5 is about philosophy and foundations, Section 6 gives an overview of mathematical models of the theory. In Section 7 finally, we describe several important variations of the core Martin-Löf “intensional” theory described in Section 3 and 4.3. Basic Intuitionistic Type Theory
3.1 Judgments
3.2 Judgment Forms
3.3 Inference Rules
3.4 Intuitionistic Predicate Logic
3.5 Natural Numbers
3.6 The Universe of Small Types
3.7 Propositional Identity
3.8 The Axiom of Choice is a Theorem
4. Extensions
4.1 The Logical Framework
4.2 A General Identity Type Former
4.3 Well-Founded Trees
4.4 Iterative Sets and CZF
4.5 Inductive Definitions
4.6 Inductive-Recursive Definitions
5. Meaning Explanations
5.1 Computation to Canonical Form
5.2 The Meaning of Categorical Judgments
5.3 The Meaning of Hypothetical Judgments
6. Mathematical Models
6.1 Categorical Models
6.2 Set-Theoretic Model
6.3 Realizability Models
6.4 Model of Normal Forms and Type-Checking
7. Variants of the Theory
7.1 Extensional Type Theory
7.2 Univalent Foundations and Homotopy Type Theory
7.3 Partial and Non-Standard Type Theory
7.4 Impredicative Type Theory
7.5 Proof Assistants
Bibliography
Academic Tools
Other Internet Resources
Related Entries
[size=30]1. Overview
We begin with a bird’s eye view of some important aspects of intuitionistic type theory. Readers who are unfamiliar with the theory may prefer to skip it on a first reading.
The origins of intuitionistic type theory are Brouwer’s intuitionism and Russell’s type theory. Like
Church’s classical simple theory of types it is based on the lambda calculus with types, but differs from it in that it is based on the propositions-as-types principle, discovered by Curry (1958) for propositional logic and extended to predicate logic by Howard (1980) and de Bruijn (1970). This extension was made possible by the introduction of indexed families of types (dependent types) for representing the predicates of predicate logic. In this way all logical connectives and quantifiers can be interpreted by type formers. In intuitionistic type theory further types are added, such as a type of natural numbers, a type of small types (a universe) and a type of well-founded trees. The resulting theory contains intuitionistic number theory (Heyting arithmetic) and much more.
The theory is formulated in natural deduction where the rules for each type former are classified as formation, introduction, elimination, and equality rules. These rules exhibit certain symmerties between the introduction and elimination rules following Gentzen’s and Prawitz’ treatment of natural deduction, as explained in the entry on
proof-theoretic semantics.
The elements of propositions, when interpreted as types, are called
proof-objects. When proof-objects are added to the natural deduction calculus it becomes a typed lambda calculus with dependent types, which extends Church’s original typed lambda calculus. The equality rules are computation rules for the terms of this calculus. Each function definable in the theory is total and computable. Intuitionistic type theory is thus a typed functional programming language with the unusual property that all programs terminate.
Intuitionistic type theory is not only a formal logical system but also provides a comprehensive philosophical framework for intuitionism. It is an
interpreted language, where the distinction between the
demonstration of a judgment and the
proof of a proposition plays a fundamental role (Sundholm 2012). The framework clarifies the Brouwer-Heyting-Kolmogorov interpretation of intuitionistic logic and extends it to the more general setting of intuitionistic type theory. In doing so it provides a general conception not only of what a constructive proof is, but also of what a constructive mathematical object is. The meaning of the judgments of intuitionistic type theory is explained in terms of computations of the canonical forms of types and terms. These informal, intuitive meaning explanations are “pre-mathematical” and should be contrasted to formal mathematical models developed inside a standard mathematical framework such as set theory.
This meaning theory also justifies a variety of inductive, recursive, and inductive-recursive definitions. Although proof-theoretically strong notions can be justified, such as analogues of certain large cardinals, the system is considered predicative. Impredicative definitions of the kind found in higher-order logic, intuitionistic set theory, and topos theory are not part of the theory. Neither is Markov’s principle, and thus the theory is distinct from Russian constructivism.
An alternative formal logical system for predicative constructive mathematics is Myhill and Aczel’s
constructive Zermelo-Fraenkel set theory (CZF). This theory, which is based on intuitionistic first-order predicate logic and weakens some of the axioms of classical Zermelo-Fraenkel Set Theory, has a natural interpretation in intuitionistic type theory. Martin-Löf’s meaning explanations thus also indirectly form a basis for CZF.
Variants of intuitionistic type theory underlie several widely used proof assistants, including NuPRL, Coq, and Agda. These proof assistants are computer systems that have been used for formalizing large and complex proofs of mathematical theorems, such as the Four Colour Theorem in graph theory and the Feit-Thompson Theorem in finite group theory. They have also been used to prove the correctness of computer software.
Philosophically and practically, intuitionistic type theory is a foundational framework where constructive mathematics and computer programming are, in a deep sense, the same. This point has been emphasized by Gonthier (2008) in the paper in which he describes his proof of the Four Colour Theorem:
[/size]
- اقتباس :
- The approach that proved successful for this proof was to turn almost every mathematical concept into a data structure or a program in the Coq system, thereby converting the entire enterprise into one of program verification.
[size]
[size=30]2. Propositions as Types[/size]
2.1 Intuitionistic Type Theory: a New Way of Looking at Logic?
Intuitionistic type theory offers a new way of analyzing logic, mainly through its introduction of explicit proof objects. This provides a direct computational interpretation of logic, since there are computation rules for proof objects. As regards expressive power, intuitionistic type theory may be considered as an extension of first-order logic, much as higher order logic, but predicative.
2.1.1 A Type Theory
Russell developed
type theory in response to his discovery of a paradox in naive set theory. In his ramified type theory mathematical objects are classified according to their
types: the type of propositions, the type of objects, the type of properties of objects, etc. When Church developed his
simple theory of types on the basis of a typed version of his lambda calculus he added the rule that there is a type of functions between any two types of the theory. Intuitionistic type theory further extends the simply typed lambda calculus with dependent types, that is, indexed families of types. An example is the family of types of
[ltr]nn[/ltr]-tuples indexed by
[ltr]nn[/ltr].
Types have been widely used in programming for a long time. Early high-level programming languages introduced types of integers and floating point numbers. Modern programming languages often have rich type systems with many constructs for forming new types. Intuitionistic type theory is a functional programming language where the type system is so rich that practically any conceivable property of a program can be expressed as a type. Types can thus be used as specifications of the task of a program.
2.1.2 An intuitionstic logic with proof-objects
Brouwer’s analysis of logic led him to an intuitionistic logic which rejects the law of excluded middle and the law of double negation. These laws are not valid in intuitionistic type theory. Thus it does not contain classical (Peano) arithmetic but only intuitionistic (Heyting) arithmetic. (It is another matter that Peano arithmetic can be interpreted in Heyting arithmetic by the double negation interpretation, see the entry on
intuitionistic logic.)
Consider a theorem of intuitionistic arithmetic, such as the division theorem
[/size]
[ltr]∀m,n.m>0⊃∃q,r.mq+r=n∀m,n.m>0⊃∃q,r.mq+r=n[/ltr]
[size]
A formal proof (in the usual sense) of this theorem is a sequence (or tree) of formulas, where the last (root) formula is the theorem and each formula in the sequence is either an axiom (a leaf) or the result of applying an inference rule to some earlier (higher) formulas.
When the division theorem is proved in intuitionistic type theory, we do not only build a formal proof in the usual sense but also a
construction (or
proof-object) “
[ltr]divdiv[/ltr]” which witnesses the truth of the theorem. We write
[/size]
[ltr]div:∀m,n:N.m>0⊃∃q,r:N.mq+r=ndiv:∀m,n:N.m>0⊃∃q,r:N.mq+r=n[/ltr]
[size]
to express that
[ltr]divdiv[/ltr] is a proof-object for the division theorem, that is, an element of the type representing the division theorem. When propositions are represented as types, the
[ltr]∀∀[/ltr]-quantifier is identified with the dependent function space former (or general cartesian product)
[ltr]ΠΠ[/ltr], the
[ltr]∃∃[/ltr]-quantifier with the dependent pairs type former (or general disjoint sum)
[ltr]ΣΣ[/ltr], the identity relation = with the type former
[ltr]II[/ltr] of proof-objects of identities, and the greater than relation
[ltr]>>[/ltr] with the type former
[ltr]GTGT[/ltr] of proof-objects of greater-than statements. Using “type-notation” we thus write
[/size]
[ltr]div:Πm,n:N.GT(m,0)→Σq,r:N.I(N,mq+r,n)div:Πm,n:N.GT(m,0)→Σq,r:N.I(N,mq+r,n)[/ltr]
[size]
to express that the proof object “
[ltr]divdiv[/ltr]” is a function which maps two numbers
[ltr]mm[/ltr] and
[ltr]nn[/ltr] and a proof
[ltr]pp[/ltr] that
[ltr]m>0m>0[/ltr] to a triple
[ltr](q,(r,s))(q,(r,s))[/ltr], where
[ltr]qq[/ltr] is the quotient and
[ltr]rr[/ltr] is the remainder obtained when dividing
[ltr]nn[/ltr] by
[ltr]mm[/ltr]. The third component
[ltr]ss[/ltr] is a proof-object witnessing the fact that
[ltr]mq+r=nmq+r=n[/ltr].
Crucially,
[ltr]divdiv[/ltr] is not only a function in the classical sense; it is also a function in the intuitionistic sense, that is, a program which computes the output
[ltr](q,(r,s))(q,(r,s))[/ltr] when given
[ltr]mm[/ltr],
[ltr]nn[/ltr],
[ltr]pp[/ltr]as inputs. This program is a term in a lambda calculus with special constants, that is, a program in a functional programming language.[/size]
Intuitionistic Type Theory
اليوم في 1:40 pm من طرف