Workshop on The Notion of Proof

Conflicts with Vienna Summer of Logic, but very interesting:


We have already witnessed the moment where chess-playing computers have surpassed humans. It might seem to be only a matter of time that computers will also surpass humans in mathematical theorem proving. In fact, the traditional notion of mathematical proof faces in the beginning 21st century what we will call “the computer challenge”. Three different aspects are worth separating:

  1. proof search;
  2. proof check;
  3. proof representation.

Proof search has its known limitations due to undecidability and complexity results. However, special areas, such as semigroup theory, already enjoy considerable support from computer-generated proofs. Proof check is recently the “hottest” area, in no small part due to the attempt to formally verify the proof of the Kepler conjecture by its author Hales. Proof representation seem currently be the stumbling block for convincing the mathematical community to accept computer aided theorem proving as a viable alternative.

In our workshop we solicit contributions for discussions the current state of the art of computer aided theorem proving (ATP), approaching the topic from the mathematical (or even philosophical) side, as well as from computer science. Special focus is put on the last two items mentioned above, addressing the more concrete question:

    1. How, and to what extent, can (or will) proof checking convince the mathematical community from the correctness of a proof?
    2. Does computer generated proof representations match with our intuitive notion of mathematical proof?

The answers to both question should give us a deeper insight in the challenges and tasks for mathematical proofs and computer-aided theorem proving in the 21st century.


    • Jesse Alama, Theory and Logic Group, Technical University of Vienna,
    • Reinhard Kahle, Center for Artificial Intelligence / Department of Mathematics, New University of Lisbon,

Extended Deadline! CFP: Symposium on the Foundations of Mathematics

CfP from

Set theory is taken to serve as a foundation for mathematics. But it is well-known that there are set-theoretic statements that cannot be settled by the standard axioms of set theory. The Zermelo-Fraenkel axioms, with the Axiom of Choice (ZFC), are incomplete. The primary goal of this symposium is to explore the different approaches that one can take to the phenomenon of incompleteness. 

One option is to maintain the traditional “universe” view and hold that there is a single, objective, determinate domain of sets. Accordingly, there is a single correct conception of set, and mathematical statements have a determinate meaning and truth-value according to this conception. We should therefore seek new axioms of set theory to extend the ZFC axioms and minimize incompleteness. It is then crucial to determine what justifies some new axioms over others.

Alternatively, one can argue that there are multiple conceptions of set, depending on how one settles particular undecided statements. These different conceptions give rise to parallel set-theoretic universes, collectively known as the “multiverse”. What mathematical statements are true can then shift from one universe to the next. From within the multiverse view, however, one could argue that some universes are more preferable than others.

These different approaches to incompleteness have wider consequences for the concepts of meaning and truth in mathematics and beyond. The conference will address these foundational issues at the intersection of philosophy and mathematics. The primary goal of the conference is to showcase contemporary philosophical research on different approaches to the incompleteness phenomenon.

To accomplish this, the conference has the following general aims and objectives: 

  1. To bring to a wider philosophical audience the different approaches that one can take to the set-theoretic foundations of mathematics.

  2. To elucidate the pressing issues of meaning and truth that turn on these different approaches.

  3. To address philosophical questions concerning the need for a foundation of mathematics, and whether or not set theory can provide the necessary foundation 

Date and Venue: 7-8 July 2014 – Kurt Gödel Research Center, Vienna

Confirmed Speakers:

Sy-David Friedman (Kurt Gödel Research Center for Mathematical Logic),

Hannes Leitgeb (Munich Center for Mathematical Philosophy)

Call for Papers: We welcome submissions from scholars (in particular, young scholars, i.e. early career researchers or post-graduate students) on any area of the foundations of mathematics (broadly construed). Particularly desired are submissions that address the role of set theory in the foundations of mathematics, or the foundations of set theory (universe/multiverse dichotomy, new axioms, etc.) and related ontological and epistemological issues. Applicants should prepare an extended abstract (maximum 1’500 words) for blind review, and send it to sotfom [at] gmail [dot] com. The successful applicants will be invited to give a talk at the conference and will be refunded the cost of accommodation in Vienna for two days (7-8 July).

