Suggest edit — mathematics

Title

Name

Note

---
title: "mathematics"
type: concept
related: [Turing Machinea, Alphabet]
source: https://www.jemoka.com/posts/kbhmathematics/
confidence: high
status: active
---

hehehe
formal system a formal system describes a formal language for&hellip;
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 &ldquo;$M$ accepts $w$&rdquo;
&ldquo;true statements $\mathcal{F}$&rdquo; 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 &ldquo;interesting&rdquo; if:
mathematical statements that can be precisely described in English should be expressible in $\mathcal{F}$ proofs have to be &ldquo;convincing&rdquo;: 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) if $M$ accepts $w$, then there is a proof $P$ in $F$ of $S_{M,w}$ consistent &ldquo;proof in $\mathcal{F}$ implies truth in $\mathcal{F}$&rdquo;
A formal system is &ldquo;consistent&rdquo;/&ldquo;sound&rdquo; if no false statement has a valid proof in $\mathcal{F}$
complete &ldquo;truth in $\mathcal{F}$ implies proof in $\mathcal{F}$&rdquo;
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&rsquo;s Theorem tells us that:
Godel&rsquo;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&rsquo;s define a Turing machine $G(x)$, for which we&hellip;
obtain own description $G$ (recursion) construct statement $S&rsquo; = \neg S_{G, \varepsilon}$ search for a proof of $S&rsquo;$ in $\mathcal{F}$ over all finite-length strings accept if a proof is found
Claim: S&rsquo; basically says &ldquo;there&rsquo;s no proof of S&rsquo; in $\mathcal{F }$&rdquo;. This is another diagonalization argument; if $S&rsquo;$ is false, we have a contradiction; if $S&rsquo;$ is true, then $S_{G, \epsilon}$ returned false, meaning $G$ doesn&rsquo;t accept $\epsilon$, meaning we weren&rsquo;t able to find a proof in $\mathcal{F}$ for $S&rsquo;$. So the proof of $S&rsquo;$ mustn&rsquo;t be in $\mathcal{F}$.
Godel&rsquo;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&rsquo; = \neg S_{G,\epsilon}$ from above which is true but has no proof in $\mathcal{F}$.
Observe that $G$ doesn&rsquo;t accept $\epsilon$ if and only if there&rsquo;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&rsquo;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&rsquo;s a proof in $\mathcal{F}$ of $S$, or there&rsquo;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