Mittwoch, 28. August 2013
Computerverifikations des Gödelschen Gottesbeweises
Kurt Gödel hat der Nachwelt in seinem Nachlass einen ontologischen Gottesbeweis hinterlassen.

Er benutzt dabei die höherstufige Modallogik und es war bislang nicht möglich, alle seine Schliessungen korrekt nachzuvollziehen.

Dies ist nun mit Computerhilfe eindeutig gelungen und damit konnte die Korrektheit von Gödels ontologischer Gottesbeweis endgültig bestätigt werden.

Dazu gibt es einen sehr ausführliches Interview mit einem der Forscher, der diese Verifikation geleistet hat, auf Telepolis, die ja alles andere als religionsfreundlich sind.

Daraus:

Nehmen wir die beiden ersten Gödelschen Axiome. Das erste Axiom sagt, dass eine Eigenschaft positiv ist oder ihre Negation, niemals aber beides. Das zweite Axiom sagt, dass Eigenschaften, die notwendigerweise aus einer positiven Eigenschaften folgen, ebenfalls positiv sein müssen. Das ist auch schon alles, was Gödel über positive Eigenschaften in seinem ontologischen Beweis voraussetzt. Beide Axiome drückt er dann in der formalen Sprache der Logik aus.

Die Rahmenbedingungen für logische Formalisierungen stimmten bei Gödel. Seine Arbeit entstand nämlich zu einer Zeit, in der die formale Logik einen hohen Reifegrad erlangt hatte, nicht zuletzt durch Gödels bahnbrechende eigene Beiträge. Insbesondere mit der so genannten "Modallogik" stand ein gut entwickelter Logikformalismus zu Verfügung, der einen adäquaten und gut untersuchten Umgang mit den Begriffen "notwendig" und "möglich" unterstützte. Gödel beschreibt den von ihm gewählten Logikformalismus aber leider nicht mit letzter Konsequenz.

In diesem Punkt konnten unseren aktuellen Arbeiten interessante Einsichten liefern. Wir haben festgestellt, dass eine sehr schwache Modallogik, die so genannte Logik KB, die auf vergleichsweise wenigen Grundannahmen beruht, bereits eine erfolgreiche Beweisführung ermöglicht. Viele Arbeiten über Gödels Gottesbeweis erwähnen hier aber die stärkere Logik S5, und diese wurde in diesem Zusammenhang auch kritisiert. Wir wissen nun also, dass diese Kritik wohl gegenstandslos ist...

Modallogiken sind Erweiterungen der klassischen Logik. Letztere führt prominente logische Verknüpfungen ein, dazu gehören: "nicht", "und", "oder", "es folgt", "äquivalent" und "für alle x gilt". Die klassische Logik unterstützt aber keinen adäquaten Umgang mit zentralen Begriffen hinsichtlich Zeit, Raum, Wissen, Glauben, und auch nicht mit Begriffen wie "notwendigerweise gilt" bzw. "möglicherweise gilt", wie hier erforderlich. Modallogiken erweitern deshalb die klassische Logik um entsprechende logische Operatoren; typischerweise werden diese notiert als "[]" und "<>". Besonders kompliziert wird es, bei der klassischen Logik und insbesondere bei der Modallogik, wenn höherstufige Quantoren ins Spiel kommen.

Ein Beispiel für einen höherstufigen Quantor findet sich in Gödels Definition von "Gott-artig". In natürlicher Sprache ausgedrückt besagt diese: Ein Wesen ist "Gott-artig", falls es alle positiven Eigenschaften aufweist. Hier wird also eine universelle Aussage für alle Eigenschaften getroffen, und dazu stellt die Logik höherstufige Quantoren bereit. In der Formelsprache drückt Gödel dies wie folgt aus:

Gott-artig(x) <-> All P [ positiv(P) -> P(x) ]

