Topoi are closely related to intuitionistic type theories. Such a theory is equipped with certain types, terms, and theorems.
Among the types there should be a type Ω for truth-values, a type N for natural numbers, and, for each type A, a type ℘(A) for all sets of entities of type A.
Among the terms there should be in particular:
The set of theorems should contain certain obvious axioms and be closed under certain obvious rules of inference, neither of which will be spelled out here.
At this point the reader may wonder what happened to the usual logical symbols. These can all be defined—for example, universal quantification∀x ∊ Aϕ(x) as {x ∊ A|ϕ(x)} = {x ∊ A|x = x} and disjunctionp ∨ q as ∀t ∊ Ω((p ⊃ t) ⊃ ((q ⊃ t) ⊃ t)). For a formal definition of implication see formal logic.
In general, the set of theorems will not be recursively enumerable. However, this will be the case for pure intuitionistic type theory ℒ0, in which types, terms, and theorems are all defined inductively. In ℒ0 there are no types, terms, or theorems other than those that follow from the definition of type theory. ℒ0 is adequate for the constructive part of the usual elementary mathematics—arithmetic and analysis—but not for metamathematics, if this is to include a proof of Gödel’s completeness theorem, and not for category theory, if this is to include the Yoneda embedding of a small category into a set-valued functor category.
Zenos-paradox-illustrated-by-Achilles-racing-a-tortoiseFigure 1: Zeno’s paradox, illustrated by Achilles racing a tortoise.[Credits : Encyclopædia Britannica, Inc.]
Contrasting-triangles-in-Euclidean-elliptic-and-hyperbolic-spacesFigure 2: Contrasting triangles in Euclidean, elliptic, and hyperbolic spaces.[Credits : Encyclopædia Britannica, Inc.]
Link to this article and share the full text with the readers of your Web site or blog-post.
If you think a reference to this article on "foundations of mathematics" will enhance your Web site,
blog-post, or any other web-content, then feel free to link to this article,
and your readers will gain full access to the full article, even if they do not subscribe to our service.
You may want to use the HTML code fragment provided below.
We welcome your comments. Any revisions or updates suggested for this article will be reviewed by our editorial staff. Contact us here.
Regular users of Britannica may notice that this comments feature is less robust than in the past. This is only temporary, while we make the transition to a dramatically new and richer site. The functionality of the system will be restored soon.