Nachtrag zum ccc-Axiom

Das ccc-Axiom besagt: " Jede offene Überdeckung eines beliebigen topologischen hausdorff Raums , besitzt eine abzählbare (nicht endlich, das ist kompakt) Teilüberdeckung ".

Schreibt man dies in der Programmiersprache eines typsierten lambda -Kalküls, so kann man die Konstrukte der Mengenlehre und Logik mittels der Theorie der Topen in der Kategorientheorie nachvollziehen.

Formuliert man in dieser Programmiersprache als Menge von lambda Ausdrücken das ccc-Axiom , so behaupte ich das das Gödelsche-Framework über die Beweisbarkeit von Sätzen ,in der Behauptung über die lambda-Ausdrücke im ccc Axiom mit enthalten sein könnten.

Man könnte Behautpten , dass eine programmiersprache Konstruktivistisch ist, dass stimmt nicht. Es gibt schwach evaluierende Programmiersprachen, bei denen die Auswertung von Ausdrücken einfach postuliert werden ohne diese notwendiger Weise auszuwerten. Bei zuhilfenahme dieses Konstruktes kann man durch mehrere lamda Ausdrücke eine objektorientiere Konstruktion der Mengenlehre , Aussagenlogik und Topologie programmieren und diese direkt in die Welt der lamda Ausdrücke zurück projizieren.