Die Mechanisierung und Automatisierung von Logik auf dem Computer - man bezeichnet solche Computerprogramme auch als "Theorembeweiser" - hat seit der Jahrtausendwende sehr gute Fortschritte gemacht. Dies betrifft aber vor allem Theorembeweiser für ausdrucksarme, eingeschränkte Logiken, beispielsweise solche ohne Quantoren oder zumindest ohne höherstufige Quantoren. Höherstufige Logik, wie hier erforderlich, wird von theoretischen Informatikern aufgrund ihrer schlechten Komplexitätseigenschaften oft sogar als nicht handhabbar eingeordnet - teilweise zu Unrecht, wie unsere erfolgreiche Arbeit nun zeigt.

Was war eine besondere Herausforderung?

Christoph Benzmüller: Ein besonderes Problem für unsere Arbeit war, dass es für die höherstufige Modallogik bisher noch keine implementierten Theorembeweiser gab. Bei höherstufigen klassischen Logiken sieht es besser aus, mittlerweile gibt es hier zuverlässige und leistungsfähige Systeme; auch ich entwickle seit etwa 15 Jahren einen solchen Theorembeweiser.

Für Gödels Gottesbeweis wendeten wir einen Trick an, der es uns ermöglicht, höherstufige Modallogiken mithilfe letzterer Systeme zu mechanisieren und zu automatisieren. Dieser Trick beruht auf eigenen Arbeiten, die zum Teil mit Larry Paulson von der Universität Cambridge entstanden sind. Diese Arbeiten zeigen, wie man höherstufige Modallogik in die höherstufige klassische Logik einbetten kann, bzw. darin simulieren kann. Die klassische Logik höherer Stufe wird dabei als eine Art universelle Logik (mit Einschränkungen) verstanden und eingesetzt.


Siehe insbesondere Formalization, Mechanization and Automation of Gödel's Proof of God's Existence

... link (0 Kommentare)   ... comment


Montag, 26. August 2013
Königszabel - Wikingerschach
Am Rand des Schach-Weltcups in Tromsö/Norwegen wurde auch ein anderes Spiel vorgestellt, dass man als 'Wikingerschach' bezeichnet, aber genau übersetzt als Königszabel zu nennen ist.

Dieses schon damals von den Nordmännern gespielte Brettspiel ist eine sehr interessante Mischung aus Schach und dem asiatischen Go und überaus interessant ob der strategisch/ taktischen Möglichkeiten.

Zu diesem Spiel habe ich folgenden informativen Link gefunden: hier.

Eine der Varianten online spielen.

... link (0 Kommentare)   ... comment


Donnerstag, 22. August 2013
Verfassungswidrige Bundestagswahlen
Ein neues Bundeswahlgesetz soll das Problem der negativen Stimmengewichte lösen. Neben den mathematisch interessanten Ausführungen, hat mich vor allem folgende Tatsache im Bericht von wissenschaft-online sehr nachdenklich gemacht:

"Ein Wahlsystem, das … zulässt, dass ein Zuwachs an Stimmen zu Mandatsverlusten führt oder dass für den Wahlvorschlag einer Partei insgesamt mehr Mandate erzielt werden, wenn auf ihn selbst weniger oder auf einen konkurrierenden Vorschlag mehr Stimmen entfallen, führt zu willkürlichen Ergebnissen und lässt den demokratischen Wettbewerb um Zustimmung bei den Wahlberechtigten widersinnig erscheinen." So die Entscheidung, mit der das Bundesverfassungsgericht am 25. Juli 2012 die nur wenige Monate zuvor verabschiedete Neufassung des Bundeswahlgesetzes außer Kraft setzte.

Das von 1957 bis zur Bundestagswahl 2009 gültige Bundestagswahlsystem war verfassungswidrig und verletzte die Prinzipien der Unmittelbarkeit und Gleichheit der Wahl. Schuld war ein Effekt, der als negatives Stimmgewicht bezeichnet wird. Zusätzliche Stimmen für eine Partei konnten für diese zu einem Sitzverlust führen; umgekehrt konnte ein Stimmenverlust einer Partei einen zusätzlichen Sitz einbringen. ..