Submission Deadline: 15 April 2014

Notification of Acceptance: 30 April 2014

Scientific Committee: Philip Welch (University of Bristol), Sy-David Friedman (Kurt Gödel Research Center), Ian Rumfitt (University of Birmigham), John Wigglesworth (London School of Economics), Claudio Ternullo (Kurt Gödel Research Center), Neil Barton (Birkbeck College), Chris Scambler (Birkbeck College), Jonathan Payne (Institute of Philosophy), Andrea Sereni (Università Vita-Salute S. Raffaele), Giorgio Venturi (Université de Paris VII, “Denis Diderot” – Scuola Normale Superiore)

Organisers: Sy-David Friedman (Kurt Gödel Research Center), John Wigglesworth (London School of Economics), Claudio Ternullo (Kurt Gödel Research Center), Neil Barton (Birkbeck College), Carolin Antos (Kurt Gödel Research Center)

Conference Website: sotfom [dot] wordpress [dot] com

Further Inquiries: please contact

Claudio Ternullo (ternulc7 [at] univie [dot] ac [dot] at)

Neil Barton (bartonna [at] gmail [dot] com)

John Wigglesworth (jmwigglesworth [at] gmail [dot] com)

Vienna Summer of Logic: Call for Volunteers

What is the Vienna Summer of Logic?

With over 2000 expected participants, the Vienna Summer of Logic 2014 (VSL) will be the largest event in the history of logic. It will consist of twelve large conferences and numerous workshops, attracting researchers from all over the world. The VSL will take place 9th-24 July 2014, at the Vienna University of Technology in Vienna, Austria.

The VSL conferences and workshops will deal with the main theme, logic, from three important aspects: logic in computer science, mathematical logic and logic in artificial intelligence. The program of the conference consists of contributed and invited research talks and includes a number of social events such as a student reception. For more information, visit

Vienna Summer of Logic Student Volunteers?

The VSL is organized by the Kurt Goedel Society, and preparations for this event have started some time ago. The most critical phase in the organization of any large scientific meeting is, of course, the time of the meeting itself! To ensure that all the scientific and social meetings taking place in the course of the VSL can be conducted successfully, the organizers of the VSL need your help as a VSL volunteer.

What are a volunteer’s duties?

There are many tasks at the VSL that will be performed by volunteers, such as helping with the registration of the participants at the conference, assisting with the use of the technical infrastructure at the conference site, etc. Each volunteer will be supervised by one of the senior organizers who will be the volunteer’s contact person at the conference.

What are a volunteer’s perks?

The most important benefit of volunteering is that volunteers may attend all the VSL conferences for free: this means that you can attend all the research talks given at the conferences, and mingle with the researchers during the coffee breaks. More precisely, your time at the VSL will be divided in the following way: 50% free time to attend lectures of your choosing, 30% fixed volunteer’s duties, and 20% ,,standby duty”. Furthermore, all volunteers may participate in the conference’s student reception (which is a party for all the students participating at VSL), and will receive a VSL volunteer’s t-shirt to be able to proudly display their participation in this event in the years to come.

How do I become a volunteer?

Interested in becoming a Vienna Summer of Logic volunteer? Please visit

for the application form. The deadline for applications is May 25, 2014. Applicants that have been chosen as volunteers will be contacted before June 1, 2014.

Visiting Research Chair in Logic or Philosophy of Science at the University of Calgary

US$25,000 for 4 months (September 2015 or January 2016)

Contact: Brad Hector, Fulbright Canada Program Officer (Scholars)

