University of Calgary
UofC Navigation

All LogBlog Posts

Halbach & Visser: Self-reference in arithmetic

Submitted by Richard Zach on Sun, 12/14/2014 - 7:19am

New in the Review of Symbolic Logic (part 1, part 2)

A Gödel sentence is often described as a sentence saying about itself that it is not provable, and a Henkin sentence as a sentence stating its own provability. We discuss what it could mean for a sentence of arithmetic to ascribe to itself a property such as provability or unprovability. The starting point will be the answer Kreisel gave to Henkin’s problem. We describe how the properties of the supposedly self-referential sentences depend on the chosen coding, the formulae expressing the properties and the way a fixed points for the formulae are obtained. This paper is the first of two papers. In the present paper we focus on provability. In part II, we will consider other properties like Rosser provability and partial truth predicates.

More on Shatunovsky, Kagan, and Yanovskaya

Submitted by Richard Zach on Sat, 12/13/2014 - 5:51am

In response to my post about "lesser known Russian/Soviet logicians", Lev Beklemishev commented:

Dirk van Dalen was interested in Shatunovsky's work and at his request I procured a copy of his book on the development of algebra on the basis of what can be called rudimentary constructivist ideas. This was, of course, pre-Brouwerian, and the ideas of Shatunovsky were perhaps more in line with Kronecker's. In any case, this was interesting to see, but it never came to a publication on it with Dirk.

Yanovskaya was his most well-known student, and she was well-respected among the mathematical logicians in Moscow, for whom she effectively provided some sort of ideological cover in the later years. She worked at the department of mathematics at MSU and is well-remembered there.

A good informative article on Shatunovsky is his obituary written by Chebotarev and published, I think, in Uspekhi matematicheskih nauk [link].

By email, Mark van Atten wrote:

A marginal note: There was a brief epistolary exchange between Kagan and Brouwer. They had been put in contact by Mrs Ehrenfest-Afanassjewa. Kagan's letter to Brouwer of June 22, 1922 can be found in The Selected Correspondence of L.E.J. Brouwer (ed. Van Dalen, Springer 2011), pp. 290-291. In that letter Kagan also mentions Schatunowsky (as he, writing in German, spells it) and the latter's work on the development of algebra without the excluded middle.

The date as given by Van Dalen there is 1925. The online-edition of the correspondence at extras.springer.com, which contains all of Brouwer's remaining correspondence (but untranslated), contains that letter twice, once dated 1922, once 1925. 1922 seems to me to be correct as Ehrenfest-Afanassjewa's request to Brouwer to send some material to Kagan was made in that year.

That online edition also includes a short second letter from Kagan, dated Feburay 8, 1925 (on Alexandrov and Urysohn, but without specifically scientific content).

