Proofs and Programs: Rethinking Mathematical Truth

Mariami Gamsakhurdia & Stella Mahler

Unterrichtssprache: Englisch

Kursbeschreibung:

What is a proof, really? And what does it have to do with writing a computer program?

In this course, we explore the basics of logic and discover how mathematicians decide what counts as “true.” You’ll see that there isn’t just one kind of logic: in classical logic, something is either true or false, but in intuitionistic logic things become more complicated.

We’ll learn what formal proofs look like, step by step, and how they behave like objects you can work with. Along the way, you’ll discover a surprising idea: proving something can be very similar to writing a program. This connection, known as the Curry–Howard correspondence, reveals that proofs and programs are, in a sense, the same thing.

No prior experience with logic is needed – just curiosity and a willingness to think in new ways. By the end, you’ll have a new perspective on both mathematics and programming and how deeply they are connected.

Voraussetzungen:

Grundlegende Vorkenntnisse in Mathematik und Logik werden empfohlen.

Mathematischer Hintergrund: Grundlegendes Verständnis zentraler Beweistechniken wie vollständige Induktion, Widerspruchsbeweise und Kontraposition.

Logische Grundlagen: Allgemeines Verständnis der Aussagenlogik, einschließlich Wahrheitstabellen, logischer Verknüpfungen (UND, ODER, NICHT, Implikation) sowie grundlegender Konzepte der Prädikatenlogik erster Stufe (Quantoren, Prädikate, logische Formeln) auf dem Niveau der gymnasialen Oberstufe oder einer einführenden universitären Lehrveranstaltung.

Auffrischungsmaterialien zu den grundlegenden mathematischen und logischen Konzepten werden zur Verfügung gestellt.

Biographie: Mariami Gamsakhurdia

Mariami Gamsakhurdia is a researcher in mathematical logic with a special focus on proof analysis, epsilon calculus, intermediate logics, and their applications in computer science. Her academic journey has been centered around mathematical logic. She completed her BSc at Tbilisi State University and MSc at the University of Milan, both in pure mathematics. Currently, she is pursuing her Ph.D. at the Computational Logic research group at TU Wien (Vienna University of Technology) under the supervision of Ao. Univ. Prof. Dr. Matthias Baaz.

Biographie: Stella Mahler

Stella Mahler is a researcher in logic, focusing on computational proof theory,
automated deduction, and the applications of logic in computer science. Currently pursuing her Ph.D. at the Logic and Theory research group at Vienna
University of Technology, she has a strong foundation in both theory and application. Stella completed her BSc in Computer Science through the International
Women’s Degree Programme at Hochschule Bremen and her MSc in Logic and
Computation at TU Vienna. With a background in pedagogy, she is passionate
about teaching and excited to collaborate with other inspiring women to explore
engaging and innovative teaching styles at the Summer University.