Auf mehrere Wahlprüfungsbeschwerden hin (darunter eine von mir) erklärte das Bundesverfassungsgericht das Wahlsystem im Juli 2008 für verfassungswidrig, gab aber dem Bundestag eine großzügige Frist von drei Jahren – also über die Bundestagswahl 2009 hinaus – für eine Korrektur. Der verabschiedete Ende 2011 ein Wahlgesetz, das allerdings das Problem mit dem negativen Stimmgewicht nicht beseitigte, sondern noch verschärfte. Im Juli 2012 kassierte das Bundesverfassungsgericht den Fehlversuch; zusätzlich entschied es, dass Überhangmandate nur in einem begrenzten Umfang (konkret: 15 Sitze) hinnehmbar sind. Daraufhin verabschiedete der Bundestag im Februar dieses Jahres schließlich das Gesetz, das für die anstehende Bundestagswahl gilt.


Also von 1957 bis 2009 waren alle Bundestagswahlen verfassungswidrig!!!

Es ist Zeit, dass im Umgang mit unserem Grundgesetz wieder mehr Sorgfalt und schlicht vorauseilende Verfassungstreue geübt wird. Die seit 1957 etablierten Parteien mit ihren Fraktionen im Bundestag scheint dies abhanden gekommen zu sein...

... link (0 Kommentare)   ... comment


Mittwoch, 21. August 2013
Experimentelle Fortschritte zum Warp Antrieb
Die NASA untersucht offiziell Möglichkeiten zur Realisierung eines Warp Antriebs. Dies ist keine Science Fiction sondern ein reales Forschungsvorhaben. Erste Experimente zegen nun erfolge bei der Verkürzung der Raumzeit und Vorstufen zur Generierung negativer Energie, wie space.com berichtet.

... link (0 Kommentare)   ... comment


Dienstag, 20. August 2013
Göbekli Tepe und Sirius
In der Türkei finden sich Steinmonumente in mehreren Kreisformationen angelegt. Die gesamte Anlage ist einmalig und gerade auch wegen ihres Alters von ca. 11000 Jahren sehr aufsehenerregend. Sie stellt Stonehenge in den Schatten.

Nun wurde entdeckt, dass die Zentrumssteine auf den Sirius ausgerichtet sind, natürlich zu der Zeit als die Anlage erbaut wurde.

Dies berichtet u.a. new scientest.

Sollte sich das bestätigen, wäre es eine Sensation, denn dass Menschen zu einem so frühen Zeitpunkt Sternenkunde betrieben war bislang ausgeschlossen worden.

... link (0 Kommentare)   ... comment


Montag, 19. August 2013
Erste Fernseh-Doku zur Ostsee-Anomalie
Die als sogenannte Ostsee-Anomalie bekannt gewordene Fundstelle eines schwedischen Tauchteams ist nun mit einer ausführlichen Fernseh-Doku der größeren Öffentlichkeit Schwedens bekannt gemacht worden. Und das ganze ist nun noch mysteriöser als schon zuvor gedacht.

Es berichtet Grenzwissenschaft-aktuell.

... link (0 Kommentare)   ... comment


Sonntag, 18. August 2013
Deutschland erkennt Bitcoin an
Das elektronische Zahlungsmittel BitCoin ist nun auch von Deutschland rechtliche anerkannt worden.

Persönlich kenne ich mich mit den BitCoin finanztechnisch nicht aus und gebe daher keine Empfehlung mit diesem elektronischen Geld zu handeln. Jedoch technisch finde ich die Realisierung des BitCoin absolut interessant.

Zur Meldung hier:

Deutschland hat die Digital-Währung Bitcoin einem Medienberichten zufolge in wesentlichen Punkten anerkannt. Die virtuellen Münzen seien rechtlich und steuerlich gebilligt und als Rechnungseinheiten anerkannt, berichten die "Frankfurter Allgemeine Zeitung" und die Online-Ausgabe der "Neuen Osnabrücker Zeitung" unter Berufung auf eine Anfrage des FDP-Abgeordneten Frank Schäffler und die Antwort des Bundesfinanzministeriums. Bitcoins seien damit "privates Geld".

Damit können auch andere private Zahlungsmittel die rechtliche Anerkennung beantragen.

... link (0 Kommentare)   ... comment