The online edition mentions Shatunovsky once more, in a letter from Alexandrov to Brouwer of March 15, 1927. Commenting on a paragraph in a letter from Brouwer to him, apparently lost, of December 27 [1926], Alexandrov writes: `Im Absatz 8 äussern Sie mir Ihre Meinung über den unsinnigen Artikel von Schatunowski. Da diese Meinung im Stillen auch immer die meinige war, sah ich keinen Grund mich irgendwie dazu zu äussern, und habe mich begnügt, dieselbe an Frau Ehrenfest zur gefälligste Kenntnisnahme mitzuteilen.'

Alas, the online edition contains no mention of Schönfinkel.

Lev responded:

This is an interesting exchange. Is there a way to find out which paper of Shatunovsky was mentioned by Brouwer and Alexandroff as non-sensical? In any case, this assessment could actually be true. From a rather superficial reading of his long work I got the impression that it was a specific way of presenting rather ordinary algebra, without anything revolutionary, accompanied by an introduction stating some philosophical pre-constructivist motivations. The case for doing all this was not a very strong one. But it could well be that they mention some other work that could be either more or less non-sensical that this.

By the way, Kagan was the grandfather of Yakov Sinai, this year's Abel laureate.  I have just watched his interview where he told some story about his grandfather and his friend Shatunovsky from their time in Odessa. Apparently he knows a lot about their lives! These coincidences are quite curious...

Mark responded to Lev's question:

The edition of Brouwer's correspondence does not carry an annotation on this point, unfortunately. Perhaps an educated guess can be made from a full bibliography. Is there one?

The interview Lev mentioned is on youtube. It's in Russian, and Google Translate didn't do a very good job on the transcript, probably because of missing punctuation. I'm attaching it here in case someone wants to play with it.

Some Lesser Known (to me) Russian/Soviet Logicians

Submitted by Richard Zach on Tue, 12/09/2014 - 8:42am

I'm working on a paper that features Moses Schönfinkel, so I was reading through a manuscript of his where he rattles off a long list of important logicians.  In addition to the usual suspects, it features the names "Schatunowski, Sleschinski, Kahan, Poretski."  I spent the better part of a day trying to figure out to whom he was referring:

Samuil Osipovich Shatunovsky (1859-1929) was a mathematician working in Odessa who, so Wikipedia, "independently from Hilbert, he developed a similar axiomatic theory and applied it in geometry, algebra, Galois theory and analysis."

Ivan Vladislavovich Sleshinsky (1854-1931), or Jan Śleszyński in Polish, was an analyst who also wrote on logic who worked in Odessa, where Schönfinkel was his student, and later Krakow. He also translated Couturat's book The algebra of logic into Russian.

Platon Sergeevich Poretsky (1846-1907) worked on Boolean algebraic logic, teaching in Kazan. He's credited with being the first mathematician to teach logic in Russia.

Kahan was a little harder to track down, but apparently Kahan is an alternative transcription of Ка́ган:

Veniamin Fedorovich Kagan (1869-1953) was a geometer and expert on Lobachevsky, who studied in Odessa, Kiev, and St. Petersburg, and worked in Moscow. He grew up in the same city as Schönfinkel, Yekaterinoslav (now Dnipropetrovsk).

In the process of googling about I also happened on Sofya Aleksandrovna Yanovskaya (1896-1966). She studied in Odessa at the same time as Schönfinkel and, like him, was a student of Shatunovsky. She was active in the revolution, and earned a doctorate in 1935 from Moscow State University, where she taught from 1931. In 1943 she founded the the seminar in mathematical logic. According to some sources, she became the first chair of the newly created Department for Mathematical Logic in 1959, however, others as well as the webpage of the institute have A. A. Markov as the first chair, 1959-1979.  From this biography, in addition to her teaching and research in mathematics, she was influential in other interesting ways:

Her work in history and philosophy of mathematics included preparation of a Russian edition of Marx's mathematical manuscripts and the study of Marx's philosophy of mathematics, as well as more general study of philosophy of mathematics. She was interested, for example, in the history of the concept of infinitesimals and her work along these lines included a study of Rolle's contributions. She also paid special attention to the role of Descartes, and in particular to his La Géométrie, in the development the axiomatic approach to mathematics. Her contributions to history and philosophy of logic included work on the problematics of mathematical logic, including problematics related to cybernetics. In the latter regard, an example can be found in the Russian translation of Alan Turing's essay "Can A Machine Think?", which she edited, and in whose introduction she contributed to the discussion of problems in the philosophical aspects of cybernetics through her original analysis of the comparison of the potentialities of man versus machine. She was also instrumental in acquainting Soviet logicians with the work of their Western colleagues through the translation program which she organized, that included the textbooks on mathematical logic of Hilbert and Ackermann, Goodstein, Church, Kleene, and Tarski, and for which she provided important interpretive introductions. She also wrote important and massive historical-expository surveys of Soviet work in mathematical logic and foundations of mathematics.

A special issue of Modern Logic was devoted to her life and work on the occasion of her centenary in 1996; it includes highly interesting articles on her work as well as some smaller biographical items (all open access). Another interesting paper is here.

UPDATE: Follow-up here.

Graduate Programs in Philosophical Logic

Submitted by Richard Zach on Mon, 12/08/2014 - 7:29am

Shawn Standefer has done us all a great service by starting and populating a Wiki of PhD programs in Philosophical Logic!

This wiki provides an unranked list of PhD (and (eventually) terminal M.A.) programs that have strengths in philosophical logic. Links are provided to the websites, CVs, and PhilPapers profiles of the relevant faculty at each program. Additionally, when known, the specialities and willingness of faculty members to work with new graduate students are noted. The primary intended audience is prospective or current graduate students with interests in philosophical logic who want to get the lay of the land by seeing who works where, and on what. This wiki is modeled on Shawn A. Miller’s PhilBio.net wiki.

It's a wiki, so you can edit it: add programs, faculty in your program, edit your own specialities, add a link to your PhilPapers page, etc.!

One person's modus ponens...

Submitted by Richard Zach on Sat, 12/06/2014 - 11:06am

...is another's modus tollens.

[W]hen I was nine years old, I came down with scarlet fever. [...] During that year there was nothing in the world which I wanted so much as a bicycle. My father assured me that when I got well I would get one but, childlike, I interpreted this as meaning that I was not going to get well.

Julia Robinson, in: Constance Reid, The Autobiography of Julia Robinson. The College Mathematics Journal, Vol. 17, No. 1, (1986), pp. 3-21

Adolf Lindenbaum

Submitted by Richard Zach on Sat, 12/06/2014 - 9:25am

Adolf Lindenbaum in 1927 (age 23)Jan Zygmunt and Robert Purdy have a paper ("Adolf Lindenbaum: Notes on his Life, with Bibliography and Selected References", open access) in the latest issue of Logica Universalis detailing what little is known about the life of Adolf Lindenbaum (1904-1941). It includes a complete bibliography of Lindenbaum's own publications and public lectures, as well as a bibliography of articles in which results are credited to Lindenbaum.  Another paper on Lindenbaum's mathematical contributions is in the works.

The entire issue is dedicated to Lindenbaum. Jean-Yves Beziau gives this poignant quote in the introduction:

A mathematician, a modern mathematician in particular, is, as it would be said, in a superior degree of conscious activity: he is not only interested in the question of the what, but also in that of the how. He almost never restricts himself to a solution tout court of a problem. He always wants to have the most ??? solutions. Most what? The easiest, the shortest, the most general, etc.
Lindenbaum was murdered by the Nazis in 1941, at age 37.

Kennedy's Interpreting Gödel Out Now

Submitted by Richard Zach on Tue, 12/02/2014 - 7:56am

Interpreting Gödel: Critical Essays, edited by Juliette Kennedy, was just published by Cambridge. It looks extremely interesting, with an all-star cast of contributors:

1. Introduction: Gödel and analytic philosophy: how did we get here? Juliette Kennedy
Part I. Gödel on Intuition:
2. Intuitions of three kinds in Gödel's views on the continuum, John Burgess
3. Gödel on how to have your mathematics and know it too, Janet Folina
Part II. The Completeness Theorem:
4. Completeness and the ends of axiomatization, Michael Detlefsen
5. Logical completeness, form, and content: an archaeology, Curtis Franks
Part III. Computability and Analyticity:
6. Gödel's 1946 Princeton bicentennial lecture: an appreciation, Juliette Kennedy
7. Analyticity for realists, Charles Parsons
Part IV. The Set-theoretic Multiverse:
8. Gödel's program, John Steel
9. Multiverse set theory and absolutely undecidable propositions, Jouko Väänänen
Part V. The Legacy:
10. Undecidable problems: a sampler, Bjorn Poonen
11. Reflecting on logical dreams, Saharon Shelah.

Two New(ish) Surveys on Gödel's Incompleteness Theorems

Submitted by Richard Zach on Fri, 11/28/2014 - 10:49am

Gödel's incompleteness theorems have many variants: semantic vs. syntactic versions, which specific theory is taken as basic, what model of computability is used, which logical system is assumed to underlie the provability relation, how syntax is arithmetized, what hypotheses the theorem itself uses (soundness, consistency, $\omega$-consistency, etc.). These result in trade-offs regarding simplicity of the proof, but also scope of application and consequences that can be drawn.

There are two new(ish) and super-useful surveys of proofs of Gödel's incompleteness theorem that review these versions and their limitations and scope. The first is by Lev Beklemishev:

Л.Д. Беклемишев (2010). Теоремы Гёделя о неполноте и границы их применимости. I., Успехи Математических Наук 65(5) 61-104. PDF.

English translation:

L. D. Beklemishev (2010). Gödel incompleteness theorems and the limits of their applicability. I., Russian Mathematical Surveys 65(5) 857-898. PDF

The second is by Bernd Buldt:

B. Buldt (2014). The scope of Gödel’s first incompleteness theorem, Logica Universalis. forthcoming. PDF preprint

Lev's is mathematically more exhaustive and more technical; Bernd's is less technical and also goes into philosophically relevant aspects such as Gödel's theorems for system with non-classical underlying logics.

Possible Postdoc on Genesis of Mathematical Knowledge

Submitted by Richard Zach on Fri, 11/28/2014 - 8:52am
Via the APMP list:
Expressions of interest are invited for a postdoc grant (financed by Junta de Andalucia) associated with the following research project: 
“THE GENESIS OF MATHEMATICAL KNOWLEDGE: COGNITION, HISTORY, PRACTICES” (P12-HUM-1216). IP: Jose Ferreiros
Contact: josef@us.es
The grant consists in a 2-year research contract to be held at the University of Sevilla. Salary is in the range of 84000 euros for 24 months. Holders must have obtained their PhD before start of the grant,  [update:] by 2014 and at most 10 years ago (exceptions apply in case of motherhood). They will be doing research along the lines of this interdisciplinary project -- devoted to philosophy of mathematics, links between cognition and mathematical practice, and the interactions logic/mathematics and physics/mathematics.  Knowledge of Spanish is desirable, although it is not a formal requirement.
The call for these grants, issued by Junta de Andalucia, will be open from early December, allowing for only 15 days. Applications will be made to the Junta de Andalucia, but we invite candidates to get in touch with the project IP in advance, so that we can coordinate and assist you.  If you are interested in applying, please contact the IP by email as soon as possible, explaining briefly your situation and interests. Keep in mind that the selection will be made on the basis of fit between the candidate's research project and the topic of the project.

Kalmár's Compleness Proof

Submitted by Richard Zach on Tue, 11/18/2014 - 7:05pm

Dana Scott's proof reminded commenter "fbou" of Kalmár's 1935 completeness proof. (Original paper in German on the Hungarian Kalmár site.) Mendelsohn's Introduction to Mathematical Logic also uses this to prove completeness of propositional logic. Here it is (slightly corrected):

We need the following lemma:

Let $v$ be a truth-value assignment to the propositional variables in $\phi$, and let $p^v$ be $p$ if $v(p) = T$ and $\lnot p$ if $v(p) = F$. If $v$ makes $\phi$ true, then \[p_1^v, \dots, p_n^v \vdash \phi.\]

This is proved by induction on complexity of $\phi$.

If $\phi$ is a tautology, then any $v$ satisfies $\phi$. If $v$ is a truth value assignment to $p_1, \dots, p_n$, let $\Gamma(v,k) = \{p_1^v, \dots, p_k^v\}$. Let's show that for all $v$ and $k = n, \dots, 0$, $\Gamma(v, k) \vdash \phi$. If $k = n$, then $\Gamma(v, n) \vdash \phi$ by the lemma and the assumption that $\phi$ is a tautology, i.e., true for all $v$. Suppose the claim holds for $k+1$. This means in particular $\Gamma(v, k) \cup \{p_{k+1}\} \vdash \phi$ and $\Gamma(v, k) \cup \{\lnot p_{k+1}\} \vdash \phi$ for any given $v$. By the deduction theorem, we get $\Gamma(v, k) \vdash p_{k+1} \to \phi$ and $\Gamma(v, k) \vdash \lnot p_{k+1} \to \phi$. By $\vdash p_{k+1} \lor \lnot p_{k+1}$ and proof by cases, we get $\Gamma(v, k) \vdash \phi$.  The theorem then follows since $\Gamma(v, 0) = \emptyset$.

Notes:

  • The inductive proof of the lemma requires as inductive hypothesis both the claim and the corresponding claim for the case where $v$ makes $\phi$ false (i.e., that then $p_1^v, \dots, p_n^v \vdash \lnot \phi$). Kalmár did not include the constants $T$ and $F$ in the language, but if you would, then Scott's (iii) would be a special case of the lemma.
  • Scott's proof does not require the deduction theorem, but does require proof of substitutability of equivalents.

Dana Scott's Favorite Completeness Proof

Submitted by Richard Zach on Sun, 11/16/2014 - 5:15pm

Last week I gave my decision problem talk at Berkeley. I briefly mentioned the 1917/18 Hilbert/Bernays completeness proof for propositional logic. It (as well as Post's 1921 completeness proof) made essential use of provable equivalence of a formula with its conjunctive normal form. Dana Scott asked who first gave (something like) the following simple completeness proof for propositional logic:

We want to show that a propositional formula is provable from a standard axiomatic set-up iff it is a tautology. A simple corollary will show that if it is not provable, then adding it as an axiom will make all formulae provable.

  1. If a formula is provable, then it is a tautology.

Because the axioms are tautologies and the rules of inference (substitution and detachment) preserve being a tautology. The argument is by induction on the length of the proof.

  1. If a formula is not provable, then it is not a tautology.

We need three lemmata about provable formulae. The symbols $T$ and $F$ are for true and false. We write negation here as $\lnot p$.

  1. $\vdash p \rightarrow [\phi(p) \leftrightarrow \phi(T)]$.
  2. $\vdash \lnot p \rightarrow [\phi(p) \leftrightarrow \phi(F) ]$.
  3. If $\phi$ has no propositional variables, then either $\vdash \phi \leftrightarrow T$ or $\vdash \phi \leftrightarrow F$.

All these are proved by induction on the structure of $\phi$ and require checking principles of substitutivity of equivalences. And I am claiming here this is less work than formulating and proving how to transform formulae into conjunctive normal form.

From (i) and (ii) it follows that: \[\vdash \phi(p) \leftrightarrow [ [ p \rightarrow \phi(T) ] \land [\lnot p \rightarrow \phi(F)] ],\] because we can show generally: \[\vdash \psi \leftrightarrow [ [ p \rightarrow \psi ] \land [ \lnot p \rightarrow \psi ] ].\] Thus, we can conclude: if $\vdash \phi(T)$ and $\vdash \phi(F)$, then $\vdash \phi(p)$. Hence if $\phi(p)$ is not provable, then one of $\phi(T)$, $\phi(F)$ is not provable.

So, if a formula $\phi$ has no propositional variables and is not provable, then by (iii), $\phi \leftrightarrow F$. So it is not a tautology. Arguing now by induction on the number of propositional variables in the formula, if $\phi(p)$ is not provable, then one of $\phi(T)$, $\phi(F)$ is not a tautology. And so $\phi(p)$ is not a tautology. QED

I don't know the answer. Do you?

The only thing it reminded me of was this old paper which shows that all tautologies in $n$ variables can be proved in $f(n)$ steps using the schema of equivalence. It uses a similar idea: evaluate formulas without variables to truth values, and then inductively generate the tautologies by induction on the number of variables and excluded middle.  You could turn that proof into a completeness proof by establishing for a given calculus that the required equivalences and formulas are provable. 

Dana's proof is a lot simpler, though. Thanks to him for allowing me to post his question here.

Lectures on the Epsilon Calculus

Submitted by Richard Zach on Fri, 11/14/2014 - 9:36am

Back in 2009, I taught a short course on the epsilon calculus at the Vienna University of Technology.  I wrote up some of the material, intending to turn them into something longer.  I haven't had time to do that, but someone might find what I did helpful. So I put it up on arXiv:

http://arxiv.org/abs/1411.3629

The Real Reasons Why Philosophers Shouldn't Use LaTeX

Submitted by Richard Zach on Wed, 10/29/2014 - 10:29am

Josh Parsons (Oxford) has written a widely discussed post on "The LaTeX cargo cult," explaining why he discourages philosophy students from using LaTeX.  He makes some interesting points.  But what he has left out is the overarching principle that you should simply always use the best tool for the purpose at hand - and "best" should take into account lots of things: cost (in money and time you need to invest to become proficient in the use of the tool), ease of use, functionality, and the needs of the prospective audience.

For a long time, LaTeX had the upper hand over available alternatives (i.e., Microsoft Word).  It produced high quality output (Word didn't), it was free (Word wasn't), it could do lots of things Word couldn't do (like bibliographies), it was an open format (Word wasn't).  Well, times have changed. There are more alternatives, and the alternatives now can do lots of things they didn't use to be able to. The latest Word document format is open, and based on open standards like XML. There are free, open source alternatives to Microsoft, such as LibreOffice. The alternatives have gotten better at typesetting, and you can now do most of the things in which LaTeX had the upper hand for a long time, e.g., bibliographies and reference management, through plug ins and add-ons (both non-free like Endnote, and free, open, cross-platform like Zotero or JabRef).

So while at one point "well, I use bibliographies and references a lot, and I want to have a nice-looking hardcopy" were sufficient reason to use LaTeX and spurn Word, that's no longer the case.

Given this fact, other considerations should probably play a more important role now when deciding whether to learn LaTeX and when to use it.

  • LaTeX still has a steep learning curve and you can run into complex issues (and simple issues that are hard to solve).  If you have limited amounts of time - say if you're a grad student writing a dissertation - then becoming proficient at and writing everything in LaTeX will probably be a distraction.
  • LaTeX on its own is very bad at revision control and commenting, but Word and LibreOffice are very good at it.  If your piece of writing requires others to read, comment on, and make revisions to it - say, if you're a grad student writing a dissertation with an advisor who doesn't use LaTeX and would like to easily comment on your drafts - then don't use LaTeX. (The same goes for writing any kind of administrative document that anyone else in your institution has to open, comment on, reformat, reuse, or revise!)
  • LaTeX is very good at producing print-based output, but pretty bad at producing output that can easily be reused in other formats - say, on a web page or in a form - so if you need to use your piece of writing in settings where formatted or unformatted text is needed - say, if you're a grad student preparing funding applications via web-based forms - think twice about using LaTeX.
  • LaTeX is very good at making your writing conform to a given format (e.g., a thesis or journal layout), but it can be very time consuming to make LaTeX output conform to a format for which no class or style package exists.  So if there's an Word (or PowerPoint or whatever) template for what you need but no LaTeX style file - then it'll probably be easier to just use that.  (E.g., I wouldn't dream of writing letters of recommendation in LaTeX given that there's an institutional letterhead template.)

Of course all this doesn't mean that you should never use LaTeX, and I think it also doesn't mean that we should discourage students from learning (about) it.  In fact, I think it would be a mistake to do so. There are lots of scenarios in which LaTeX is the best option.  And there are good reasons grad students should at least have a passing familiarity with LaTeX.

  • Do you work in a (sub)field where LaTeX use is prevalent (logic, physics, math)? Then you should probably learn and use LaTeX. (Parsons acknowledges this! But even if all you do is TA intro to formal logic once, learning and using LaTeX can pay off immensely!)
  • Does the thing you're writing need any of the powerful features that LaTeX has but, say, LibreOffice doesn't?  Use LaTeX.
  • Does your advisor use LaTeX and invite you to co-author a paper with her? Learn LaTeX.

There are other reasons to use LaTeX. There are other reasons to not use LaTeX (and scenarios where other tools are better).  But don't not use or learn LaTeX because it's a cargo cult - it isn't - or because it's a proprietary format - it isn't - or because it's not a "declarative language."  It's a powerful tool that's useful in certain contexts. If you find yourself in such a context, learn it, and use it. And given that it is relatively widely used, at least learn what it is so you can make an informed decision. And perhaps encourage your students to do so, too.

Bringing Logic (and Philosophy, CS) to the Masses

Submitted by Richard Zach on Mon, 10/27/2014 - 3:55pm

At this year's Vienna Summer of Logic the organizers did something I haven't seen done before, and which I think should be emulated: over the course of the two weeks that 2,400 logicians were gathered in Vienna, they organized a Logic Lounge in seven instalments.  For an hour each, one or more conference participants engaged in a moderated conversation in front of a general audience in a café near the conference venue. The moderators were well-prepared, and the discussants all had interesting things to say: about what logicians "do," about important results and why they were important, about connections between logic and other areas.  There was a session with Georg Gottlob about how logic regained a foothold in Austrian intellectual discourse and in Vienna's universities in the 1980s (due in large part to people like Peter Weibel, a high-profile Austrian media artist), one on Gödel's theorems, a conversation with Christos Papadimitriou (among other things about Logicomix), one with Moshe Vardi on the ethics of AI, and one on women in logic with Ruzica Piskac and Magdalena Ortiz .  (I unfortunately had two miss the events featuring Roderick Bloem and Byron Cook.) These, I thought, were very successful and engaging ways to bridge the gap between the rarefied and technical academic program of the conferences making up the VSL and the public.

It was a rewarding experience for me: both as a member of the audience, and as the guy that got to explain what the incompleteness theorems are about.  It wasn't something teaching prepares you for: in the classroom, you have audiovisual materials, you can rely on a textbook, you can expect your students to have some background.  In the Logic Lounge, it was basically like explaining Gödel to someone you just met in a bar.  You can't presume anything, you can't use any jargon or formulas, and you have to make sure you give the "big picture" and explain why anyone should care.  I hope I did a decent job.

The organizers put a lot of effort into the events and the "public" aspect of the VSL in general, and I find that very laudable. Logic isn't something you learn about in high school or even in university unless you take a course in it.  It's something the general public only has pretty vague ideas about - but something the specialists think (with good reason) is important and should attract more interest, students, and funding.  The same can be said for philosophy and probably at least for some areas of computer science (theory) and (pure) mathematics.  So why don't more conferences do that sort of thing?

Organizing a conference is a lot of work.  But it's also a valuable opportunity to publicize the value of what we do in academia to the "outside" world.  You'll have a number of able and hopefully willing eminent people available to participate, you don't have to worry about attendance (since at least some of the conference goers will be curious), and you have a chance to raise the profile of your discipline and perhaps the local university department to the public.  Topics aren't hard to find. The ASL could have a keynote speaker chat about infinity or hypercomputation. The PSA could have a philosopher of science talk about scientific evidence and climate change. At LICS you can have someone talk about security and verification of programs, at PLoS about why the language in which you code is important.  And at the APA: any neat topic that would wow students in intro courses: philosophy of travel, existence of god, paradoxes, justice, science and free will  -- but don't just do it like an intro course: have your participants also talk about what they're writing on.  

You need a venue willing to cooperate: since the people attending will all order at least a drink and you're probably running the event before dinner, that should be easy to find.  And you need someone to moderate and ask questions, and that person should probably be someone who isn't an expert - else you run the risk of the conversation ending up at too high a level.  Ask a local journalist, or someone who already has some experience running events like these, e.g., a local Science Café. And then get some publicity: send out a press release (or have the local University send out one).

Thanks to the organizers of the VSL Logic Lounge, Oliver Lehmann and Helmut Veith, to Thomas Kramar (Die Presse) for the keeping us on track, and everyone who came and asked questions!

Proof Formalization in Mathematics: Guest Post by Jeremy Avigad

Submitted by Richard Zach on Mon, 10/20/2014 - 6:34pm

There's a discussion going on at the Foundations of Mathematics mailing list about the purpose and value, actual and potential, for formalized proofs in mathematics.  Harvey Friedman asked Jeremy Avigad to comment; he sent this super-useful list of references, republished here with his approval.

John Harrison and I recently wrote a survey on formalized mathematics, for computer scientists:

Here are some slides from a related talk that I presented at the AMS Joint Meetings in Baltimore earlier this year:

Tom Hales recently wrote a nice piece for the Bourbaki seminar:

He has another lovely survey here (which discusses computation in mathematics more generally):

There is an issue of the Notices of the AMS from 2008 dedicated to formal proof:

I recently wrote a review of Hales' nice book on the proof of the Kepler conjecture, to appear in the Bulletin of Symbolic Logic:

Here is a survey of mine on some of the difficulties involved in making sense of ordinary mathematical language and notation:

There is now a substantial literature on formal mathematics, and writeups of formalizations regularly appear in conferences like Interactive Theorem Proving (ITP), as well as journals like the Journal of Automated Reasoning. Homotopy type theory has also gotten a lot of press lately, in parts for its interest as a new framework for verification.

Here are some formalizations I personally have worked on:

Most of these have something to say about the current challenges and difficulties.

There are number of good interactive theorem provers out there. I am currently involved in the design and library development for a new one, Lean, being developed by Leonardo de Moura at Microsoft (it is an open source project): 

https://github.com/leanprover/lean

There are slides describing it.  It is in its early stages, and not yet fully functional, but I am excited about it. We are aiming for a public "release" early next year.

As indicated in many of the publications just listed, progress is needed before interactive theorem provers are commonly used, though I am absolutely certain it will eventually happen. This includes things like developing better user interfaces, automated support, and libraries. A student of mine, Rob Lewis, and I are working on a heuristic method of proving real-valued inequalities, described here:

Jeremy Avigad, Robert Y. Lewis, Cody Roux, 2013, "A heuristic prover for real inequalities," arXiv:1404.4410 and LNCS 8558 (2014)

Many others are developing other types of automation, both for the purposes of supporting the verification of mathematical proof, and for supporting the verification of hardware and software.

I apologize for over-emphasizing my own projects; there is a tremendous amount of work being done in the area of now, and mine is just a small part of it. I once heard Natarjan Shankar say that this is "the golden age of metamathematics," and I agree.  This is a really exciting time to be working with formal methods.

Awodey's "HoTT for Philosophers" on mathtube.org

Submitted by Richard Zach on Fri, 10/17/2014 - 9:04am

Steve Awodey's talk in the Calgary Mathematics & Philosophy lecture series ("Univalence as a New Principle of Logic" aka "HoTT for Philosophers") is now up on mathtube.org.

bpextra: new version v 0.2

Submitted by Richard Zach on Thu, 10/16/2014 - 9:22pm

I've fixed a bug in bpextra.The new version can be downloaded from github.

See also this issue for how to define your own deduction styles.

SotFoM II: Competing Foundations

Submitted by Richard Zach on Thu, 10/16/2014 - 2:49pm

The second installment of SotFom (Symposium on the Foundations of Math) is asking for papers by Halloween:

http://sotfom.wordpress.com/2014/10/14/final-cfp-and-extended-deadline-s...

FINAL CFP and *EXTENDED DEADLINE*: SoTFoM II `Competing Foundations?’, 12-13 January 2015, London.