The University of Calgary is pleased to offer the opportunity for a Fulbright Visiting Research Chair in Logic or the Philosophy of Science. The visiting researcher will be a part of the Department of Philosophy and collaborate with a dynamic research faculty and graduate students. The Department of Philosophy is internationally recognized in logic and the philosophy of science and home to 22 professors, including a Tier 1 Canada Research Chair in the philosophy of biology. The scholar will offer a combined seminar for senior undergraduate students and graduate students in his or her area of expertise, and will participate in departmental and interdisciplinary research groups while pursuing his or her own research projects. 

Specialization: History and philosophy of science, mathematical and philosophical

Applicants are encouraged to identify their primary and alternate choices on the application. Formal letters of invitation should not be sought; however, applicants are encouraged to contact the institution to discuss research interests.

Leslie Lamport wins Turing Award

The Association for Computing Machinery has awarded the 2013 Turing Award (the Computer Science equivalent of the Nobel Prize Fields Medal Schock Prize) to Leslie Lamport at Microsoft Research for his work on formal specification and verification techniques, specifically the Temporal Logic of Actions and his work on fault tolerance in distributed systems. Not as close to logic as some other Turing Laureates (is that what they’re called?) but still a nice nod to the continued importance of formal methods derived in part from logic in CS. (Oh yeah, he also invented LaTeX.)

Constructive Ordinals and the Consistency of PA

Today’s the last of three lectures on Gentzen’s second proof of the consistency of PA in my proof theory course.

a) Still looking for good resources on ordinal notations, esp., \(<\epsilon_0\), especially around the question how one can “see” that they are well-ordered without mentioning that they are order-isomorphic to \(\epsilon_0\)  Takeuti has a discussion in his textbook, anything else?

b) Some fun links:

Andrej Bauer’s Hydra game applet:

David Madore’s ordinal visualizer:

c) Looking for a good intro to Goodstein’s theorem and incompleteness in PA: Will Sladek’s paper linked from Andrés Caicedo’s blog:

E. W. Beth Dissertation Prize: 2014 Call for Nominations

