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.