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

Loading full text...

Similar articles

Loading recommendations...

x1

A constructive proof of dependent choice in classical arithmetic via memoization

Click on play to start listening