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 \left\{(S,P) | P\text{ is a proof of }S\text{ in }F\right\} 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:

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