mathematics

hehehe

formal system

a formal system describes a formal language for…

writing finite mathematical statements
have a definition of what statements are true
has a definition of a proof of a statement

examples

Every Turing Machine $M$ defines some formal system $\mathcal{F}$ such that $\Sigma^{*}$ string $w$ represents the statement “$M$ accepts $w$”

“true statements $\mathcal{F}$” is $L(M)$
a proof that $M$ accepts $w$ can be defined to be an accepting computation history on $M$ for $w$

interesting

a formal system $\mathcal{F}$ is “interesting” if:

mathematical statements that can be precisely described in English should be expressible in $\mathcal{F}$
proofs have to be “convincing”: a turing machine can check that a proof of a theorem is correct
simple proofs that can be precisely described in English should be expressible in $\mathcal{F}$

given $(M,w)$, there is a computable $S_{M,w}$ in $\mathcal{F}$ such that $S_{M,w}$ is true in $\mathcal{F}$ if and only if $M$ accepts $w$
the set $\qty {(S,P) | P\text{ is a proof of }S\text{ in }F}$ should be decidable, because we can just run it
if $S$ is in $F$ and there is a proof of $S$ describable as a computation, then there is a proof of $S$ in $\mathcal{F}$ (i.e. its just the computational path)
1. if $M$ accepts $w$, then there is a proof $P$ in $F$ of $S_{M,w}$

consistent

“proof in $\mathcal{F}$ implies truth in $\mathcal{F}$”

A formal system is “consistent”/“sound” if no false statement has a valid proof in $\mathcal{F}$

complete

“truth in $\mathcal{F}$ implies proof in $\mathcal{F}$”

A formal system $\mathcal{F}$ is complete if every true statement has a valid proof in $\mathcal{F}$

Limitations of Mathematics

For every consistent and interesting $\mathcal{F}$, Godel’s Theorem tells us that:

Godel’s incompleteness

There are mathematical statements in $\mathcal{F}$ which are true but cannot be proven in $\mathcal{F}$.

Proof: Let $S_{M,w}$ in $\mathcal{F}$ be true IFF $M$ accepts $w$. Let’s define a Turing machine $G(x)$, for which we…

obtain own description $G$ (recursion)
construct statement $S’ = \neg S_{G, \varepsilon}$
search for a proof of $S’$ in $\mathcal{F}$ over all finite-length strings

accept if a proof is found

Claim: S’ basically says “there’s no proof of S’ in $\mathcal{F }$”. This is another nationalization argument; if $S’$ is false, we have a contradiction; if $S’$ is true, then $S_{G, \epsilon}$ returned false, meaning $G$ doesn’t accept $\epsilon$, meaning we weren’t able to find a proof in $\mathcal{F}$ for $S’$. So the proof of $S’$ mustn’t be in $\mathcal{F}$.

Godel’s consistency

the consistency of interesting and consistent $\mathcal{F}$ itself cannot be proven in $\mathcal{F}$

Suppose we can prove $\mathcal{F}$ is consistent in $\mathcal{F}$. We constructed $S’ = \neg S_{G,\epsilon}$ from above which is true but has no proof in $\mathcal{F}$.

Observe that $G$ doesn’t accept $\epsilon$ if and only if there’s no proof of $\neg S_{G,\varepsilon}$ in $\mathcal{F}$. Yet, if we can proof $\mathcal{F}$ is consistent within $\mathcal{F}$, then we can prove $\neg S_{G,\varepsilon}$: since $G(x)$ accepts if $\neg S_{G,\varepsilon}$ is found, if $G(\varepsilon) = true \implies S_{G,\varepsilon} = true \implies \neg S_{G,\varepsilon}$, but they can’t be both true. So $\neg S_{G, \varepsilon}$ is true.

This contradicts the previous theorem.

Church-Turing undecidability

The problem of checking whether or not a given statement in $\mathcal{F}$ has a proof is undecidable.

Consider:

\begin{equation} PROVABLE_{F} = \qty {S | \text{there’s a proof in $\mathcal{F}$ of $S$, or there’s a proof in $\mathcal{F}$ of $\neg S$}} \end{equation}

suppose this is decidable with a Turing Machine $P$; then we can decide $A_{TM}$ using the following procedure:

on input $(M,w)$, run the TM $P$ on input $S_{M,w}$
if $P$ accepts, then look at all proofs in $\mathcal{F}$, then we know we can iterate and find the proof
so if we found $S_{M,w}$ is found, then accept
otherwise, for $\neg S_{M,w}$, reject
if $P$ rejects, we know its not provable, so we reject