"In Raymond Smullyan’s story there was a planet on which the concept of humor was unknown and laughter was treated as a disease. Those who laughed were sent to live in laugh-hospitals, away from normal people. As time passed ever more people contracted laughter and the laugh-hospitals grew into whole laugh-communities, until the few remaining normal people pretended to understand humor just so that they could join the rest. What if constructive models are like the laugh-hospitals? What if not understanding constructivism is like not having a sense of humor?"
The world of constructive mathematics is becoming more and more popular due to its connection to both topology and the theory of computation. On the other hand, theories of arithmetic (in the classical world) have been studied for their ability to formalize computation for decades. One may wonder - if intuitionistic logic already in some sense formalizes computation, wouldn't intuitionistic theories of arithmetic be better for the job? This semester, we aim to build enough background in intuitionistic logic to answer this question. If the time permits, we hope to conclude by introducing Heyting arithmetic, the intuitionistic counterpart of Peano arithmetic.
The program of the past semesters can be found at professor Krajíček's website.
The timeslot for the seminar is not neccesarily set in stone and if there is a better time for most participants, can be changed. So either come join us for the first organizational meeting, or please send us your time preferences by email.
Our seminar meets regularly to discuss the assigned readings. Here is the schedule:
If you have any questions or would like to join our seminar, please feel free to contact us: