Logblog: Richard Zach's Logic Blog

University of Calgary

UofC Navigation

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

Submitted by Richard Zach on Sat, 06/28/2014 - 7:54am

More sad news, via the Studia Logica list:

We sadly inform that Professor Joachim Lambek (Jim for friends) passed away on June 23, 2014, at 2:00 p.m. in Montreal.

Joachim Lambek was born in Leipzig on December 5, 1922. His parents moved to Leipzig from a small town near Krakow (Poland). In the late 1930-ties the family left Germany for England. After the outbreak of the SWW, he spend two years in an internment camp in Canada, then entered McGill University in Montreal. He earned Ms.C. in mathematics in 1946. This university has remained his affiliation throughout his academic career; in the years 1963-1993 he was a professor at the Department of Mathematics and Statistics and occupied the Peter Redpath Chair, then a professor emeritus at McGill. He has visited many universities and research centers in Europe and America.

J. Lambek's scientific interests focused on algebra, category theory, mathematical logic, mathematical linguistics and number theory. In category theory he developed categorical logic, e.g. he has shown close connections between cartesian closed categories and typed lambda calculi. In mathematical linguistics, Lambek's Syntactic Calculus, introduced in 1958 (nowadays called Lambek Calculus), is a basic logic for modern type grammars. This calculus and its different variants are extensively studied also in algebraic logic as the basic substrutural logics. In the last decades J. Lambek developed an algebraic approach to grammar, involving pregroups. He also studied some algebras of physics (quaternions) and published books on the history of mathematics.

Submitted by Richard Zach on Thu, 06/19/2014 - 11:19am

So while everyone is following the World Cup, I'm getting excited about the FLoC Olympic Games to be held at the Vienna Summer of Logic this year. Still doing my research to pick favourites, but here are some of the disciplines:

- Answer Set Programming (ASP) Model & Solve, divided into single- ("Men's") and multi-processor ("Women's") competitions.
- Automated Theorem Proving, with events in Typed Higher-order Theorems, First-order Theorems (with/without arithmetic, with/without identity), etc.
- Term Rewrite System Confluence, with events in First-order and Conditional Term Rewrite Systems Confluence as well as Certification of Confluence Proofs
- Boolean Satisfiability Solving is the biggest event with two separate competitions, plus a competition in MAXSAT.
- Quantified Boolean Formulas has events in QBF Solving, Preprocessing, and Certification.
- Hardware Model Checkers compete in Single safety, Liveness, and Deep Bound.
- Web Ontology Language (OWL) reasoning competitions will be held in Consistency Checking, Classification, and Realisation

plus a few others. There will even be **live viewing** and a medal ceremony!

Submitted by Richard Zach on Sun, 06/08/2014 - 5:12am

Submitted by Richard Zach on Fri, 05/30/2014 - 5:46am

Very sad news today: Grisha Mints has died. He was born June 7, 1939 in Leningrad (now St. Petersburg). He received his education in mathematics at Leningrad State University under N. A. Shanin, and held positions there, at the Steklov Institute in Leningrad, and then, from 1980-1991, at the Estonian Academy of Science in Tallinn. In 1991 he joined the Philosophy Department at Stanford University, where he also held courtesy appointments in computer science and mathematics (since 1992 and 1997, respectively). In 2008 he was elected to the Estonian Academy of Sciences, and in 2010 named a fellow of the American Academy of Arts and Sciences.

Grisha was a force in logic, especially in proof theory. His early work centered on systems for automated theorem proving, where he contributed significantly to the development of Maslov's inverse method, resolution, and the relation between the two. He made major contributions to general proof theory, non-classical logics, constructive mathematics, program verification, and proof mining. He was the leading expert on Hilbert's epsilon calculus and the substitution method approach to the proof theory of strong subsystems of arithmetic. In addition to over 200 papers, he wrote two introductory books on modal and intuitionistic logic, and some of the early papers from his days in the Soviet Union were collected in his *Selected Papers in Proof Theory*.

