Mathematiker versuchen Tag ein, Tag aus herauszufinden, ob bestimmte Formeln Tautologien sind. Immer, wenn ihnen das gelingt (und es noch niemand anderem gelungen ist), dann sind sie ganz aufgeregt und schreiben die Formel ganz schnell auf ein Papier, gefolgt von einer Begründung, weshalb die Formel eine Tautologie ist. Um herauszustreichen, dass ihnen die Tautologie besonders wichtig und tiefschürfend erscheint, nennen die Formel einen »Satz«; die Begründung, weshalb die Formel eine Tautologie ist, nennen sie einen »Beweis«. Ihren Satz schicken sie dann an andere Mathematiker. Wenn diese den Satz genauso aufregend finden kann der Satz sogar den Namen seines Entdeckers bekommen, was diesen dann wirklich ganz doll freut.
Die Bezeichnung »Satz« ist übrigens ausgesprochen irreführend, dies ist in typischer Fall, wo Mathematiker ein unschuldiges deutsches Wort genommen haben und es nun für ihre eigenen, je nach Standpunkt üblen oder hehren, Ziele gebrauchen. Ähnlich ergangen ist es dem »Ring«, unter dem Mathematiker weder eine runde Scheibe mit einem Loch in der Mitte verstehen, die man sich typischerweise an Finger steckt, noch einen etwas zu lang und pathetisch geratenen Opernzyklus.
Warum freuen sich Mathematiker denn so, wenn sie einen Satz bewiesen haben? So spannend ist der Umstand, dass a \lor (b \lor \neg b) eine Tautologie ist, nun auch wieder nicht. Das Schöne an Sätzen ist, dass man sie in Beweisen von neuen Sätzen benutzen kann. Deshalb finden Sie in Beweisen oft Formulierungen wie »... und nun folgt nach dem Satz von Bolzano-Weierstraß, dass...«, so dass über die Jahre, Jahrzehnte, Jahrhunderte und Jahrtausende immer komplexere Sätze bewiesen werden können. Der Satz des Pythagoras mag vor zweitausend Jahren noch sehr aufregend gewesen sein, heute lernt man das in der Schule. In tausend Jahren werden sich wahrscheinlich Lehrplanverantwortlichen für die Vorschule darüber streiten, ob das PCP-Theorem nicht lieber doch erst in der ersten Schulklasse unterrichtet werden sollte.
Wenn also Mathematiker normalerweise Tautologien beweisen, indem sie aus bereits bekannte Tautologien neue Tautologien folgern, was liegt näher, als ein formales Beweissystem aufzubauen, das genauso funktioniert? Der Hilbertkalkül der Aussagenlogik (auch als Fregekalkül bekannt) leistet genau dieses: Ausgangspunkt sind einige wenige so genannte Axiome, welche ganz einfache Tautologien sind. Es gibt eine Regel, den Modus ponens, nach der man neue Tautologien folgern darf: Wenn phi eine Tautologie ist und phi \to psi auch, so auch psi. Mehr ist nicht nötig, um alle aussagenlogische Tautologien zu beweisen.