Four freebies of constructive arithmetic

constructive_arithmetic_freebies.md

Test used in the video

https://youtu.be/-lPrjPHElik

=====four freebies of constructive arithmetic=====

Ref:

https://www.amazon.com/Constructivism-Mathematics-Studies-Logic-Foundations/dp/0444702660

====Gödel-Gentzen-translation====

https://en.wikipedia.org/wiki/Double-negation_translation

For arithmetic: All classically provable formulas are provable with $\neg\neg$ before every existential quantifier.

${\mathsf{PA}}\ \vdash\ \phi\iff {\mathsf{HA}}\ \vdash\ \phi^{\exists\to\neg\neg\exists}$

(Here this is particularly simple in arithmetic, as e.g. $\neg P$ when $\big(P\to (0=S0)\big)$, etc. Apart from arithmetic - which has no atomic formulas and disjunction isn't necessarily decidable -, you'd also have to put $\neg\neg$ before those things.)

===Pedestrian propositional minimal logic examples===

$\bullet$ Theorem: $\Big(\big(P\lor (P\to Q)\big)\to Q\Big)\to Q$ Proof: Assume $\big(P\lor (P\to Q)\big)\to Q$. Now by in-left this is stronger than $P\to Q$, but using that for in-right implies $Q$. QED. $\bullet$ Lemma: $\neg \neg (P\lor\neg P)$

$\bullet$ Theorem: $P\to((P\to Q)\to Q)$ Proof: Assume $P$. Now consider $\land$-form of modus ponens $(P\land (P\to Q))\to Q$. QED. $\bullet$ Lemma: $P\to\neg\neg P$

$\bullet$ Lemma: $\Big(\big((P\to Q)\to Q\big)\to R\Big) \to (P\to R)$ $\bullet$ Lemma's lemma: $(\neg \neg \neg P)\leftrightarrow \neg P$

$\bullet$ Bonus theorem: $\land$-form of modus ponens generalized non-contradiction $\neg(P\land \neg P)$ $\bullet$ Bonus alternative proof of double-negated PEM when taking de Morgan for granted: Consider $\neg((\neg P)\land \neg (\neg P))$

====Harrop formulas====

https://en.wikipedia.org/wiki/Harrop_formula

Very broad generalization of the "Lemma's lemma" above: Not only $Q$ but also $P\to Q$ "behaves" classically as long as the conclusion $Q$ has no existential quantifier. (Antecedent can be anything, also be universal quantification.)

====$\Pi_2^0$-conservativity====

https://en.wikipedia.org/wiki/Friedman_translation

$\varphi$ ... any quantifier-free predicate.

${\mathsf{PA}}\ \vdash\ \forall n.\exists m. \varphi(n, m)\iff {\mathsf{HA}}\ \vdash\ \forall n.\exists m. \varphi(n, m)$

I.e. the theories make the same computable statements about computable relations. E.g. predicates having nothing to do with infinity are all classical:

${\mathsf{HA}}\ \vdash\ \forall n. \cdots \forall m.,\varphi(n, \dots, m)\lor\neg\varphi(n, \dots, m)$

====Markov Rule====

https://en.wikipedia.org/wiki/Markov%27s_principle

${\mathsf{HA}}\ \vdash\ \Big(\forall m. \phi(m)\lor\neg \phi(m)\Big)\land\Big(\neg\neg\exists m. \phi(m)\Big)\ \ \ \iff\ \ \ {\mathsf{HA}}\ \vdash\ \exists m. \phi(m)$

"Decidable formulas have simple behaved existence" "Numbers that are not absent will eventually be found"

====So what's actually not provable?====

Any theory with numbers has polynomials $p$ (theory-specific) such that existence of zero's is independent.

${\mathrm{Con}_{\Pi_1^0}} := \neg\exists n. p(n)=0$

Roughly, the (primitive recursive) $p$ on $n$ represents the job of checking that whether $n$ is an (encoded) proof of $0=1$.

This is of Goldbach-type (i.e. a pure $\forall$-sentence) via switching of commutators (valid in intuitionistic predicate logic) ${\mathsf {IQL}}\ \vdash\ \neg\exists(x\in A).(x\in B) \leftrightarrow \forall(x\in A).\neg(x\in B)$

${\mathsf{ZFC}}\ \nvdash\ {\mathrm{Con}_{\Pi_1^0}}$

${\mathsf{ZFC}}\ \nvdash\ \neg {\mathrm{Con}_{\Pi_1^0}}$

(For the latter we assume soundness of ZFC.)

Therefore (maybe see future video on Disjunction property of ${\mathsf{HA}}$, ${\mathsf{CZF}}$, etc.)

${\mathsf{HA}}\ \nvdash\ {\mathrm{Con}{\Pi_1^0}}\lor \neg {\mathrm{Con}{\Pi_1^0}}$

(Note: Each theory of course has its own ${\mathrm{Con}_{\Pi_1^0}}$. Formally one shouldn't reusing the exact notation for ${\mathsf{ZFC}}$, given we want to discuss ${\mathsf{HA}}$ here.)

This breaks logical schemas. E.g. $\mathrm{PEM}$, in fact $\mathrm{WPEM}$, in fact $\mathrm{WLPO}$.

====More generally speaking... (Halting problems)====

https://en.wikipedia.org/wiki/Halting_problem#Formalization

https://en.wikipedia.org/wiki/Kleene%27s_T_predicate

https://en.wikipedia.org/wiki/Computably_enumerable_set

$H={\langle e, x\rangle\in{\mathbb N}\times{\mathbb N} \mid \exists n. T_1(e, x, n)}$

Theorem (Turing): $H$ is only computably enumerable (c.e.)

${\mathbb N}\times{\mathbb N}\setminus H$ is not even c.e.

Define special non-halting claim:

$ \mathrm{H}_{\Sigma_1^0} := \exists n. T_1(e, e, n) $

$ \mathrm{L}{\Pi_1^0} := \neg \mathrm{H}{\Sigma_1^0} $

${\mathsf{HA}}\ \nvdash\ \forall e.\ {\mathrm{H}{\Sigma_1^0}}(e)\lor\neg{\mathrm{H}{\Sigma_1^0}}(e)$

${\mathsf{HA}}\ \nvdash\ \forall e.\ {\mathrm{L}{\Pi_1^0}}(e)\lor\neg{\mathrm{L}{\Pi_1^0}}(e)$

Both are classical tautologies, but Turing: There are no total recursive functions deciding these.

(Closely related to Gödel I, although that result wasn't with a parameter $e\in{\mathbb N}$.)

$\bullet$ ${\mathrm{PEM}}$ implies: For predicates " $ {\mathbb N} \to \text{Prop} $" and any $e\in{\mathbb N}$, the propositions are bivalent.

Assuming function choice in ${\mathbb N} \times {0,1} $: All total relations mapping to a unique bit give rise to a (potentially "hyper-computing") function.

$\bullet$ Formal Church's thesis $ \mathrm{CT}_0 $ implies: All total relations contain a recursive function. Contrapositive of ${\mathrm{CT}_0}$ implies: Provable absence of a recursive function means totality isn't provable at all.

$ \mathrm{PEM} $ and $ \mathrm{CT}_0 $ don't go together:

$ \mathsf{HA} $ is consistent with $ \mathrm{CT}_0 $. and $ \mathsf{HA} + \mathrm{CT}_0 \vdash \neg\forall e.\ \big(\neg\exists n. T_1(e, e, n)\big) \lor \neg\big(\neg\exists n. T_1(e, e, n) \big) $

(not just failing but rejected)