I'm grateful to have had many beautiful interactions with Grisha over the years. The logicians at the TU Vienna had close contacts with Tallinn in the late 80's and early 90's, and I had the good fortune to meet Grisha then. While at Berkeley and Stanford, I attended a couple of his classes. He was a demanding teacher, but I learned a lot. I often visited before I taught at Stanford, and a few times since I've left. Whenever I did, he would ask me what I was working on, and he'd acknowledge what I'd said with a smile and a sideways nod and "um-hmm." Often he would then tell me about some obscure, usually Soviet-era, book or paper that addressed all the problems and questions I had. Then came the part where he'd tell me about his current work, and I would struggle to keep up. I'll always fondly remember those visits. He was a wonderful, generous teacher and colleague.

UPDATE: Memorial notice from Stanford's department chair Lanier Anderson.

Submitted by Richard Zach on Thu, 05/29/2014 - 2:26pm

Here's a simple way to pretty-print documentation included as comments in a source file (I'm mainly interested in LaTEX code), with or without the intervening code. It's useful if you don't want to bother with a more complicated solution such as LaTeX's docstrip + ltxdoc. It uses the ubiquitous bash tools grep and cut (available on Linux and probably (?) on Mac OS) plus John MacFarlane's pandoc , which you might have to install separately.

Include your documentation in the source file as comments, i.e., in LaTeX, on lines which start with %. Make sure they in fact start with "% ", i.e., % followed by a space. Your documentation can use any format pandoc understands, but Markdown is probably the simplest. Your comments will be easily readable in the source file, but you can include markup, e.g., # headers, *italicized* or **boldface**, `code`, \$math\$, itemized lists, etc. Because your documentation is a regular comment that doesn't have to be stripped for the file to compile, you can use/compile your source file as you ordinarily would without running it through a pre-processor. To get the documentation, you filter out the non-commented lines, removethe comment signs, and run them through pandoc.

Submitted by Richard Zach on Thu, 05/29/2014 - 12:36pm

Just came via the proof theory mailing list. I'm wondering why the ASL is not mentioned along with the EATCS, EACSL, and KGS.

Submitted by Richard Zach on Thu, 05/29/2014 - 6:46am

The Arthur Prior Centenary Conference will be held at Balliol College, Oxford, on 21–22 August 2014, to celebrate the work of Arthur Norman Prior (1914-1969). Prior was a Fellow of Balliol and famous for his contributions to logic, ethics and metaphysics, but most of all he is known as the founder and principal inventor of modern symbolic temporal logic; for more details, see the conference website.

Submitted by Richard Zach on Tue, 05/27/2014 - 1:49pm

*Ergo* is a new general philosophy journal, open access, licensed under CC, with an innovative editorial model and triple-blind review. Their first issue with four papers was published today, the papers are discussed on topic-appropriate blogs.

Read the report on submissions, turn-around times, etc., by the editors Jonathan Weisberg and Franz Huber here.

Submitted by Richard Zach on Fri, 05/23/2014 - 11:47am

Within the VIDI project ‘The Roots of Deduction’ led by Catarina Dutilh Novaes, the Faculty of Philosophy of the University of Groningen is advertising a **12-month post-doc position**, to commence in January 2015 or shortly thereafter.

Submitted by Richard Zach on Sat, 05/17/2014 - 10:34am

Bored by small powers of 2? You can now play 2048, but with large cardinals instead. For the long version, you have to get all the way to 0=1.

Fork by Chris Le Sueur, h/t David Schrittesser

Submitted by Richard Zach on Thu, 05/15/2014 - 12:17pm

The SEP finally has an entry on Jan Łukasiwicz, by Peter Simons:

Jan Łukasiewicz (1878–1956) was a Polish logician and philosopher who introduced mathematical logic into Poland, became the earliest founder of the Warsaw school of logic, and one of the principal architects and teachers of that school. His most famous achievement was to give the first rigorous formulation of many-valued logic. He introduced many improvements in propositional logic, and became the first historian of logic to treat the subject’s history from the standpoint of modern formal logic.

Submitted by Richard Zach on Wed, 05/07/2014 - 12:42pm

Helmut Veith and I are organizing a special session at the Logic Colloquium in Vienna. The panelists will be Byron Cook (Microsoft Research), Alexander Leitsch (University of Technology Vienna), Prakash Panangaden (McGill University), Nicole Schweikardt (Goethe-University Frankfurt am Main). The abstract copied from the ASL Committee on logic Education page:

