Mariami Gamsakhurdia & Stella Mahler
Start:
End:
Monday, 24.8. 10:00
Wednesday, 26.8. 14:15
Language: English
Credit Points: 1 CP upon agreement with the lecturers
Course description:
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.
Prerequisites:
Prior knowledge in mathematics and logic is recommended.
Mathematical Background: Basic understanding of fundamental proof techniques, such as induction, proof by contradiction, and contrapositive reasoning.
Logic Foundations: A general understanding of propositional logic, including truth tables, logical connectives (AND, OR, NOT, implication), and basic first-order logic concepts (quantifiers, predicates, logical formulae) at a high school or introductory undergraduate level.
Refresher materials for the core mathematical and logical concepts will be available.
Biography: 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.
Biography: 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.