# Questions tagged [realizability]

Realizability is a collection of methods in proof theory used to study constructive proofs and extract additional information from them.

6
questions

**9**

votes

**1**answer

257 views

### Computability-theoretic results relevant to realizability

This may be a very naive question which only reflects my failure at literature search, but:
Although realizability (in its original form at least) is grounded in computability, the details of ...

**8**

votes

**1**answer

241 views

### Kleene realizability in Peano arithmetic

For completeness of MathOverflow and for clarity of the question, I will first recall a few things, including the the definition of Kleene realizability: experts can jump directly to the question ...

**5**

votes

**1**answer

146 views

### How is this HA unprovable formula recursive realizable?

In Realizability: A Historical Essay [Jaap van Oosten, 2002], it is said that recursive realizability and HA provability do not concur, because although every HA provable closed formula is realizable, ...

**5**

votes

**0**answers

323 views

### Did Kleene constructively prove Brouwer's axioms?

Harvey Friedman's request on the FoM-forum for an overview of current intuitionistic foundations revived the following question, which I have been meaning to ask for five years. (I'm no expert on ...

**3**

votes

**0**answers

286 views

### A polytime feasible subuniverse of the Effective Topos

The effective topos is a well known universe of sets suitable for abstract computability, as it is build "from the ground up" via the classical notion of realisability by Kleene.
I have found a few ...

**13**

votes

**2**answers

1k views

### Why is Kleene's notion of computability better than Banach-Mazur's?

In this post about the difference between the recursive and effective topos, Andrej Bauer said:
If you are looking for a deeper explanation, then perhaps it is fair to say that the Recursive Topos ...