www.qedeq.org

 Hilbert II

English   Deutsch
Hilbert II bei SourceForge
Einführung
News
Mathematik
QEDEQ
Planung
Download
Glossar
Entwicklung
Prototyp
Installation
Anleitung
Aussagenlogik
Prädikatenlogik
QEDEQ
Fehler
Links
Kontakt
Sitemap
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

proptheo1   html o.html pdf tex qedeq   erste Theoreme
proptheo2   html o.html pdf tex qedeq   die Axiome des Whitehead-Russell-Kalküls als Theoreme hergeleitet

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.

prophilbert1   html o.html pdf tex qedeq   erste Schritte
prophilbert2   html o.html pdf tex qedeq   nächste Stufe
prophilbert3   html o.html pdf tex qedeq   dritte Stufe

Erste Metaregel

subst   html o.html pdf tex qedeq   Deklaration einer neuen Substitutions-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.

prophilbert1'   html o.html pdf tex qedeq   erste Schritte, hier werden weitere Metaregeln deklariert
prophilbert2'   html o.html pdf tex qedeq   nächste Stufe
prophilbert3'   html o.html pdf tex qedeq   dritte Stufe

update 2014-01-20 09:20:48+0100