Logic has been called the "calculus of computer science" - and yet, while any physics student is required to take several semesters of calculus, the same cannot be said about logic and students of computer science. Despite the great and burgeoning activity in logic-related topics in computer science, there has been very little interest, in North America at least, in developing a strong logic component in the undergraduate curriculum. Meanwhile, in other parts of the world, departments have set up specialized degree programs on logical methods and CS. This special session, organized under the auspices of the ASL's Committee on Logic Education, aims to explore the role of logic in the computer science curriculum. How are computer scientists trained in logic, if at all? What regional differences are there, and Is a greater emphasis on logic in the computer science undergraduate curriculum warranted, both from the point of view of for research in CS and from the point of view of training for industry jobs? What should an ideal "Logic for Computer Science" look like?

Byron Cook believes that, in the rush to create engineers and scientists, we have lost sight of the fact that an education should be

broad and place emphasis on principles rather than specific skills such as Javascript. Logic is the perfect topic in this setting, as it

has application in both humanities and science, and fosters a discussion about mechanics while not requiring a significant amount of

technical overhead.The Association for Computing Machinery has just chartered a new Special Interest Group on Logic and Computation (SIGLOG). Education is one of the prime concerns of this new SIG and one of the activities on the SIG's education committee will be to advocate for a greater presence of logic in the curriculum. Prakash Panangaden discusses the aims of the new SIG with particular emphasis on its educational mission.

Nicole Schweikardt will report on experiences with designing an undergraduate introductory course on logic in computer science at

Goethe-University Frankfurt.The University of Technology Vienna participates in a European Masters program in computational logic and has just started a doctoral program in Logical Methods in Computer Science. Alexander Leitsch describes these initiatives and considers lessons other departments can draw from the Vienna experience.

Submitted by Richard Zach on Mon, 05/05/2014 - 7:28pm

Wow. Learn something new every day.

a) BASIC just turned 50 years old four days ago.

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

Please add your favorite Frege joke in comments (or tweet @RrrichardZach with #fregejokes hashtag).

Doesn't have to be good. In fact, just any logic joke is fine.

Submitted by Richard Zach on Sun, 05/04/2014 - 5:09pm

Check out the funded doctoral program in logic in computer science!

TU Wien, TU Graz, and JKU Linz are seeking exceptionally talented and motivated students for their joint doctoral program LogiCS. The LogiCS doctoral college focuses on interdisciplinary research topics covering

(i) computational logic, and applications of logic to

(ii) databases and artificial intelligence as well as to

(iii) computer-aided veriﬁcation.

LogiCS is a doctoral college focusing on logic and its applications in computer science. Successful applicants will work with and be supervised by leading researchers in the fields of computational logic, databases and knowledge representation, and computer-aided

verification.

We are looking for 1-2 doctoral students per faculty member, where 30% of the positions are reserved for highly qualiﬁed female candidates. The doctoral positions are funded for a period of 3 years according to the funding scheme of the Austrian Science Fund (details: http://www.fwf.ac.at/de/projects/personalkostensaetze.html) The funding can be extended for one additional year contingent on a

placement at one of our international partner institutions.

The applicants are expected to have completed an excellent diploma or master's degree in computer science, mathematics, or a related ﬁeld. Candidates with comparable achievements will be considered on a case-by-case basis. Applications by the candidates need to be

submitted electronically.

Submitted by Richard Zach on Thu, 05/01/2014 - 12:16pm

The LaTeX package bussproofs.sty for typesetting natural deduction/sequent calculus proofs is nifty especially for its nice alignment of sequents. By contrast to the proof.sty package, it doesn't allow you to typeset missing parts of a proof, though. proofs.sty has the \deduce command for that; it typesets vertical dots instead of a horizontal inference line.

I wrote an add-on for bussproofs.sty that does the same. Not quite ready for prime time yet, but if you like playing with bleeding-edge stuff, you can get it here. Feedback? Please file an issue on github.

Submitted by Richard Zach on Tue, 04/29/2014 - 12:28pm

All-around awesome logician colleagues and friends Steve Awodey and Jeremy Avigad have netted a $7.5m, 5-year grant to develop Homotopy Type Theory!

http://www.cmu.edu/news/stories/archives/2014/april/april28_awodeygrant....

http://homotopytypetheory.org/2014/04/29/hott-awarded-a-muri/