⁇Incompleteness and Undecidability Unit 1 – Mathematical Logic & Formal Systems Intro

Key Concepts and Definitions

• Mathematical logic studies the formal principles of deduction and the foundations of mathematics
• Formal systems consist of a set of symbols, formation rules, axioms, and inference rules used to derive theorems
• Soundness ensures that a formal system proves only valid statements, while completeness guarantees that all valid statements can be proven
• Consistency means a formal system cannot prove both a statement and its negation
• Decidability refers to the existence of an algorithm that can determine the truth or falsity of any well-formed formula in a formal system
• Incompleteness theorems, proven by Kurt Gödel, demonstrate the limitations of consistent formal systems containing arithmetic
  • First Incompleteness Theorem states that any consistent formal system containing arithmetic is incomplete
  • Second Incompleteness Theorem shows that a consistent formal system cannot prove its own consistency

Historical Context and Development

• Mathematical logic emerged from the works of philosophers and mathematicians in the late 19th and early 20th centuries
• Gottlob Frege developed first-order predicate calculus and attempted to formalize arithmetic using logic in his Begriffsschrift (1879)
• Bertrand Russell discovered Russell's Paradox (1901), exposing inconsistencies in Frege's system and prompting the development of type theory
• David Hilbert's program sought to establish the consistency and completeness of mathematics using finitary methods
• Kurt Gödel's Incompleteness Theorems (1931) demonstrated the limitations of Hilbert's program and the inherent incompleteness of formal systems containing arithmetic
• Alonzo Church and Alan Turing independently developed the notion of computability and proved the undecidability of the Entscheidungsproblem (decision problem) in the 1930s
• The development of mathematical logic laid the foundations for computer science and the theory of computation

Formal Systems: Structure and Components

• Formal systems are composed of a set of symbols, formation rules, axioms, and inference rules
• Symbols include constants, variables, function symbols, and predicate symbols used to construct well-formed formulas (wffs)
• Formation rules specify how symbols can be combined to create valid expressions and well-formed formulas
• Axioms are self-evident or assumed statements that serve as the starting points for deriving theorems
  • Logical axioms capture the fundamental principles of reasoning
  • Non-logical axioms are specific to a particular formal system (Peano arithmetic)
• Inference rules define how new theorems can be derived from axioms and previously proven statements
  • Modus ponens allows inferring $B$ from $A$ and $A \to B$
  • Generalization introduces universal quantifiers
• Proofs are sequences of well-formed formulas, each either an axiom or derived from previous formulas using inference rules

Propositional Logic Fundamentals

• Propositional logic deals with the logical relationships between propositions or statements
• Propositions are declarative sentences that are either true or false
• Logical connectives combine propositions to form compound statements
  • Negation ($\neg$) reverses the truth value of a proposition
  • Conjunction ($\land$) is true when both propositions are true
  • Disjunction ($\lor$) is true when at least one proposition is true
  • Implication ($\to$) is false only when the antecedent is true and the consequent is false
  • Biconditional ($\leftrightarrow$) is true when both propositions have the same truth value
• Truth tables enumerate all possible truth value assignments for a compound proposition
• Tautologies are propositions that are always true regardless of the truth values of their constituent propositions
• Contradictions are propositions that are always false
• Logical equivalence means two propositions have the same truth value for all possible truth value assignments

First-Order Logic and Quantifiers

• First-order logic extends propositional logic by introducing predicates, quantifiers, and variables
• Predicates are functions that map objects to truth values, representing properties or relationships
• Variables stand for objects in the domain of discourse
• Quantifiers express the extent to which a predicate holds for the objects in the domain
  • Universal quantifier ($\forall$) asserts that a predicate holds for all objects in the domain
  • Existential quantifier ($\exists$) asserts that a predicate holds for at least one object in the domain
• First-order logic allows for the construction of more expressive statements and the formalization of mathematical theories
  • Peano arithmetic can be formalized using first-order logic with non-logical axioms specifying the properties of natural numbers
• The Löwenheim-Skolem theorem states that if a first-order theory has an infinite model, it has models of every infinite cardinality
• The Compactness theorem asserts that a first-order theory is consistent if and only if every finite subset of its axioms is consistent

Proof Techniques and Methods

• Proofs demonstrate the validity of statements within a formal system
• Direct proof derives the conclusion from the premises using a sequence of logical steps
• Proof by contradiction assumes the negation of the conclusion and derives a contradiction, thereby establishing the truth of the original statement
• Proof by induction is used to prove statements about natural numbers
  • Base case proves the statement holds for the smallest value (usually 0 or 1)
  • Inductive step assumes the statement holds for $n$ and proves it holds for $n+1$
• Proof by cases considers all possible cases and proves the statement holds for each case
• Proof by counterexample disproves a universal statement by providing an instance where it does not hold
• Proof by construction provides an explicit example or algorithm to demonstrate the existence of an object or solution
• Proof by exhaustion verifies a statement by checking all possible cases in a finite domain

Applications in Computer Science

• Mathematical logic provides the theoretical foundation for computer science and programming languages
• Propositional logic is used in digital circuit design and boolean algebra
  • Logical gates (AND, OR, NOT) implement logical connectives
  • Simplification of boolean expressions optimizes circuit design
• First-order logic is used in databases, artificial intelligence, and knowledge representation
  • Relational databases use first-order queries to retrieve data
  • AI systems use first-order logic to represent and reason about knowledge
• Hoare logic is a formal system for reasoning about the correctness of computer programs
  • Hoare triples $\{P\}C\{Q\}$ specify preconditions $P$, commands $C$, and postconditions $Q$
  • Inference rules allow proving the correctness of programs
• Type theory and lambda calculus form the basis for functional programming languages (Haskell, ML)
• Automated theorem provers use mathematical logic to prove theorems and verify the correctness of software and hardware systems

Challenges and Limitations

• Gödel's Incompleteness Theorems reveal the inherent limitations of consistent formal systems containing arithmetic
  • First Incompleteness Theorem shows that such systems are incomplete, with true statements that cannot be proven within the system
  • Second Incompleteness Theorem demonstrates that a consistent system cannot prove its own consistency
• The undecidability of the Entscheidungsproblem, proven by Church and Turing, shows that there is no algorithm for determining the truth of arbitrary first-order statements
• The Halting Problem, which asks whether a given program will halt on a given input, is undecidable
• Russell's Paradox and other paradoxes expose the challenges in creating consistent and comprehensive foundations for mathematics
• The expressiveness of higher-order logics and type theories comes at the cost of increased complexity and potential inconsistency
• The trade-off between expressiveness and decidability limits the capabilities of formal systems in practical applications
• The complexity of automated theorem proving and program verification poses challenges in terms of computational resources and scalability