| 02.03.2025, 22:44 |
Finn_ |
Auf diesen Beitrag antworten » |
Schlanker Beweisprüfer
Resultat meiner letzten Studie ist dieser neue Beweisprüfer, der bei aufkommender Unsicherheit Abhilfe schafft. Das kurze Python-Programm, unter 900 Zeilen lang, prüft die korrekte Anwendung der Regeln des natürlichen Schließens zur Logik erster Stufe. Die Maschine sorgt für absolute Sicherheit. Keine Zweifel, keine Unschärfe, keine menschliche Nachlässigkeit. Ich denke, dies hilft, auf dem Weg zur Klärung einen Schritt weiterzukommen.
[attach]58170[/attach]
Mir tut sich allerdings die Frage auf, ob der Prüfer selbst frei von Lücken ist, insbesondere, ob dieser keine Ableitung gestattet, die ohne Heranziehung dubioser Axiome im Widerspruch mündet. Der Mechanismus zur Festlegung eines Axioms ließe sich ja nach dem Durchlaufen des Präludiums ausschalten. Dahinter dürften dann beliebige Eingaben erscheinen, die entweder als korrekt oder als fehlerhaft befunden werden. Für Spitzfindige: Eine Nachlässigkeit ist mir aber gerade noch aufgefallen. Die hat damit zu tun, dass sich die Bedeutung einer freien Variable innerhalb eines Theoremschemas durch eine spätere Definition verändert. Der Zeitpunkt der Musterbildung mit dem vorgestellten Fragezeichen liegt zu spät; diese müsste wohl unmittelbar nach der Prüfung des jeweiligen Schrittes stattfinden. Allerdings sollte diese Nachlässigkeit lediglich zu einer unbedenklichen Spezialisierung der Formel führen. Es wäre diesbezüglich aber auch noch zu untersuchen, ob man sich damit nicht durch die Typprüfung mogeln kann. |
