Logblog: Richard Zach's Logic Blog

University of Calgary

UofC Navigation

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.

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.

- 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.

- 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$.

- $\vdash p \rightarrow [\phi(p) \leftrightarrow \phi(T)]$.
- $\vdash \lnot p \rightarrow [\phi(p) \leftrightarrow \phi(F) ]$.
- 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.

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:

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.

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!*

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:

- Jeremy Avigad, John Harrison, 2014, "Formally verified mathematics."
*Communications of the ACM*57: 66-75

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

- Jeremy Avigad, 2014, "Formal verication, interactive theorem proving, and automated reasoning"

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

- Thomas C. Hales, 2013-14, "Developments in formal proofs",
*Séminaire Bourbaki*1086

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

- Thomas C. Hales, 2013, "Mathematics in the age of the Turing machine," arXiv:1302.2898

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

- Special Issue on Formal Proof, with contributions by Tom Hales, Georges Gauthier, John Harrison, and Freek Wiedijk

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:

- Jeremy Avigad, 2012, "Type inference in mathematics," arXiv:1111.5885

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:

- The central limit theorem
- The Feit-Thompson theorem
- Homotopy limits, in the framework of homotopy type theory:
- The prime number theorem

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.

Submitted by Richard-Zach on Mon, 10/20/2014 - 12:00pm

Just found out that Edward Nelson died last month.

http://www.princeton.edu/main/news/archive/S41/11/36I14/index.xml

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.

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.

Submitted by Richard-Zach on Tue, 10/14/2014 - 12:03pm

Did you know? The *Moritz Schlick Gesamtausgabe* is available for free at the Moritz-Schlick-Forschungsstelle! Just click on the cover image to download the PDF (instead of the "order online" link). Alas, it's only in German.

Submitted by Richard-Zach on Mon, 10/13/2014 - 8:16am

If you're in that part of the world (or will be in January), you might be interested to know that registration for the 8th Annual Cambridge Graduate Conference on the Philosophy of Mathematics and Logic (17-18 January 2015) is now open:

The conference will be held in St. John's College, Cambridge. There will be two keynote speakers and six talks from graduate students on a variety of topics in the Philosophy of Mathematics and Logic, broadly construed. The graduate papers will have respondents, and the talks will be followed by open discussion. The keynote speakers this year are Prof Alan Weir (Glasgow) and Dr Mary Leng (York)To register for the conference please click here. Registration will close on Monday the 1st of December 2014.

For more information please see the conference website:

http://www.phil.cam.ac.uk/events/camb-grad-conf-2015

Submitted by Richard Zach on Thu, 10/02/2014 - 9:36am

Hilary Putnam is writing on Tarski's theory of truth (and Field's analysis of it) at Sardonic Comment. First two blog posts are up:

http://putnamphil.blogspot.ca/2014/09/first-of-series-of-posts-on-tarski...

http://putnamphil.blogspot.ca/2014/09/a-second-post-on-tarski-this-post....

Submitted by Richard Zach on Wed, 10/01/2014 - 3:17pm

I'm very excited that Steve Awodey is on his way here to deliver the first Calgary Mathematics & Philosophy Lecture tomorrow! He's speaking on "Univalence as a New Principle of Logic." If you're in Calgary, you should come. It'll be exciting. Thursday, 3:30 pm, in Engineering Building A aka ENA 101 on the UofC campus. Here's the abstract:

It is often convenient or useful in mathematics to treat isomorphic structures as the same. The Univalence Axiom for the foundations of mathematics elevates this idea to a foundational principle in the setting of Homotopy Type Theory. It states, roughly, that isomorphic structures can be identified. In his talk, Prof. Awodey will explain this principle and how it can be taken as an axiom, and explore the motivations and consequences, both mathematical and philosophical, of making such an assumption.

Steve will give a more technical talk in the Math Department on Friday at 2pm.

Also check out the sweet poster:

Submitted by Richard Zach on Tue, 09/23/2014 - 10:51am

I've been having a conversation with Alex Douglas and Eric Schliesser on their posts (Alex's, Eric's) about Milton Friedman's footnote about observer-dependence and Gödel's incompleteness theorem.

Submitted by Richard Zach on Mon, 08/04/2014 - 2:21am

