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