80-614 Formal Methods: Incompleteness
6 units, Carnegie Mellon University
The material of this Mini and the Formal Mini 4 Undecidability is, for some, a perfect combination of logical work with mathematical rigor and methodological reflection with historical background. At its center is the notion of a formal theory. Explicating formality with the help of computability the topic of Mini 4, we will prove two central theorems Gdels First and Second Incompleteness Theorems. These theorems answer two broad informal questions Can mathematical truth be fully captured by formal theories and Can the consistency of a formal theory be proved by elementary mathematical means To address these questions, Mini 1 is divided into two parts. Part 1 introduces axiomatic set theory ZF as a rigorous framework that allows the representation of most of contemporary mathematical practice Part 2 shows how the precise description of that framework can be represented in ZF and then exploits this representability to prove the Incompleteness Theorems. The core developments in this Mini are mathematical, but they have been shaped by broad methodological constraints, for example, the insistence on the decidability of the concept of proof. The course presents these concepts and some of their history, so that you understand not only the mathematical techniques and results but also the fundamental methodological issues. The results put a theoretical limit on developing mathematics in strict formalisms thus, answering the above informal questions by No and No.
Prerequisites: none listed
Courseweave needs JavaScript to show sections, workloads and planning tools.