This is the script discussed in the video at

Gödel arithmetization and the anti-classical Church's thesis

Outlook for this video:

On the arithmetization of proof
On Gödel incompleteness with emphasis on quantifiers
Note on Existence and Disjunction property
Note on the failure of the Least Number Principle
Kleene predicate and Halting problems
Anti-classical semnatics and constructive schools
Outlook on Brouwerian continuity

A simple formal logic system

I'll formulate a small Hilbert system framework to make sense of the computable inconsistency checking function later.

Axioms

(For any propositions $\varphi, \psi $ and also, below, $\chi$)

Axioms ${\mathsf{A1}}$:

$\varphi \to (\psi \to \varphi)$

Axioms ${\mathsf{A2}}$:

$(\varphi \to (\psi \to \chi)) \to ((\varphi \to \psi) \to (\varphi \to \chi))$

(Those are two of the standard logic, ones that only use implications.)

Inference rule (Modus Ponens, MP)

From $\varphi$ and $\varphi \to \psi$, infer $\psi$, i.e.

$\dfrac{\varphi \qquad \varphi \to \psi}{\psi}$

Small set of propositional variables

$P$

$\bot$

Example proof

tl;dr a constructive Hilbert proof of $P \to P$ as a finite sequence $\langle \varphi_1,\varphi_2,\varphi_3,\varphi_4,\varphi_5\rangle$ where each line is either an axiom instance A1/A2 or obtained by MP.

$\varphi_1 := P \to (P \to P)$

Justification: ${\mathsf{A1}}$ with $\varphi := P$, $\psi := P$.

$\varphi_2 := P \to ((P \to P) \to P)$

Justification: ${\mathsf{A1}}$ with $\varphi := P$, $\psi := (P \to P)$.

$\varphi_3 := (P \to ((P \to P) \to P)) \to ((P \to (P \to P)) \to (P \to P))$

Justification: ${\mathsf{A2}}$ with $\varphi := P$, $\psi := (P \to P)$, $\chi := P$.

$\varphi_4 := (P \to (P \to P)) \to (P \to P)$

Justification: ${\mathsf{MP}}$ from lines 2 and 3.

$\varphi_5 := P \to P$

Justification: ${\mathsf{MP}}$ from lines 1 and 4.

(Reminder: ${\mathsf{A1}}$ is $\varphi \to (\psi \to \varphi)$ and axioms ${\mathsf{A2}}$ is $(\varphi \to (\psi \to \chi)) \to ((\varphi \to \psi) \to (\varphi \to \chi))$. ${\mathsf{MP}}$ you should know.)

When is a sequence a valid proof?

Let $\pi = (\varphi_1,\dots,\varphi_n)$ be a finite sequence of formulas. We say $\pi$ is a valid proof sequence iff for each $i \in {1,\dots,n}$, either:

There exist formulas $\alpha,\beta$ with $\varphi_i = \alpha \to (\beta \to \alpha)$, or there exist formulas $\alpha,\beta,\gamma$ with $\varphi_i = (\alpha \to (\beta \to \gamma)) \to ((\alpha \to \beta) \to (\alpha \to \gamma))$,

