Sign in

A constructive proof of dependent choice in classical arithmetic via memoization

By Étienne Miquey
In a recent paper, Herbelin developed dPA\({^\omega}\), a calculus in which constructive proofs for the axioms of countable and dependent choices could be derived via the memoization of choice functions. However, the property of normalization (and therefore the one of soundness) was only conjectured. The difficulty for the proof of... Show more
March 18, 2019
=
0
Loading PDF…
Loading full text...
Similar articles
Loading recommendations...
=
0
x1
A constructive proof of dependent choice in classical arithmetic via memoization
Click on play to start listening