Are you an EPFL student looking for a semester project?
Work with us on data science and visualisation projects, and deploy your project as an app on top of Graph Search.
Concept
Effective topos
Summary
In mathematics, the effective topos introduced by captures the mathematical idea of effectivity within the framework.
The topos is based on the partial combinatory algebra given by Kleene's first algebra . In Kleene's notion of recursive realizability, any predicate is assigned realizing numbers, i.e. a subset of . The extremal propositions are and , realized by and . However in general, this process assigns more data to a proposition than just a binary truth value.
A formula with free variables will give rise to a map in the values of which is the subset of corresponding realizers.
is a prime example of a realizability topos. These are a class of elementary topoi with an intuitionistic internal logic and fulfilling a form of dependent choice. They are generally not Grothendieck topoi.
In particular, the effective topos is . Other realizability topos construction can be said to abstract away the some aspects played by here.
The objects are pairs of sets together with a symmetric and transitive relation in , representing a form of equality. But the so called existence predicate can be empty, and so this is not generally reflexive.
Arrows amount to equivalence classes of functional relations appropriately respecting the defined equalities.
The classifier amounts to . The pair (or, by abuse of notation, just that underlying powerset) may be denoted as .
An entailment relation on makes it into a Heyting pre-algebra.
Such a context allows to define the appropriate lattice-like logic structure, with logical operations given in terms of operations of the realizer sets, making use of pairs and computable functions.
The terminal object is a singleton with trivial existence predicate (). The finite product respect the equality appropriately.
The classifier's equality is given through equivalences in its lattice.
Some objects exhibit a rather trivial existence predicate depending only on the validity of the equality relation "" of sets, so that valid equality maps to the top set and rejected equality maps to .
Official source
About this result
This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.