Introduction to Formal Systems

Formal Systems: Definition and Key Properties What is a Formal System? A formal system is a rigorous framework for mathematical reasoning that consists of a set of symbols, rules for combining them, and specific starting points. The system is designed to generate true statements (called theorems) through mechanical, step-by-step processes. Think of it as a game with strict rules: you start with certain given statements, and you follow precise rules to derive new statements. The key insight is that everything in a formal system is syntactic—meaning it operates on the symbols themselves, not on meanings or interpretations. A computer could, in principle, verify every step of a formal proof without understanding what the symbols mean. The Five Core Components Alphabet (Symbols) The alphabet is your toolkit of basic symbols. Just as the English alphabet consists of the letters A through Z, a formal system's alphabet is a finite set of characters you're allowed to use. For example, in propositional logic, the alphabet includes: Propositional variables (like $p$, $q$, $r$) Logical connectives: $\land$ (and), $\lor$ (or), $\neg$ (not), $\to$ (implies) Parentheses for grouping These symbols are the raw materials from which all statements in the system are built. Syntax (Well-Formed Formulas) Not every string of symbols makes sense. Syntax refers to the rules that determine which combinations of symbols are legitimate statements, called well-formed formulas (often abbreviated as WFFs or just formulas). For propositional logic, the syntax rules might include: Any propositional variable ($p$, $q$, etc.) is a well-formed formula If $\varphi$ is a well-formed formula, then $\neg \varphi$ is also a well-formed formula If $\varphi$ and $\psi$ are well-formed formulas, then $(\varphi \land \psi)$ is a well-formed formula These rules allow you to build complex formulas from simpler ones. For instance, starting from the variable $p$, you could build $\neg p$, then $(\neg p \land q)$, and so on. The key point: syntax is purely about the form of the statements, not their truth or meaning. The formula $(p \land q)$ is well-formed whether or not we know what $p$ and $q$ represent. Axioms Axioms are statements that the system assumes to be true without proof. They form the foundation on which all reasoning in the system rests. In Peano Arithmetic, for example, one axiom states that $0$ is a natural number. In propositional logic, axioms might include statements like: $$(\varphi \to (\psi \to \varphi))$$ This says: "If $\varphi$ is true, then whenever $\psi$ is true, $\varphi$ is still true." This seems intuitively reasonable, so we accept it as an axiom. The crucial distinction: axioms are assumed, not proven. Every formal system must start somewhere, and axioms are the starting point. Inference Rules Inference rules are the legal moves you're allowed to make when reasoning. They specify how you can take existing formulas and derive new ones. The most famous inference rule is modus ponens: If you have already established that $\varphi$ is true, and you have established that $\varphi \to \psi$ (meaning "if $\varphi$ then $\psi$"), then you may conclude that $\psi$ is true. In symbols: From $\varphi$ and $(\varphi \to \psi)$, infer $\psi$. This rule captures the basic intuition of logical deduction. If a statement $\varphi$ is true, and we know that $\varphi$ implies $\psi$, then $\psi$ must also be true. Theorems A theorem is any formula that can be derived from the axioms by applying inference rules a finite number of times. In other words, theorems are the "output" of the system—the statements that can be proven true. The distinction is important: axioms are assumed to be true, while theorems are proven to be true. Every axiom is trivially a theorem (it can be proven in zero steps), but not every theorem is an axiom. The diagram above shows this hierarchy: theorems are the formulas you can reach; all theorems must be well-formed formulas; and all well-formed formulas are strings of symbols from the alphabet. The Mechanical Nature of Proof Checking One defining feature of formal systems is that proving a statement is entirely mechanical. This means: Each step in a proof either applies an inference rule or states an axiom A computer can verify each step by checking the syntactic form No insight, intuition, or interpretation is needed to verify correctness This doesn't mean computers can find proofs easily, but they can verify that a proposed proof is correct. The computer doesn't need to understand what the symbols mean—it only needs to check that the rules were followed correctly. Examples of Formal Systems Propositional Logic Propositional logic is the simplest formal system. Its symbols include propositional variables and logical connectives ($\land$, $\lor$, $\neg$, $\to$). The axioms encode basic facts about how these connectives work—for instance, that "if $\varphi$ and $\varphi$ implies $\psi$, then $\psi$" (modus ponens). Propositional logic allows you to reason about how complex statements relate to each other based purely on their logical structure, without needing to understand what the individual propositions mean. First-Order (Predicate) Logic First-order logic is more powerful. It adds: Quantifiers: $\forall$ (for all) and $\exists$ (there exists) Variables: $x$, $y$, $z$ that can range over objects in a domain Predicates: symbols representing properties or relations This allows you to express statements like "for all $x$, if $x$ is a human, then $x$ is mortal" ($\forall x: \text{Human}(x) \to \text{Mortal}(x)$). First-order logic is powerful enough to express most mathematical reasoning, which is why it's fundamental in mathematical logic. Peano Arithmetic Peano Arithmetic is a formal system specifically designed for reasoning about natural numbers. Its alphabet includes symbols for numbers and operations, and its axioms include: Zero is a natural number Every natural number has a successor The principle of mathematical induction: if a property holds for zero and holds for the successor of any number that has it, then it holds for all natural numbers Peano Arithmetic is powerful enough to formalize most results in elementary number theory. Key Metatheoretic Properties Beyond the components of a formal system, we can ask important questions about the system itself. Three properties are particularly crucial: Consistency A formal system is consistent if it is impossible to prove both a statement and its negation. In other words, you can never derive both $\varphi$ and $\neg \varphi$. Why does this matter? If a system is inconsistent, then by the principle of explosion, you can prove literally any statement (true or false). An inconsistent system is useless for reasoning because everything is "provable," which means nothing is meaningful. Consistency is non-negotiable: a formal system must be consistent to be worth studying. Completeness A formal system is complete if every statement that is true (in the intended interpretation) can be proved within the system. Here's the key idea: there's a difference between what is true and what is provable in the system. Suppose the system intends to describe the natural numbers. A statement like "there are infinitely many prime numbers" is true (in the standard interpretation of arithmetic). A complete system would be able to prove this statement. Conversely, an incomplete system has some true statements that cannot be proven. These statements are independent of the system—they're neither provable nor disprovable. Soundness A formal system is sound if every theorem (every statement it proves) is actually true in the intended interpretation. The difference between soundness and completeness is subtle but crucial: Soundness: Everything provable is true (no false proofs) Completeness: Everything true is provable (no missed truths) A sound system will never prove something false, but it might fail to prove something true (incompleteness). A complete system will prove everything true, but it might accidentally prove something false (unsound). Most mathematicians prioritize soundness over completeness. We want a system that never lies to us, even if it can't prove everything. Gödel's Incompleteness Theorems In 1931, Kurt Gödel proved two remarkable theorems: First Incompleteness Theorem: Any consistent formal system powerful enough to formalize arithmetic (like Peano Arithmetic) is incomplete. There exist true statements that cannot be proved within the system. Second Incompleteness Theorem: No sufficiently powerful consistent formal system can prove its own consistency. These theorems shattered the hope that mathematics could be reduced to a single, complete, axiomatized system. What Gödel showed is that any such system either: Is inconsistent (proves false things), or Is incomplete (fails to prove true things) <extrainfo> This doesn't mean mathematics is broken or that we can't prove things rigorously. Rather, it means that for any formal system we choose, there will always be true statements (within that system's domain) that lie beyond its reach. We can extend the system by adding new axioms, but then Gödel's theorems apply to the new, larger system as well. </extrainfo> Peano Arithmetic and first-order logic both fall under Gödel's results: they cannot be both consistent and complete.