3 citations · 3 across the 2 of their papers we have counts for
4 papers
A Guide to Krivine Realizability for Set Theory
Richard Matthews
The method of realizability was first developed by Kleene and is seen as a way to extract computational content from mathematical proofs. Traditionally, these models only satisfy i…
Constructing the Constructible Universe Constructively
Richard Matthews, Michael Rathjen
We study the properties of the constructible universe, L, over intuitionistic theories. We give an extended set of fundamental operations which is sufficient to generate the univer…
Very large set axioms over constructive set theories
Hanul Jeon, Richard Matthews
We investigate large set axioms defined in terms of elementary embeddings over constructive set theories, focusing on and . Most previously studied lar…
Taking Reinhardt's Power Away
Richard Matthews
We study the notion of non-trivial elementary embeddings under the assumption that satisfies without Power Set but with the Collection Scheme. We sh…