# Grigori Mints, 1939-2014

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.

# Simple Way to Document Code with Markdown, grep, and pandoc

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.

First, we have to filter out the non-comment lines from the source file and throw away the rest. This can be done using grep:

    grep -e "^%" -e "^$"  The first filter “^%” matches any line beginning with a %, the second “^$” matches empty lines (so you get paragraph breaks between documentation blocks in the output).

Then you want to strip the initial comment character; in fact, we can just throw away the first two characters of every remaining line, using the cut command

    cut --bytes=3-


The result is a file in Markdown format which you can now run through pandoc to create your favorite output, e.g., HTML or PDF.

    pandoc -f markdown -t html


You can put all of this together into a pipe, or make a bash script, or use it in a Makefile target. For instance, if you save the following as “makedoc”

    #!/bin/bash
grep -e "^%" -e "^$$" 1.tex | cut --bytes=3-| pandoc -f markdown -o 1.pdf  you can use “./makedoc <mytexfile>” to produce a PDF of the documentation included in <mytexfile>.tex in <mytexfile>.pdf. (Note the double$$ and make sure you make the file executable, e.g., via chmod u+x makedoc).

To set title, author, and date of the documentation, include them, preceded by an extra “% ” in the first three lines of your file (in that order).

The procedure above will filter out the comments and turn them into the documentation, e.g., a user guide or something like that.  You can also set it up to print a documented source by beginning and ending every block of code with a commented “code fence”, i.e., a line that contains “% “” (%, space, three backticks). Then we’ll run the file first through sed and tell it to remove all the “% ” at the beginning of a line.

    sed "s/^% *//" $1.tex | pandoc -f markdown -o$1.pdf


Extra geek points for the person to come up with a sed command to print any commented line and all lines between code fences but remove code not between code fences!

UPDATE: The extra geek points go to Mark van Atten who sent in this solution using awk:

Yours sincerely,
SIGLOG Chair

# Arthur Prior Centenary Conference, August 21-22, 2014

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.

The two-day conference will concentrate on logical, philosophical, mathematical and computational research concerned with, or inspired by, Prior’s work. Accepted papers will (with the final approval of Synthese) be published as a special issue of Synthese.

It is being held by the Royal School of Library and Information Science, University of Copenhagen, and the Department of Communication and Psychology, Aalborg University, in partnership with Balliol College and the University of Oxford. The organisers are:

• Professor Dr Per Hasle, Director of the Royal School of Library and Information Science, University of Copenhagen, Denmark (General Chair)
• Professor Dr Jack Copeland, University of Canterbury, Christchurch, New Zealand (New Zealand Chair)
• Professor Dr Peter Øhrstrøm, Aalborg University, Denmark (Program Chair)

# Ergo Publishes First Issue, Report

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.

First issue: http://www.ergophiljournal.org/

Julia Jorati (OSU) on a paper in early modern by Paul Lodge (Oxford):

Anna Mahtani (LSE) on a paper by Michael Caie (Pittsburgh):
http://choiceandinference.com/, http://m-phi.blogspot.ca/

Ellen Clark (Oxford) on a paper in philosophy of biology by
Christopher Hitchcock (Caltech) and Joel Velasco (Texas Tech):
http://philosomama.blogspot.co.uk/

Thomas Nadelhoffer (Charleston) on a paper in experimental philosophy
by John Turri (Waterloo):

# Post-doc in Groningen: The Roots of Deduction

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.

Given the broad scope of the project, candidates with a number of different backgrounds will be considered, as long as they have a keen interest in the general topic of deductive proofs in logic and mathematics. In particular, candidates may have the following areas of expertise:

• Ancient logic
• Ancient mathematics (Greek as well as other traditions)
• Philosophical logic and philosophy of logic
• Philosophy of mathematics and philosophy of mathematical practice (proofs in particular)
• Dialogical logic and games in logic
• Deductive and mathematical cognition (psychology/cognitive science)

More details here.

# SEP Entry on Łukasiewicz

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.

# The Place of Logic in Computer Science Education

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

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.

# Did You Know Who Invented BASIC!?

Wow. Learn something new every day.

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

b) You know who invented BASIC? John G. Kemeny, student of Alonzo Church, and the guy who’s credited with first defining the now-standard notion of truth in a model!

(Kemeny was apparently also a great president at Dartmouth, opening the college to women students and championing women faculty.)