The focus of this conference is on different approaches to the foundations of mathematics. The interaction between set-theoretic and category-theoretic foundations has had significant philosophical impact, and represents a shift in attitudes towards the philosophy of mathematics. This conference will bring together leading scholars in these areas to showcase contemporary philosophical research on different approaches to the foundations of mathematics. To accomplish this, the conference has the following general aims and objectives. First, to bring to a wider philosophical audience the different approaches that one can take to the foundations of mathematics. Second, to elucidate the pressing issues of meaning and truth that turn on these different approaches. And third, to address philosophical questions concerning the need for a foundation of mathematics, and whether or not either of these approaches can provide the necessary foundation.

Date and Venue: 12-13 January 2015 – Birkbeck College, University of London.

Confirmed Speakers: Sy David Friedman (Kurt Goedel Research Center, Vienna), Victoria Gitman (CUNY), James Ladyman (Bristol), Toby Meadows (Aberdeen).

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). While we welcome submissions from all areas concerned with foundations, particularly desired are submissions that address the role of and compare different foundational approaches. Applicants should prepare an extended abstract (maximum 1,500 words) for blind review, and send it to sotfom [at] gmail [dot] com, with subject `SOTFOM II Submission’.

Submission Deadline: 31 October 2014

Notification of Acceptance: Late November 2014

Scientific Committee: Philip Welch (University of Bristol), Sy-David Friedman (Kurt Goedel Research Center), Ian Rumfitt (University of Birmigham), Carolin Antos-Kuby (Kurt Goedel Research Center), John Wigglesworth (London School of Economics), Claudio Ternullo (Kurt Goedel Research Center), Neil Barton (Birkbeck College), Chris Scambler (Birkbeck College), Jonathan Payne (Institute of Philosophy), Andrea Sereni (Universita  Vita-Salute S. Raffaele), Giorgio Venturi (CLE, Universidade Estadual de Campinas)

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

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

Further Inquiries: please contact
Carolin Antos-Kuby (carolin [dot] antos-kuby [at] univie [dot] ac [dot] at)
Neil Barton (bartonna [at] gmail [dot] com)
Claudio Ternullo (ternulc7 [at] univie [dot] ac [dot] at)
John Wigglesworth (jmwigglesworth [at] gmail [dot] com)

The conference is generously supported by the Mind Association, British Logic Colloquium, and Birkbeck College.

Pages