John Venn would have been 180 today (August 4). In celebration, Google put up an interactive Venn Diagram doodle, which is pretty amazing.

Also, TIL that it's not a Venn diagram if it doesn't contain all possible intersections, a restriction that doesn't apply to Euler diagrams. So representing an empty intersection by two non-intersecting regions is, technically, not a Venn diagram; and Venn diagrams for more than three sets get harder and harder to draw. Check out the informative Wikipedia entry.

I have a previous entry on humorous Venn (and Euler) diagrams around the Internets.

Submitted by Richard Zach on Thu, 07/24/2014 - 3:51am

The Café Reichsrat in Vienna is notable as the place where Gödel, on August 26, 1930, first announced the incompleteness theorem to Carnap, Feigl, and Weismann. The members of the Vienna Circle had met there to prepare for the trip to the "Zweite Tagung für Erkenntnislehre der Exakten Wissenschaften," a satellite meeting to the congress of the German Society of Mathematicians organized by the Vienna Circle. This was where the famous symposium on the foundations of mathematics took place, with Carnap representing logicism, Heyting intuitionism, and von Neumann speaking for Hilbert's school of formalism -- the contributions are reprinted in Benacerraf's anthology *Philosophy of Mathematics*. From Carnap's diary: "6-1/2 9 [6pm to 8:30pm] Cafe Reichsrat ... preparations for the trip to Königsberg. Gödel's discovery: incompleteness of the system of *Principia Mathematica* ... difficulties of the consistency proof." In February 1930, Gödel and Tarski discussed logic here during the latter's first visit to Vienna.

The Reichsrat no longer exists, and the only picture that's around shows just the top of one of its doors (from Jimmy Schimanovich's photo gallery).

The window atop the door, columns, and stucco match the entrance to the Konditorei Sluka at Rathausplatz 8, and presumably on the basis of this it's long been believed that the Reichsrat used to be located where the Sluka is now. But the Sluka has been around since 1891, which led Paul Raymont to speculate that it expanded into the Reichsrat's space after the latter closed down. In 2010, Karlis Podnieks noticed that on the other side of the main driveway to Rathausplatz 8 there's another door that also looks like the one in the picture, and conjectured that the Reichsrat might have been located there. But Vienna's *Kaffeehäuser* were cavernous establishments and also almost all located at corners. So I asked Karl Sigmund, co-editor of *Kurt Gödel: The Album* and creator of the Gödel Exhibition, for help, and he suggested to check the phone book! And indeed, *Adolph Lehmann's allgemeiner Wohnungs-Anzeiger : nebst Handels- u. Gewerbe-Adressbuch für d. k.k. Reichshaupt- u. Residenzstadt Wien u. Umgebung* gives the address for the Reichsrat as Stadiongasse 2.

The Café Reichsrat was thus located at the north-west corner of Stadiongasse and Reichsratsstraße/Rathauspark, and the archive picture probably shows the mid-block back entrance facing the Rathauspark identified by Podnieks. A bank now occupies the space:

If you go visit, do have a coffee and cake at the Sluka! I also made a map for all you Gödel pilgrims.

And here is some background reading:

- John W. Dawson, Jr., Karl Sigmund, 2006. Gödel’s Vienna.
*The Mathematical Intelligencer*28(3), 44-55

For an almost complete list of people and places from the time of the Vienna Circle, consult:

- Volker Thurm, 2003.
*Wien und der Wiener Kreis: Orte einer unvollendeten Moderne: Ein Begleitbuch*, Vienna: facultas.wuv / maudric

Submitted by Richard Zach on Mon, 07/21/2014 - 4:42am

A group of researchers in philosophy, psychology and mathematics are requesting the assistance of the mathematical community by participating in a survey about mathematicians’ philosophical intuitions. The survey is here: http://goo.gl/Gu5S4E. It would really help them if many mathematicians participated. Thanks.

Submitted by Richard Zach on Thu, 07/17/2014 - 4:42am