(This is the axiom case, in our case that's ${\mathsf{A1}}$ and ${\mathsf{A2}}$)

or:

There exist indices $j,k < i$ such that $\varphi_k = (\varphi_j \to \varphi_i)$. (In which case $\varphi_j$ is also there.)

(i.e. we got a previous $\varphi_j$ that also previously, in the language entailed our current $\varphi_i$) (This is the inference rule case, in our case, and as often that's ${\mathsf{MP}}$)

Coding

Let $({\mathrm{prime}}i){i \ge 1}$ be the increasing sequence of primes: $p_1 = 2, p_2 = 3, p_3 = 5, p_4 = 7, p_5 = 11,\dots$.

Let $(x_i)_{i=1} = {\vec x}$ be a finite sequence of numbers, and ${\mathrm{Len}}({\vec x})$ its length.

Define the embedding of a finite sequence of numbers (e.g. ${\mathbb N}{\ge 0}^{\ell}$) into a unique number (always ${\mathbb N}$) by ${\mathrm{inj}}({\vec x}) = \prod{i=1}^{{\mathrm{Len}}({\vec x})} {\mathrm{prime}}i^{x_i + 1}$. or ${\mathrm{inj}}({\vec x}) := \prod{i=1}^{{\mathrm{Len}}(x)} {\mathrm{prime}}i \cdot \prod{i=1}^{{\mathrm{Len}}({\vec x})} {\mathrm{prime}}_i^{x_i}$.

(The shift in exponents by $+1$ is so the length is recoverable without trailing-zero ambiguity. As with choice of primes/numbers, those are technicalities to ensure uniquness and no information loss - but are conceptually easy.)

So, e.g., ${\mathrm{inj}}(\langle 9001, {\mathrm{inj}}(\langle 5, 5, 10\rangle)\rangle) = 2^{9002}\cdot 3^{(2^{6}\cdot 3^{6}\cdot 5^{11})+1}$

Formula codes

For each propositional variable (we have two) let its code be some distinct prime. Define the coding of implication, between any primitive or composed propositions, by

$\mathrm{c}(\varphi \to \psi) ,:=, {\mathrm{inj}}(\langle 2, \mathrm{c}(\varphi), \mathrm{c}(\psi)\rangle) ,=, 2^3 \cdot 3^{\mathrm{c}(\varphi)+1}\cdot 5^{\mathrm{c}(\psi)+1}$. So e.g. a factor $2^3$ hints at the start of an implication, etc.

Note: Negation may be treated as abbreviation, so $\mathrm{c}(\neg \varphi) ,=, \mathrm{c}(\varphi \to \bot) ,=, {\mathrm{inj}}(\langle 2, \mathrm{c}(\varphi), \mathrm{c}(\bot)\rangle)$.

Our number choices are largely open, but shall be tuned to your fixed system, to avoid conflicting coding. In particular, our system had only two variables and one connective, the implication. So fix distinct primes $\mathrm{c}(P)$ resp. $\mathrm{c}(\bot)$ to e.g. $7$ resp. $11$.

Encoding a proof-sequence as one number

Given a finite sequence of formulas $\vec\pi = (\varphi_1,\dots,\varphi_n)$ define its code by ${\mathrm{inj}}(\langle\mathrm{c}(\varphi_1),\dots,\mathrm{c}(\varphi_n)\rangle)$ i.e. $\prod_{i=1}^{n} {\mathrm{prime}}_i^{\mathrm{c}(\varphi_i)+1}$.

Example use: The five-propositions proof above, $\vec\pi = (\varphi_1,\varphi_2,\varphi_3,\varphi_4,\varphi_5)$ In our coding, both proof sequences (no matter how short) and implications sequences of propositions and so as numbers have factors.

On unpacking

$\mathrm{inj}$ is injective but not all numbers $n\in {\mathbb N}$ will be sequences in our system. E.g. $10$, which has a factorization $2^1 \cdot 3^0 \cdot 5^1$ and so is a non-prime non-sequence. It's not anything recognized w.r.t. to our small Hilbert system. We have to, in various places, relativize to "if for $n$ there's a sequence of propositions $\vec\pi$, then $\to$ so and so.." But this is very checkable - it's only a technical inconvenience.

Computability

Not that $\mathrm{inj}$ is very computable, and extracting the $i$'s component is, as is the check "is $p$ a $\vec\pi$". Our axiom and inference rule list is finite and anything with primes up to a given number can be brute forced if needed. We really only need repeated division. Many components here will even be primitive recursive (not needing while-loops.)

For $S$ a proposition and $\vec\pi$ a sequence of propositions, the following are also computable functions, and in particular, is decidable

$\vec\pi$ is valid w.r.t. axioms/inference rules
$\vec\pi$ is a proof of $S$ in particular (the last element of $\vec\pi$ represents $S$)

(I describe a lot of this in words simply because introducing even more intermediate functions names that I'll not use later would not benefit this video.)

So define this computable predicate $\mathrm{IsProofOf}_T(n, \mathrm{c}(\varphi))$ as follows: Given any $n$ and a propositions $\varphi$, map embed the propositions in the number and then

decompose $n$,
check if it's a sequence of propositions $\vec\pi$ w.r.t. the language of our Hilbert system, and if so
check if that sequence moreover also a valid proof in our theory, and if so
and finally that the final component is the proposition $\varphi$ If all of this check out, the predicate on the inputs is true.

E.g. we already established $P\to P$ is provable, or in other words

$\exists (p\in {\mathbb N}). \mathrm{IsProofOf}_T(p, \mathrm{c}(P\to P))$.

Tangent: Gödel Incompleteness

$T \ \vdash\ G\ \leftrightarrow
( (\exists n. {\mathrm{IsProofOf}}_T!(n, \mathrm{c}(G))) \ \to
\exists n. {\mathrm{IsProofOf}}_T!(n, \mathrm{c}(\bot)) ).$

Roughly, read it as a proof-theory-wrapped variant of $T \ \vdash\ G\ \leftrightarrow$ "$G\to \bot$"

Intermezzo: Existence property

Note that if (in the metalogic discussing $T$) we know $\exists (q\in {\mathbb N}). \mathrm{IsProofOf}_T(q, \mathrm{c}(Q))$ then we know $T\vdash Q$.

Note that if I give you term (something like $SSSS0$ in an arithmetic theory $T$), then you can computably verify and a particular propositions $Q$, then you can check if $\mathrm{IsProofOf}_T$ holds.

Beware that we deal with two levels here (or more if I report this to you.) Homework: Ponder the other direction, i.e. ponder the strength or weakness of existence claims.

Related sidenote for latter (when we get to the Least Number Principle): Existence property for a theory $S$: $S\ \vdash\ \exists n. \psi(n)\implies\text{ exists a term }{\mathrm{n}}\text{ such that }S\ \vdash\ \psi({\underline{\mathrm{n}}})$

(Note: In a reasonable system, that's really an iff.)

Inconsistency checker

Consider now $\bot$ for $\varphi$ and define another computable function.

Let $\mathrm{IsBot}(n)$ ... $\mathrm{IsProofOf}_T(n, \mathrm{c}(\bot))$

and (which is of equivalent use, as everything is computable so far) translate this to a characteristic function,

$\chi_\bot(n) := \begin{cases} 1 & \text{if }\mathrm{IsBot}(n),\ 0 & \text{otherwise.} \end{cases}$

Constructive logic usually has $\bot$ as primitive and defines $\neg Q$ as $Q\to \bot$. In arithmetic, which we are able to do in the theories of interest here, we got $0$ and $1$ and anyway alternatively use $0=1$. Our theories of interest prove $(0=1)\leftrightarrow \bot$. In standard textbook notation, our $\mathrm{isBot}$/$\chi_\bot(n)$ is $\mathrm{Prf}(n, \ulcorner 0=1 \urcorner)$ and the $\ulcorner Q \urcorner$ do what we described with our $\mathrm{c}$ notation.

Gödel incompleteness

$\chi_\bot$ is w.r.t. a theory (and a proof calculus), so fix a theory $T$. E.g. $T = {\mathsf{ZFC}}$ ... or some theory with numbers/arithmetic

Define the arithmetized consistency claim for $T$ (Goldbach-type via, i.e. $\Pi_1^0$) ${\mathrm{Con}{\Pi_1^0}}$ ... $\forall n. \chi\bot(n) = 0$

With ${\mathsf {IQL}}\ \vdash\ \neg\exists(x\in A).(x\in B),,,\leftrightarrow,,,\forall (x\in A).\neg(x\in B)$ that's also ${\mathrm{InCon}{\Sigma_1^0}} \leftrightarrow \exists n. \chi\bot(n) = 1$ with ${\mathrm{Con}{\Pi_1^0}}$ ... $\neg {\mathrm{InCon}{\Sigma_1^0}}$

Note: Any such $T$ also has polynomials $p$ (theory-specific) such that existence of zero's is independent: ${\mathrm{Con}_{\Pi_1^0}}, \leftrightarrow, \exists n. p(n)\neq 0$

If $T$ consistent, then it doesn't prove $\bot$. If it's sound, then $T$ also doesn't claim wrongly. $T\ \nvdash\ {\mathrm{InCon}_{\Sigma_1^0}}$

And as per Gödel: $T\ \nvdash\ {\mathrm{Con}{\Pi_1^0}}$ or $T\ \nvdash\ \neg{\mathrm{InCon}{\Sigma_1^0}}$

Disjunction property

If our logic is classical, then however (by one axiomatic step)

$T\ \vdash\ {\mathrm{InCon}{\Sigma_1^0}} \lor \neg{\mathrm{InCon}{\Sigma_1^0}}$ as well as $T\ \vdash\ {\mathrm{Con}{\Pi_1^0}} \lor \neg{\mathrm{Con}{\Pi_1^0}}$

For a theory with the arithmetical disjunction property ${\mathsf{T}}\ \vdash\ A\lor B$ $\iff$ (${\mathsf{T}}\ \vdash A$ or ${\mathsf{T}}\ \vdash\ B$ )

In words (constructive reading of propositions): "If the theory claims either $A$ or $B$ is provable, then indeed either $A$ or $B$"

For many theory theories (${\mathsf{HA}}$, ${\mathsf{CZF}}$, etc.), this is metalogically provable. In turn,

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

This is how some classical principles ($\mathrm{PEM}$, in fact $\mathrm{WPEM}$) fail. Indeed even e.g. $\mathrm{WLPO}$ fails.

That said, for all $Q$, ${\mathsf{HA}}\ \vdash\ \neg\neg(Q\lor \neg Q)$

Least number principle

Strong induction classically proves the ${\mathrm {LNP}}$: $\exists n. Q(n) \to \exists m. ( Q(m),\land, \forall(k < m). \neg Q(k) )$

Use with $Q(n)$ as $n=1\lor(n=0\land {\mathrm{Con}{\Pi_1^0}})$. Seen to be equivalent to ${\mathsf{PEM}}$ for ${\mathrm{Con}{\Pi_1^0}}$.

Assume now theory with a form of comprehension (e.g., set theory and similarly in second order logic): I.e. predicates $Q$ translate to set $A_Q = {x\in X\mid Q(x)}$. Then $Q(x)\leftrightarrow x\in A_Q$.

The above $Q$ corresponds to the subset of ${0,1}$ given as ${n\in {0}\mid {\mathrm{Con}_{\Pi_1^0}}}\cup{1}$.

Note how this is a very concise demonstration showing how classical theories with comprehension violate the Existence Property

So constructive set theory doesn't prove $\omega$ to be well-ordered. (And so you rather define ordinals in terms of transitivity.)

That said, for all $Q$, ${\mathsf{HA}}\ \vdash\ \neg\neg{\mathrm {LNP}}$

Halting problem

Here we pass on to the Kleene predicate $T_1(e, x, n)$: Function given by code $e\in{\mathbb N}$, when ran with input $x\in{\mathbb N}$, halts with history $n\in{\mathbb N}$. And from $n$ you can read off $y$ in those formalizations.

Vaguely, think of the previous situation as having chosen a fixed/single proof checking routine $e$ (what we used to define $\chi_\bot(n)$, I wasn't super explicit) and were only interested in the fixed/single proposition $x$. (Above that was $\mathrm{c}(\bot)$, a prime even.)

$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.

So there are no total recursive functions deciding membership in those sets of pairs. I.e., e.g., there's no total program $\begin{cases} 1 & \text{if }\exists n. T(e, e, n),\ 0 & \text{otherwise.} \end{cases}$

Since ${\mathsf{HA}}$ respects computable semantics, we get the following: With ${\mathrm{H}{\Sigma_1^0}} := \exists n. T(e, e, n)$ ${\mathrm{L}{\Pi_1^0}} := \neg {\mathrm{H}_{\Sigma_1^0}}$

we have the negative metalogical results

${\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)$

Classical (before going anti-classical)

Define the function graph $G_Q = { \langle x, y\rangle\in {\mathbb N}\times{0,1} \mid (y=1 \land Q(x)) \lor (y=0 \land \neg Q(x)) }$ For any $x$, $Q(x)\leftrightarrow \langle x, 1\rangle\in G_Q$ $\neg Q(x)\leftrightarrow \langle x, 0\rangle\in G_Q$ By consistency, $\forall x. \neg (\langle x, 1\rangle\in G_Q\land \langle x, 0\rangle\in G_Q)$

$(Q(x)\lor \neg Q(x)) \leftrightarrow \exists(y\in {0,1}). \langle x, y\rangle \in G_Q$ Indeed, by consistency, $(Q(x)\lor \neg Q(x)) \leftrightarrow \exists!(y\in {0,1}). \langle x, y\rangle \in G_Q$ (Note: In set theory, "functions" are their function graph, there's no distinction. In other framework you'd need an axiom of non-choice to pass from one to the other.)

So classically, every set $A_Q$/predicate $Q$ gives rise to a so called characteristic function. I.e. all total relations (predicates, sets of pairs) we can describe also give rise to a (potentially "hyper-computing") function. The other direction is trivial, with comprehension, ever function $f\in{0,1}^X$ injects into ${\mathcal P}X$ as $f^{-1}{1}$. Constructively, apriori only the injection provably exists.

In particular, classically (e.g. in set theory or second order arihtmetic) $\exists n. T(e, e, n)$ defines a halting function. This one is not codable. However, $\exists n. T(e, e, n)$ is not a show-stopper for "functions" in classical logic.

Formal Church's thesis

${\mathrm{CT}_0}$:

$(\forall x. \exists y. R(x,y)); \to; \exists e.(\forall x. \exists y. \exists n. R(x, y)\land T_1(e, x, n)\land U(n, y))$

"All relations $R$ can be pinned down to a total functions - and a computable one."

Trivial example: $R={\langle 3,12\rangle,\langle 6,15\rangle,\langle 6,11\rangle,\langle 7,13\rangle}$ contains the function $\begin{cases} 12 & \text{if } x=3,\ 11 & \text{if } x=6,\ 13 & \text{otherwise.} \end{cases}$ and I could code this up in python.

(Contrapositive: Provable absence of a computable function realizing a predicate means totality isn't provable at all.)

${\mathsf{HA}}$ is consistent with ${\mathrm{CT}_0}$.

and

${\mathsf{HA}}+{\mathrm{CT}_0}\vdash \neg\forall e.\ (\neg\exists n. T(e, e, n))\lor\neg(\neg\exists n. T(e, e, n))$

This is math in the Markovian school. So here $\mathrm{PEM}$ is not just failing to hold, it's rejected in that it can't be adopted anymore.

Motivation for the next video on Brouwerian continuity principles

While the constructive framework was agnostic about ${0,1}^{\mathbb N}$ contra the same framework with $\mathrm {PEM}$, now in the anti-classical system some predicates are ruled out from entailing a corresponding function existence.

This gives a semantic explanation for the classically just false. "All functions ${\mathbb N}^{\mathbb N}$ are computable" All are computable, not because some non-computable functions are turned computabe, but because the non-computable functions aren't in there in the first place.

Similary, in the Brouwer school: "All functions ${\mathbb R}^{\mathbb R}$ are continuous."

Brouwerian principle that all ${\mathbb N}^{\mathbb N}\to{\mathbb N}$ are locally constant. Breaks $\mathrm{WLPO}$ (and so $\mathrm{PEM}$) but also ${\mathrm{CT}_0}$. So those are competing worlds.

(Albeit it's consistent with a double-negated variant of ${\mathrm{CT}_0}$.)

Nikolaj-K/churchs_thesis.md

Select an option

No results found