3 papers
math.LO2024
Extensional realizability and choice for dependent types in intuitionistic set theory
Emanuele Frittaion
In "Extensional realizability for intuitionistic set theory", we introduced an extensional variant of generic realizability, where realizers act extensionally on realizers, and sho…
math.LO2022
A note on fragments of uniform reflection in second order arithmetic
Emanuele Frittaion
We consider fragments of uniform reflection for formulas in the analytic hierarchy over theories of second order arithmetic. The main result is that for any second order arithmetic…
math.LO2021
Completeness of the primitive recursive -rule
Emanuele Frittaion
Shoenfield's completeness theorem (1959) states that every true first order arithmetical sentence has a recursive -proof encodable by using recursive applications of the -rul…