|
Prototyp / Aussagenlogik
Die logischen Gesetzmässigkeiten, auf denen die mathematische Argumentation aufbaut, werden im Folgenden entwickelt. Das Vorgehen ist dabei strikt formal: es werden Zeichenkettenmanipulationen nach einfachen Regeln durchgeführt. Die Ausgestaltung der Definitionen, Theoreme, Regeln und Beweise erfolgte nach den Ideen von Bernays, Hilbert und Ackermann.
Die folgenden Dokumente wurden mit dem Prototypen aus Qedeq-Modulen generiert. Diese Qedeq-Module wurden von dem darin integrierten Beweisprüfer auf formale Korrektheit hin kontrolliert. (Siehe auch die letzte Spalte.)
Falls das Betrachten der in der ersten Spalte referenzierten HTML-Seiten Probleme bereitet, versuchen Sie bitte die zweiten HTML-Links (o.html), die auf Seiten verweisen, welche einen installierten Symbol-Font voraussetzen. Falls auch diese HTML-Seiten nicht richtig dargestellt werden, schauen Sie bitte auf Ian Hutchinson's Seiten nach: Browser Problems und Comparative Review of World-Wide-Web Mathematics Renderers.
Grundlegende Definitionen der Aussagen- und Prädikatenlogik
lang&rules |
|
html |
o.html |
|
|
|
|
informelle Definition der verwendeten Sprache und der Schlussregeln |
propaxiom |
|
html |
o.html |
pdf |
tex |
qedeq |
|
Axiome, Definitionen und Deklarationen der Schlussregeln der Aussagenlogik |
Einfache Herleitungen
Systematische Entwicklung der Aussagenlogik
Nun werden systematisch die elementaren Sätze der Aussagenlogik hergeleitet. Die Grundlage und Vorlage dafür ist das Dokument Deduction. In diesem Dokument werden allerdings schon Metaregeln eingesetzt. Hier erfolgt die Ableitung nur mithilfe der Basisregeln, daher sind die nachfolgenden Dateien etwas groß. Für kürzere und lesbarere Beweise, die neue Metaregeln benutzen, siehe die nächsten Abschnitte.
Erste Metaregel
Systematische Entwicklung mit Metaregeln
Die selbe Entwicklung wie zuvor, aber nun werden Metaregeln benutzt. Dieses Vorgehen entspricht der üblichen mathematischen Methodik eher und ist dem Dokument Deduction ähnlicher. Die obigen Qedeq-Module, welche die Metaregeln nicht verwenden, wurden aus den nun folgenden Qedeq-Modulen automatisch generiert.
|