Formal systems, explained honestly

Gödel Incompleteness Explorer

A clearer interactive page about formal systems, axioms, derivations, consistency, and why incompleteness appears.

What this page really is

This is a toy formal system simulator. It does not prove Gödel’s theorems directly. It helps you see what axioms do, how derivations grow, and why “adding more axioms” does not magically eliminate incompleteness.

Axioms 0
Known statements 0
Derived theorems 0
Proof depth 0
Consistency Consistent

Derivation Timeline

0

Each step below is either a starting axiom or a derived statement produced by the toy engine.

Pending Next Steps

These are the statements the simulator can derive next from the current axioms and already known statements.

Formal system in one sentence

A formal system starts with axioms and uses inference rules to derive theorems. The crucial question is not only what can be derived, but also what cannot be derived without breaking consistency.

Gödel’s move

Gödel encoded formulas and proofs as numbers, then built a sentence that effectively says: “I am not provable in this system.” If the system is consistent, that sentence cannot be proved inside the system, yet it is true in the intended interpretation.

What this simulator can and cannot do

This page models a small rule engine so you can see how axioms expand a theory. It does not implement full first-order arithmetic, Gödel numbering, or real proof checking. It is a conceptual bridge, not a proof assistant.

Useful experiments

  • Start from “0 ∈ ℕ” and the successor axiom, then step through the derived numerals.
  • Add P → Q and then add P to watch modus ponens create Q.
  • Add both P and ¬P to see how inconsistency is detected.