The Special Session on "The Place of Logic in Computer Science Education" took place at the Logic Colloquium on Tuesday. It was well attended and, I think, overall a successful session. The newly-formed ACM Special Interest Group on Logic and Computation (SIGLOG) was represented by its chair Prakash Panangaden. He stressed the importance of logicians (and computer scientists/instructors relying on logic and logical methods) to push for the integration of logical methods in the CS curriculum -- the way the SIG on Programming Languages SIGPLAN has successfully managed to give prominence to programming languages and design. In the US, the existence of a standard curriculum makes it difficult for departments that would even want to put a focus on logic and formal methods to introduce dedicated courses, a point made by Phokion Kolaitis in discussion. That curriculum includes only propositional logic and just the very basics of predicate logic as a requirement for all CS majors. In a previous panel at a SIGCSE meeting, it was argued that a remedy would be to integrate bits of logic in other courses where logical methods are needed. This resulted in the TeachLogic Project, led by Moshe Vardi at Rice University, which aimed to provide course materials and ideas for where and how to incorporate logic into CS courses.

In Europe, departments seem to have a lot more leeway. This makes it possible, e.g., for Austrian CS departments to even offer specialized grad programs in logic and computing, as Alex Leitsch reported. Nicole Schweikardt presented ideas from an introductory course she teaches in Frankfurt. One of her didactic lessons was that engaging examples are important to draw in students -- pure logic courses tend to do a less-than-optimal job at convincing students that this stuff is useful and important. Her "provocative statement was: "When confronting computer science students with formal logic for the first time, we should dare to be less formal." This tied in with another topic of discussion: diversity. In the US, the gender split in CS is even worse than in philosophy: 12% of 2010-11 CS degrees were awarded to women. Byron Cook also mentioned this as an issue, and pointed to Harvey Mudd College as a success story for how to get and keep members of underrepresented groups in(to) CS. Now Harvey Mudd is an elite college and in many places that kind of institution-wide initiative is sadly not feasible (as Phokion pointed out).

There are lessons to be learned, not just for how we teach formal methods in CS but also for logic courses in philosophy departments. One may be to make these courses -- not: less rigorous -- but simply more appealing by focussing more on examples and applications which are familiar and engaging to a broader audience that's not already familiar with formal methods. In the discussion, Brigitte Pientka pointed out, however, that it would be a mistake to think that we have sacrifice rigor in logic or CS courses to make them appealing to women and enable them to succeed in them. She referred to the environment at Carnegie Mellon University and the research by Carol Frieze and others who have documented that a more balanced environment allows both men and women to participate, contribute, and be successful, in the CS major, without accommodating presumed gender differences or watering down the curriculum to become "more female friendly". Since 2002 the percentage of bachelor‘s degrees granted to women in the CS major at CMU has exceeded and stayed well above the national average. It is currently at 25%. These and other initiatives are covered in a piece on drawing women to computer science published in the NYT's TheUpshot blog just yesterday.

SIGLOG is forming an Education Committee, which will carry on the work of the TeachLogic project and hopefully can serve as a clearing house for ideas, materials, and tools. If you're interested in being involved, Prakash would like to hear from you! In addition, this would be a good place to announce that the conference Tools for Teaching Logic is happening again next year!

(Cross-posted at the Vienna Summer of Logic blog.)

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

So there will be a student party at the Summer of Logic. Help me crowdsource logic/math/CS/AI tracks, preferably danceable. Ideas?

Pet Shop Boys - He Dreamed of Machines

Turing Machines - Slave to the Algorithm

My Robot Friend - Robot High School

Super Furry Animals - Fuzzy Logic

Daniel Avery - Drone Logic

Scooter - The Logical Song [Supertramp cover]

Squarepusher - Music for Robots

The Illuminator - 4 r square pi (Association for Symbolic Logic)

Or I guess we can just play Logic all night:

Logic - Mind of Logic / The Spotlight / ...

or A-Track's "Infinity + 1" mix and the entire Stills album "Logic will Break your Heart."

- Kalmár's Compleness Proof
- Dana Scott's Favorite Completeness Proof
- Lectures on the Epsilon Calculus
- The Real Reasons Why Philosophers Shouldn't Use LaTeX
- Bringing Logic (and Philosophy, CS) to the Masses
- Proof Formalization in Mathematics: Guest Post by Jeremy Avigad
- Edward Nelson, 1932-2014
- Awodey's "HoTT for Philosophers" on mathtube.org