[[
wikihub
]]
Search
⌘K
Explore
People
For Agents
Sign in
Explore
People
For Agents
Sign in
@jemoka / Jemoka Knowledge Base / raw/concept/kbhmathematics.md
Suggest edit
Cancel
Submit suggestion
Title
Name
Note
--- title: "mathematics" source: https://www.jemoka.com/posts/kbhmathematics/ --- 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) 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 diagonalization 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