Organisatorisches:

Erster Vorlesungstermin ist der 21.10.2016, erster Übungstermin der 28.10.2016. Während der Vorlesung werden 10-12 Übungsblätter bearbeitet.

Die Vorlesung wird durch einen elektronischen Online-Kurs unterstützt, der aufgrund technischer Beschränkungen der FU-seitigen e-Learning-Infrastruktur am University College London gehostet wird. Details hierzu und Zugangsdaten werden in der ersten Vorlesungswoche bekanntgegeben.

Die Vorlesung Logik gibt eine Einführung in Themen der Logik sowie ihrer praktischen Anwendungen. Sie richtet sich primär an Studierende der Mathematik, der Informatik, und Interessierte mit mathematischen Grundlagenwissen.

In der Vorlesung behandelt werden Grundlagen der formalen Logik:

• Aussagenlogik: „dieser Pinguin ist schwarz-weiß“
• Prädikatenlogik erster Stufe: „und alle Pinguine sind schwarz-weiß, aber nicht alles, was schwarz-weiß ist, ist ein Pinguin“
• Logik höherer Stufe: „jedoch sind alle Nachfahren von diesem Pinguin schwarz-weiß“
• Automaten und Turingmaschinen: „das kann man in polynomieller Zeit nachrechnen.“

mit theoretischen Schwerpunkten auf:

• Modelltheorie und Kalküle: Wie formalisiert man logische Schlussfolgerung? Beweise? „Wahrheit“?
• Beweistheorie und (Un-)Vollständigkeit: Ist alles Schlussfolgerbare wahr, und alles Wahre schlussfolgerbar?
• Berechenbarkeit und Entscheidbarkeit: … durch einen (Computer-)Algorithmus?

Praktische Aspekte stellen einen zentralen Bestandteil der Vorlesung und v.a. der Übungen dar, behandelt werden:

• Logik und Wissenschaftstheorie: wie axiomatisiert man empirische Beobachtungen? Wann ist eine logische Schlussfolgerung empirisch korrekt? Wie erkennt man mathematisch „korrekte“, aber empirisch unnütze (mathematisch/axiomatische) Modelle oder Schlussfolgerungen? Beispiele und Vermeidung von „Mathematistry“-Pseudowissenschaft.
• Inferenz- und Beweissysteme: wie formalisiert man logische Schlussfolgerung in einem Computer? Wie überprüft man in-silico, ob eine Schlussfolgerung, ein Beweis korrekt ist? Wie automatisiert man logisches Schlussfolgern im Computer? Der berühmte, vor kurzem erbrachte Maschinenbeweis der Kepler-Vermutung wird hier ausführlich als ein Beispiel-Highlight diskutiert werden.
• Anwendungen formaler Logik in der technischen Informatik: Schaltkreisdesign, formale Verifikation von Prozessoren.
• (falls zum Schluss noch Zeit ist und Interesse besteht) eine Einführung in Quantenlogik und Quantencomputing.

Literatur:

Für die theoretischen Teile orientiert sich die Vorlesung an

Ebbinghaus (2007) – Einführung in die mathematische Logik

Schöning (2000) – Logik für Informatiker