Carnegie Mellon University
December 14, 2015

Logic and Proofs: Computer-Supported Learning and the Philosophy of Mathematics

By Emily Stimmel

Wilfried Sieg arrived at Carnegie Mellon University in 1985 to help found the CMU Philosophy Department. He was its head from 1994 to 2005. Today, Sieg remains a central figure in the department and is one of the world’s foremost experts in areas ranging from proof theory and computer-assisted education to the history and philosophy of mathematics. He was elected as a Fellow of the American Academy of Arts and Sciences in 2007.

Whether in freshman seminars or in work with Ph.D. students, Sieg’s teaching pivots on central themes of logic, mathematics and their history, but also their application in philosophical theory and scientific practice—an inexhaustible source of course content.

“One of the great pleasures of teaching is to learn with and for students,” Sieg said.

Sieg developed an interest in improving education through technology as a Ph.D. student at Stanford University, where he worked closely with Patrick Suppes, a pioneer in computer-assisted instruction. An interdisciplinary philosopher who drew from logic, psychology and education theory in his work, Suppes was a strong supporter of CMU’s Philosophy Department—one of the youngest in the country—and chaired its advisory board in the mid-1990s.

Today, Sieg carries on Suppes’ legacy as the Patrick Suppes Professor of Philosophy. He plays an important role in Carnegie Mellon’s Open Learning Initiative (OLI), which emerged out of work in the Philosophy Department done by Sieg and Richard Scheines —now dean of the Dietrich College of Humanities & Social Sciences and professor of philosophy, machine learning and human-computer interaction. Their early joint work started around 1990 and aimed for the implementation of strategic proof search in logic, eventually leading to the AProS system that is now at the core of a dynamic intelligent tutor, the Proof Tutor.

In 2004, with funding from the National Science Foundation, Sieg began to develop an OLI course called Logic & Proofs, a highly interactive introduction to modern symbolic logic that utilizes the Proof Tutor. One of its central objectives is for students to learn how to construct logical arguments. As students attempt to give a proof in a sophisticated graphical interface, the Proof Tutor checks the correctness of their logical steps and provides instant feedback. If students get stuck, they can enter into a dialogue with the Proof Tutor, which encourages them to analyze the state of the problem and to review appropriate strategies. Ultimately, it can provide a hint on how to proceed in the argument; the hint is based on the proof that AProS found when completing the student’s partial argument.

As an unanticipated benefit, technology-supported learning is helping to close the divide between students in the humanities and those in math and science. Humanities students have shown substantial improvements in their performance when learning logic through Logic & Proofs.

“His work on bringing a more interactive experience to Logic & Proofs helped a lot of people understand the concept better,” said Andrey Tydnyuk (SCS’13), who worked with Sieg as a research and teaching assistant when he was an undergraduate student.

Another major advantage of a virtual learning space is that it allows for instructional time to expand and meet individual students’ needs more efficiently.

“Having automated tools do all of the manipulations of axioms and truth tables meant that students would have to spend less time sketching out complicated diagrams and more time actually learning the logical rules,” added Tydnyuk.

Now offered every semester at CMU, Logic & Proofs has grown from 20 students in its first term to an average of 120 students per term; it is also offered at other universities nationwide and internationally, for example, in Italy and Guatemala.

The interactivity and flexibility that make automated tutoring such an appealing concept make it a challenge as well.

“It is an unending task to exploit the dynamic possibilities of the computer,” said Sieg.

His collaborator, Dawn McLaughlin, has been involved in various aspects of the course, from writing text to software programming, while working towards her Ph.D. in logic, computation and methodology. She believes Sieg’s efforts have driven improvements not only to the course, but also to the OLI framework in general.

McLaughlin said, “He has always pushed, and encouraged us to push, the limits of the available technology in order to provide a really superior learning experience for students—and a superior teaching experience for instructors.”

Sieg’s work using technology in the classroom is transforming how logic is taught at Carnegie Mellon and elsewhere. The advancements made in Logic & Proofs and other OLI courses are core reasons why Carnegie Mellon is recognized as a leader in educational research. They are also fundamental components of the Simon Initiative, a university-wide effort to measurably improve learning outcomes by harnessing CMU's learning research and engineering ecosystem.

Like his teaching, Sieg’s research spans three distinct areas—mathematical logic (in particular, proof theory), computation theory and philosophy of mathematics—and the points at which they overlap.

His research in proof theory is rooted in the work of David Hilbert, a German mathematician widely regarded as one of the most influential mathematicians of the late 19th and early 20th centuries. One of the founders of proof theory and mathematical logic, Hilbert defined concepts that helped shape mathematical and logical research in the 20th century.

Sieg—himself a German native and dual citizen—describes Hilbert as one of his intellectual heroes. In 2013, his analyses of Hilbert’s work culminated in the publication of Hilbert’s Programs & Beyond. In the book, published by Oxford University Press, Sieg highlights Hilbert’s role in the development of mathematical logic and proof theory through a series of essays. In the same year, a long collaborative effort to edit Hilbert’s unpublished lecture notes on logic came to fruition with a volume of more than 1,000 pages published by Springer.

More recently, Sieg’s research has found him working alongside OLI Director Norman Bier and Majd Sakr, teaching professor of computer science. The group received a Simon Initiative ProSEED grant for the project, which is using two OLI courses—Sakr’s Cloud Computing and Sieg’s Logic & Proofs—to develop a mechanism to help students gain insights into problem-solving strategies.

Sieg’s work has taken him around the world. He spent much of 2015 traveling, for example, to Paris, Vienna, Tokyo, Kyoto and Doha, to give talks about the interdisciplinary areas of his expertise.

In spite of his accomplishments and involvement in many projects, Sieg remains approachable and accessible to students.

“I’ve always had the highest opinion of Professor Sieg,” remarked Tydnyuk. “During all my time working with him and taking his classes, whenever I asked him a question, I got a perfect answer. Sometimes it took me a while to realize it, but it was always there.”