Four freebies of constructive arithmetic
Channel: Nikolaj-K
Date: 2023-05-16

Sorry for rushing through the video a bit. Around 22:10 we have a failure of WPEM for an \exists-statement (\Sigma_1^0) that can be expressed as failure of PEM for a \forall-statement (\Pi_1^0). 
Meaning what's on the screen is correct there, not what I say in the summary sentence. Also, when talking of provability in relation to the arithmetized consistency proposition, I tacitly assume consistency and soundness of the theory at hand. I've also added 5 more lines or so to the Halting section, in the used text I go through, here: https://gist.github.com/Nikolaj-K/ed323cd4c1df63cd4a3a407de2e76a23
The videos discussed Gödel-Gentzen translation, Friedman translation, Markov's rule and principles, Harrop formula results, Kleene predicate, Incompleteness,  Church's rule, Heyting arithmetic, Weak limited principle of omniscience. All that good stuff.