Talk by Chad Brow (Czech Technical University in Prague): Formalization of Mathematics in Higher Order Set Theory (Wed, Nov 16, 14:15-15:45)
Title: Formalization of Mathematics in Higher Order Set Theory
Speaker: Chad Brown (Czech Technical University in Prague)
Abstract: Church's simple type theory is a formulation of higher-order logic upon which many interactive theorem provers are based. A benefit of using Church's type theory is that for many theories that have no first-order finite axiomatization, there are corresponding theories that do have higher-order finite axiomatization. I will introduce Church's type theory and sketch a finite axiomatiation of a set theory in which one can formalize mathematics. I will also discuss the interplay be interactive theorem proving and automated theorem proving in this context.
When: Wed, Nov 16, 14:15-15:45
Where: Erba, Room WE5/04.004