Since 2002, FoLLI (the Association for Logic, Language, and Information, has awarded the E.W. Beth Dissertation Prize to outstanding dissertations in the fields of Logic, Language, and Information. We invite submissions for the best dissertation which resulted in a Ph.D. degree awarded in 2013. The dissertations will be judged on technical depth and strength, originality, and impact made in at least two of three fields of Logic, Language, and Computation. Interdisciplinarity is an important feature of the theses competing for the E.W. Beth Dissertation Prize.

Who qualifies?

Nominations of candidates are admitted who were awarded a Ph.D. degree in the areas of Logic, Language, or Information between January 1st, 2013 and December 31st, 2013. Theses must be written in English; however, the Committee accepts submissions of English translations of theses originally written in other languages, and for which a PhD was awarded in the preceding two years (i.e. between January 1st, 2011 and December 31st, 2012). There is no restriction on the nationality of the candidate or on the university where the Ph.D. was granted. 


The prize consists of:

  • a certificate
  • a donation of 2500 euros provided by the E.W. Beth Foundation
  • an invitation to submit the thesis (or a revised version of it) to the FoLLI Publications on Logic, Language and Information (Springer). For further information on this series see the FoLLI site. 

How to submit

Only electronic submissions are accepted. The following documents are required:

  1. The thesis in pdf format (ps/doc/rtf not accepted).
  2. A ten-page abstract of the dissertation in pdf format.
  3. A letter of nomination from the thesis supervisor. Self-nominations are not admitted: each nomination must be sponsored by the thesis supervisor. The letter of nomination should concisely describe the scope and significance of the dissertation and state when the degree was officially awarded.
  4. Two additional letters of support, including at least one letter from a referee not affiliated with the academic institution that awarded the Ph.D. degree.

All documents must be submitted electronically (preferably as a zip file) to Ian Pratt-Hartmann ( Hard copy submissions are not allowed. In case of any problems with the email submission or a lack of notification within three working days, nominators should write to Ian Pratt-Hartmann.

Important Dates

Deadline for Submissions: May 5th, 2014.
Notification of Decision: July 14th, 2014.
Committee :
Julian Bradfield (Edinburgh)
Wojciech Buszkowski (Poznan)
Michael Kaminski (Haifa)
Marco Kuhlmann (Linköping)
Larry Moss (Bloomington)
Ian Pratt-Hartmann (chair) (Manchester)
Ruy de Queiroz (Recife)
Giovanni Sambin (Padua)
Rob van der Sandt (Nijmegen)
Rineke Verbrugge (Groningen)

Brian Leiter Should Apologize

In a (since removed) long post on his widely read blog, Brian Leiter attacked my colleague Rachel McKinnon, calling her “singularly unhinged” and “crazy”.  I don’t know what to say, except that I hope an apology for this singularly unprofessional outburst is forthcoming.

Journal for the History of Analytical Philosophy (JHAP) Essay Prize

JHAP is an international open access, peer reviewed publication that aims to promote research in and provide a forum for discussion of the history of analytic philosophy. ‘History’ and ‘analytic’ are understood broadly. JHAP takes the history of analytic philosophy to be part of analytic philosophy. Accordingly, it publishes historical research that interacts with the ongoing concerns of analytic philosophy and with the history of other twentieth century philosophical traditions.

JHAP invites submission for its first Essay Prize Competition. 

The competition is open to PhD candidates and recent PhDs (no more than 3 years at the time of submission). Articles on any topic in the History of Analytical Philosophy are welcome. There are no constraints on length.

Authors are requested to submit their papers electronically according to the following guidelines:

1) Papers should be prepared for anonymous refereeing, 2) put into PDF file format, and 3) sent as an email attachment to the address given below — where 4) the subject line of the submission email should include the key-phrase “JHAP ESSAY PRIZE submission”, and 5) the body text of the email message should constitute a cover page for the submission by including i) return email address, ii) author’s name, iii) affiliation, iv) paper title, and v) short abstract.


Submission Deadline: 1 September 2014

Adjudication: The winner of the competition will be decided by a committee composed of members of the editorial board.

Prize: The winning article will be published in a special issue of JHAP and the author will receive a cash prize.

Philosophy of Mathematics Postdoc at Nancy or Paris

One year Post-doc Fellowship in the context of the ANR-DFG research   program MATHEMATICS: OBJECTIVITY BY REPRESENTATION (MathObRe) at the <a href=" d’Histoire des Sciences et de Philosophie—Archives Henri-Poincaré, Nancy (UMR 7117) or at the <a href="%20 d’Histoire et de Philosophie des Sciences, Paris (UMR 8590).

We invite applications for a postdoctoral fellowship for 12 months  in the academic year 2014/15 (October 1st 2014 to September 30th 2015) in the context of the project mentioned above. The project aims to study the relation between mathematical objectivity and the role of representation in mathematics from a philosophical point if view, with particular attention to historical development of mathematics and to mathematical practice. The directive lines of the project are available here:

The successful candidate is expected to contribute to the realization of this project and to reside in Nancy or Paris during the whole your of her/his grant. The decision where she/he should reside in Nancy or Paris throughout the year will be taken by ourselves, according to the research topic. The grant amount (1600-1800€/month after taxes) is set by French regulations. We encourage to apply young scholars having received their doctoral   degree in the last 5 years in the domain of philosophy of mathematics and the like with a proven potential to conduct and publish research at a level of international excellence.

Applications should include:

  • A (brief) letter of application including personal information academic background, and research interests
  • A proposal for a research project (3-4 pages) aiming to contribute to MathObRe
  • CV including a list of publications, talks, conferences attended  and teaching experience.
  • One or two recommendation letters from a recognised scholar in the field.

This material is to be sent by e-mail to  Gerhard Heinzmann and Marco Panza before April 30th at midnight (French time). Decisions will be made by May 31th, 2014.