Logblog: Richard Zach's Logic Blog

University of Calgary

UofC Navigation

You are looking at the old blog archive. LogBlog has moved to richardzach.org.

If you'd like to receive updates on new posts, please subscribe there!

Submitted by Richard Zach on Tue, 09/01/2009 - 1:45am

I had to look up a Russell quote the other day, and that's when I noticed that many of his books -- including the Foundations of Geometry, Our Knowledge of the External World, Introduction to Mathematical Philosophy, Analysis of Mind, Principles of Mathematics, Mysticism and Logic, and Principia Mathematica (annoyingly, only vol. II) -- are available in their full glory through Google Books. There are lots of other gems, including Hilbert's Grundlagen der Geometrie, the Tractatus, etc. But beware: the Google metadata are unreliable, to say the least (see Geoff Nunberg on Google Books: A Metadata Trainwreck).

Submitted by Richard Zach on Fri, 08/28/2009 - 3:34pm

Here's another article in the "you might not have thought it but philosophy undergrads are actually doing well in careers in business and law" mold, from a Canadian perspective.

Philosophy’s makeover: Why job prospects for philosophy grads are brightening, by Daniel Drolet

Submitted by Richard Zach on Fri, 08/28/2009 - 3:24pm

- Read more about T-Rex on Vagueness
- Richard Zach's blog
- 2 comments
- Log in to post comments

Submitted by Richard Zach on Mon, 08/24/2009 - 5:19pm

A long time ago I posted on Richard Statman's dissertation work on the geometrical complexity of proofs: take a proof in natural deduction, interpret the formulas in it as nodes of a graph with edges going from premise to conclusion of an inference and from assumption to the (conclusion of the) inference where it is discharged. The genus of that graph is an interesting complexity measure. Ale Carbone has also worked on this complexity measure, and now has an exciting paper entitled "Logical structures and genus of proofs" forthcoming in the Annals of Pure and Applied Logic. Here's the introduction:

The objects of our analysis are proofs. We shall not ask why we prove a statement, nor how to show a statement, but how difficult it is to prove it. An answer to the third question might give insight into the second.At present, there is no notion that captures well how difficult it is to prove a theorem. Measures employed to grasp this idea are the number of steps and symbols used in a deduction, and these measures are far too rough: proofs containing no cuts/lemmas usually have a larger number of steps and symbols than proofs with cuts, but their combinatorial structure is simple, essentially a tree; on the other hand, the combinatorial structure of proofs with cuts can be quite intricate, and lemmas might be very hard to guess. Despite this, in practice, we look for lemmas in order to show a theorem.

Here we consider the genus of a proof as a measure of proof complexity and we discuss a few geometrical properties of logical flow graphs of proofs, with and without cuts, with the purpose of representing how complicated a cut-free proof can be. The main result of the article says that arbitrarily complicated non-oriented graphs, that is graphs of arbitrarily large genus, can be encoded in a cut-free proof. This fact was proved by Richard Statman in his thesis written in the early seventies and never published. Here, we reformulate Statman’s result in a purely graph theoretical language and give a proof of it. We show that there are several ways to embed non-oriented graphs of arbitrary complexity into cut-free proofs and provide some other direct embeddings of arbitrarily complex non-oriented graphs into proofs possibly with cuts. We also show that, given any formal circuit, we can codify it into a proof in such a way that the graph of the circuit corresponds to the logical flow graph of the encoding proof.

- Read more about Carbone on the Genus of Proofs
- Richard Zach's blog
- Log in to post comments

Submitted by Richard Zach on Mon, 08/03/2009 - 9:26pm

The BBC 4 radio program "In Our Time," presented by Melvyn Bragg, has archives of previous features on a range of topics, including some relevant to logic. Haven't had the time to listen to them, but it you do, let me know what you think. Might be the kind of thing you can tell your relatives to listen to when they want to know what you are interested in.

- Logical Positivism with Barry Smith, Nancy Cartwright, and Thomas Uebel (in the Philosophy archive)
- Gödel's Incompleteness Theorem with Marcus du Sautoy, John Barrow, and Philip Welch
- Infinity (with Ian Stewart, Robert Kaplan, and Sarah Rees (in the Science archive)

HT: Chris Green

Submitted by Richard Zach on Sun, 08/02/2009 - 10:21pm

Exciting developments! The Association of Symbolic Logic has made the now-out of print volumes in the Lecture Notes in Logic (vols. 1-12) and Perspectives in Mathematical Logic (vols. 1-12) open-access through Project Euclid. This includes classics like

- Shoenfield's Recursion Theory,
- Lindström's Aspects of Incompleteness in the LNL,
- Sacks' Higher Recursion Theory,
- Hájek and Pudlák's Metamathematics of First-order Arithmetic,
- Shelah's Proper and Improper Forcing,
- Barwise's Admissible Sets and Structures, and
- Barwise and Feferman's Model-theoretic Logics in the PiML.

I'm especially excited about the Hájek/Pudlák and Barwise/Feferman volumes, which are chock-full of useful material! Check out the full list of volumes available (click on the "Series Contents" link on the right side). For now it's available in nicely scanned and OCR'd PDF format, perhaps there will also be a print-on-demand way of getting a bound copy.

Submitted by Richard Zach on Thu, 07/23/2009 - 7:17pm

Catarina Dutilh Novaes' list of women in philosophical logic and philosophy of logic (see this earlier post) is now online. Updates over there, please!

Submitted by Richard Zach on Tue, 07/14/2009 - 7:49pm

For your amusement: a list of all countries with at least 5 members of the Association for Symbolic Logic, rank-ordered by number of logicians per 10,000,000 inhabitants. Bonus info: percentage of women logicians in these countries.

Country | # ASL members | % Women | per 10,000,000 |

New Zealand | 17 | 0% | 39.5 |

Switzerland | 25 | 4% | 32.5 |

Israel | 22 | 18% | 29.7 |

Norway | 13 | 0% | 27.1 |

USA | 806 | 12% | 26.3 |

Netherlands | 43 | 21% | 26.1 |

Canada | 85 | 11% | 25.2 |

Belgium | 23 | 4% | 21.5 |

Finland | 10 | 10% | 18.9 |

United Kingdom | 100 | 10% | 16.4 |

Denmark | 9 | 0% | 16.4 |

Sweden | 15 | 20% | 16.3 |

Singapore | 7 | 17% | 14.6 |

Greece | 16 | 25% | 14.3 |

Austria | 11 | 9% | 13.3 |

Croatia | 5 | 0% | 11.4 |

Germany | 87 | 8% | 10.6 |

Portugal | 9 | 33% | 8.5 |

Australia | 17 | 6% | 7.8 |

Spain | 35 | 11% | 7.6 |

Italy | 42 | 24% | 7.0 |

France | 40 | 11% | 6.2 |

Japan | 63 | 12% | 5.0 |

Czech Republic | 5 | 0% | 4.8 |

Poland | 12 | 8% | 3.1 |

Brazil | 40 | 13% | 2.1 |

Colombia | 8 | 25% | 1.8 |

Argentina | 6 | 33% | 1.5 |

South Africa | 6 | 0% | 1.2 |

Iran | 5 | 0% | 0.7 |

Russia | 8 | 25% | 0.6 |

Mexico | 5 | 20% | 0.5 |

China | 14 | 0.1 | |

India | 8 | 20% | 0.1 |

Submitted by Richard Zach on Fri, 06/26/2009 - 4:24pm

Catarina Dutilh Novaes sent the following important message to PHILOS-L last weekend, reposted here with her permission:

Dear all,Recently (and admittedly very late!), I started thinking more seriously about the lack of gender balance in the areas in which I do most of my research, namely history and philosophy of logic and philosophical logic. What got me thinking was probably the (positive) noise being made at Feminist Philosophers. One of the issues raised by the Feminist Philosophers is the low proportion of women in most philosophy conferences (in particular as invited/keynote speakers); I realized that in the workshop I am organizing, there are only three women as speakers, including myself! So I think this is a matter that deserves further attention.

Richard Zach had a blog entry a while ago on the staggeringly low number of women publishing in the journals of the area (his data concerned the Journal of Philosophical Logic). From this sort of data it is all too easy to conclude that there simply aren't enough women around working in (philosophy of) logic and philosophical logic so as to redress the imbalance seen in conference lineups. But here again the usual analysis applies: the lack of female speakers at such conferences reinforces the idea that the area is just not 'for women', which in turn does not encourage young female students to pursue interests they might have in the area. Absence of female keynote speakers may also be a discouraging factor for other female researchers to submit papers to such conferences. Sally Haslanger has a wonderful piece on how vicious these mechanisms can be, which can be found here: Changing the Ideology and Culture of Philosophy: Not by Reason (Alone)

So the purpose of this message now is to question the widespread impression that there are not (or very few) prominent female logicians and philosophers of logic, people with the standing to be keynote speakers at major conferences. I was thinking it might be useful to compile a list of such people, sort of a handy device that could help those organizing conferences in the area to ensure a better gender balance among the speakers. Please send me names off list, and I will post the results to the whole list once we have a significant number of names. Just to give you an idea of what I have in mind, here are some women that would obviously be on such a list: Juliet Floyd, Penelope Maddy, Gila Sher, Delia Graff Fara. I’m sure there are many more such talented women working in the philosophy of logic and philosophical logic, so I look forward to many reactions!Thanks!

Catarina

cdutilhnovaes at yahoo dot com

Please respond to Catarina at the email address above!

UPDATE: Results of the effort are collected "women in philosophy of logic and philosophical logic" on the Logic and Rational Interaction blog.

Submitted by Richard Zach on Wed, 06/24/2009 - 1:28am

Call for Papers

PM@100: Logic from 1910 to 1927

PM@100: Logic from 1910 to 1927

21 – 24 May, 2010

Bertrand Russell Research Centre

McMaster University

Hamilton, Ontario

Canada

The Bertrand Russell Research Centre in 2010 will host a conference to celebrate the 100th anniversary of the publication of the first volume of Russell and Whitehead’s *Principia Mathematica*.

The publication in 1910 of the first of the three volumes of Russell and Whitehead’s *Principia Mathematica* was a landmark in the development of logic, the foundations of mathematics, and the application of logic in philosophy. The rapid development of these fields in the two decades after 1910 owes perhaps more to *Principia Mathematica* than to any other work. Subsequently, however, its lessons learnt in different ways by different people, it becomes more difficult to determine exactly what the world owes to this gigantic piece of work. Daunting both for its size and its technical difficulty, the book is now known more by reputation than by detailed study. Russell himself maintained, no doubt with some exaggeration, that he knew of only six people besides the authors who had read the entire three volumes. He remained dissatisfied with the foundations of the work and attempted a major revision (this time without Whitehead’s help) in a second edition published in 1925–27, which further complicated its historical legacy.

A century after its first appearance, a great deal has changed. Many of Russell’s working papers on the problems it addressed have been published, and this has led to significant re-interpretations of the work itself. Enough time has now passed to make it possible to evaluate what contributions it made, or failed to make, to philosophy, logic, and the foundations of mathematics.

Presenters Include: Patricia Blanchette, Charles Chihara, Warren Goldfarb, Ivor Grattan-Guinness, Leila Haaparanta, Allen Hazen, David Kaplan, Gregory Landini, Peter Simons, Alasdair Urquhart, and Richard Zach.

Submissions to the conference are sought in all areas relating to *Principia Mathematica* or to the development of logic and to the philosophy and foundations of mathematics in the years between the two editions.

Contributors are asked to submit two copies of an essay suitable for 30–45 minute presentation with an abstract no later than 1 January 2010 to:

Professor Nicholas Griffin, Director

The Bertrand Russell Research Centre

1280 Main Street West

Hamilton, Ontario

CANADA L8S 4M2

EMAIL: ngriffin@mcmaster.ca

FAX: 905-577-6930

Graduate students are also encouraged to submit. Announcements of acceptances for the program will be made by the end of February 2010.

Conference Co-Organizers:

Nicholas Griffin

The Bertrand Russell Research Centre

McMaster University

ngriffin@mcmaster.ca

Bernard Linsky

Department of Philosophy

University of Alberta

bernard.linsky@ualberta. ca

- Read more about PM@100: Logic from 1910 to 1927
- Richard Zach's blog
- Log in to post comments

Submitted by Richard Zach on Fri, 06/19/2009 - 6:40pm

My website people changed something on the server and now this blog isn't displaying properly and my website is completely down. Sorry. If you want to get to my website, try www.ucalgary.ca/rzach/ instead of www.ucalgary.ca/~rzach/

- Read more about Server Problems
- Richard Zach's blog
- Log in to post comments

Submitted by Richard Zach on Tue, 05/19/2009 - 8:11am

Benson Mates, Professor emeritus of Philosophy at the University of California, died May 14. He was a logician, historian of logic, philosopher of language,epistemologist, Leibniz scholar, and author of the excellent logic textbook Elementary Logic.

- Read more about Benson Mates, 1919-2009
- Richard Zach's blog
- Log in to post comments

Submitted by Richard Zach on Sat, 05/16/2009 - 6:34am

In between thinking and lecturing about the epsilon-calculus, I'm in Paris for a few days: it's where all the Carnap action is right now. Heard wonderful talks by the likes of Steve Awodey, Dan Isaacson, Alan Richardson, Erich Reck, Delphine Chapuis-Schmitz, and Tom Uebel, unfortunately missed those by Michael Beaney, Juliet Floyd, and Rick Creath, and looking forward to some by André Carus, Gottfried Gabriel, Peter Hylton, Thomas Morman, and Pierre Wagner today. Thanks to Pierre for putting on this exciting conference!

- Read more about Carnap Action in Paris
- Richard Zach's blog
- 2 comments
- Log in to post comments

Submitted by Richard Zach on Sat, 05/09/2009 - 12:47pm

Bob Meyer, emeritus professor of logic and philosophy at ANU, died last Thursday at the age of 77. He worked mainly on relevant logics and entailment, and is remembered not just for his work in logic, but also his wit and humor.

Dave Chalmers and Greg Restall remind us of the paper "God exists!", in which Bob proved that the existence of God is equivalent to the Axiom of Choice, and the Manifesto of the Logician's Liberation League.

UPDATE: Obit from the ASL Newsletter:

Robert Kenneth (Bob) Meyer, a major contributor in the field of non-classical logics, and a central figure on the Australasian logical scene, died in Canberra on May 6, 2009 at the age of 76, after a long struggle with cancer. Before his retirement as Professor in 1998, Meyer spent more than twenty years at the Australian National University, first in Philosophy at the Research School of Social Sciences, and subsequently in the Automated Reasoning Project, of which he was a founder. Meyer was born on May 27, 1932 in Philadelphia. He received a Bachelor of Divinity at Princeton Theological Seminary in 1956. After studying Japanese in Kyoto, he served as a missionary at the Christian Institute of Industrial Relations in Osaka from 1959 to 1962. Impelled by questions about the foundations of his religious beliefs, he enrolled as a graduate student in Philosophy at the University of Pittsburgh, receiving a Ph.D. in 1966 under the supervision of Nuel Belnap. From 1965 to 1974, he taught in Philosophy departments at West Virginia University, Rice University, Bryn Mawr College, Indiana University, and the Universities of Toronto and Pittsburgh. From 1974 until his retirement in 1998, he was at the Australian National University. Meyer served as the President of the Australasian Association for Logic in 1982 and was elected as a Fellow of the Australian Academy of the Humanities in the same year. Meyer was famous for his work in relevant logic and entailment. An early major contribution in the area was his proof (with J.M. Dunn) of the admissibility of the rule $\gamma$ in the logics $R$ and $E$. His best known work in the area is his series of papers with Richard Routley, expounding the relational semantics for relevant logics, and proving completeness theorems and many other results with its aid. Bob Meyer's brilliance as a logician and his infectious enthusiasm stimulated the growth of the Australian school of logic. In the 1980s, the research group surrounding him pioneered the use of computers in investigating logical problems. This group formed the nucleus of the Automated Reasoning Project, that later morphed into the Logic and Computation Group (both at ANU). Bob was noted not only for his enormous and unquenchable enthusiasm for logic, but also for his wit and humour. From 1969 onwards, he was the Maximum Leader of the Logicians Liberation League; for the manifesto of the LLL see http://users.rsise.anu.edu.au/~rkm/manifesto.html. Remarkable also is his contribution to rational theology, "God Exists!'' (published in Noûs 21: 345-61, 1987), in which he proves that God's existence (under a certain interpretation) is equivalent to the Axiom of Choice. Bob is remembered fondly by his family and his many friends and colleagues as a remarkable logician, and a wonderful human being.

- Read more about Robert K. Meyer, 1932-2009
- Richard Zach's blog
- 3 comments
- Log in to post comments

Submitted by Richard Zach on Fri, 05/08/2009 - 6:55am

- Read more about
- Richard Zach's blog
- Log in to post comments

Submitted by Richard Zach on Tue, 05/05/2009 - 3:50am

At least I hope it does. I'll see in a couple of days, when I get there. Scheduled to give a talk on proof interpretations at the Institute Vienna Circle on Thursday (5 pm, Institut für Zeitgeschichte, Uni Wien Campus, Hof 1, 2. Stock, links). Friday, I start teaching a short course on the epsilon calculus at the TU Wien Logic Group. It'll be 10-2 in the seminar room of the department, 185/2, Favoritenstrasse 9, 3rd floor, yellow zone. Both of those will be in English, contrary to what you might think from the content of the linked pages.

- Read more about Vienna Waits For Me
- Richard Zach's blog
- 3 comments
- Log in to post comments

Submitted by Richard Zach on Wed, 04/29/2009 - 11:15pm

The May 2009 issue of the Proceedings and Addresses of the APA contain an interesting study conducted by the Committee on the Status of Women. It's online on the APA website:

Submitted by Richard Zach on Wed, 04/22/2009 - 6:42pm

SSHRC has posted the list of funded projects from the most recent Standard Research Grants competition. These grants are for three years. Last year's results are here. (Check the discussion in comments for info on what these grants are for, comparison with NEH grants, etc. UPDATE: Actually, the interesting discussion followed the 2006 list.)

This year's stats: 105 applications (2008: 92; 2007: 88; 2006: 85, 2005: 96, 2004: 92), 32 grants, for a success rate of 30% (2008: 30%; 2007: 29%; 2006: 37%, 2005: 38%, 2004: 48%). Full stats here.

Here's a list of the projects that jumped out at me as being philosophy projects or where I recognized the applicants as philosophers. So, the list is certainly incomplete! I haven't bothered sorting them alphabetically this time: they're sorted by province, east to west, then by university. The list doesn't give the department, nor does it give the grant selection committee, so some of these may have applied to a GSC other than philosophy--I don't think there's a way to tell. As always, please email with corrections and additions, or post in comments. Congratulations to all! And kudos to SSHRC for making the list of results available right away, and not with a delay of several months as in the past.

And a question: is it just my impression, or is Quebec overrepresented in philosophy SSHRC's? 42% of my list from Quebec, but only 27% of overall applications. It wasn't like this in the past few years. Maybe just coincidence? (After all, the prairies got nothing this year, it seems, but we had a pretty good showing last year.)

- Renaud, François - Université de Moncton $25,787

Cicéron platonicien : la forme du dialogue et le débat entre scepticisme et dogmatisme - Charles, Syliane - Bishop's University $44,400

Entre physique et métaphysique, l'individu chez Spinoza - Danisch, Robert C. - Concordia University $59,000

Completing the linguistic turn: neopragmatism as rhetorical theory - Smith, Justin E.H. - Concordia University $76,874

Nature, human nature, and human difference: philosophical anthropology and the problem of diversity in the new science of nature, 1500-1800 - Al-Saji, Alia - McGill University $39,957

Vision, race and ethics: a phenomenological investigation of racializing perception - Davies, David A. - McGill University $38,625

The ontology of multiple artworks: a performance-theoretic approach - Deslauriers, Marguerite L. - McGill University $80,237

Women, rationality and immortality: the reception of Plato and Aristotle in 16th and 17th C. feminist philosophy - McGilvray, James A. - McGill University $52,802

Philosophy and biolinguistics - Duchesneau, François - Université de Montréal $49,500

Monades et systèmes de la nature : Leibniz et sa postérité - Lepage, François - Université de Montréal $45,000

Les systèmes logiques de Lesniewski : une perspective contemporaine - Macdonald, Iain - Université de Montréal $35,724

Adorno and Heidegger: history and stakes of an unfinished debate - Lacroix, André - Université de Sherbrooke $71,660

Bégin, Luc - Université Laval

La formation chez les praticiens en éthique - Fisette, Denis - Université du Québec à Montréal $91,270

La philosophie de Franz Brentano via sa correspondance avec ses étudiants - Panaccio, Claude - Université du Québec à Montréal $71,540

Le nominalisme médiéval et l'externalisme : ontologie et théorie de l'esprit - Daigle, Christine - Brock University $42,873

Nietzsche as phenomenologist - Griffin, Nicholas J. - McMaster University $164,297

The collected letters of Bertrand Russell - Kumar, Rahul - Queen's University $51,300

Contractualism and the contours of morality - Russon, John E. - University of Guelph $27,445

Being through another: the idealist legacy in continental philosophy - Moggach, Douglas A. - University of Ottawa $53,832

Freedom and perfection: Kant's metaphysics of morals in context - Thompson, Evan T. - University of Toronto $41,640

The self and the brain: a neurophenomenological approach - Ripstein, Arthur S. - University of Toronto $71,050

Tort law as philosophy - Whiting, Jennifer E. - University of Toronto $58,000

Personal identity: practical yet metaphysical; or the ancient origins of Locke's account - and of any truly neo-Lockean account - of personal identity - Morrison, Margaret C. - University of Toronto $73,250

Computer simulation, modelling and experiment: knowledge at the boundaries - Mullin, Amy M. - University of Toronto $39,723

Children and parents: ethical relationships - Franks, Paul W. - University of Toronto $75,852

What is the human: Kantianism the development of the humanities and the threat of Nihilism - Nagel, Jennifer - University of Toronto $38,220

Metacognition and epistemic assessment - DeVidi, David M. - University of Waterloo $73,350

Pluralisms, mathematical and logical - Boran, Idil - York University $36,155

The idea of a market for carbon and its implications for philosophy and public policy - Shapiro, Lisa C. - Simon Fraser University $45,900

Emotions and sense perception in 17th and 18th century philosophy - Margolis, Eric - The University of British Columbia $64,250

The origins of human concepts - Aydede, Murat - The University of British Columbia $45,750

Pain and the nature of phenomenal consciousness - Woodcock, Scott - University of Victoria $46,108

Practical wisdom and naturalistic moral psychology

Submitted by Richard Zach on Mon, 04/20/2009 - 5:50pm

[On March 27, 2009, Stanford/CSLI hosted a workshop on OpenProof (aka, the software behind Barwise and Etchemendy's Language, Proof, and Logic textbook). Alexei Angelides was there and provided the following report for LogBlog.]

On March 27th, CSLI and the OpenProof Project hosted a full day of presentation and discussion commemorating the, so to speak, tenth anniversary of the publication of Language, Proof, and Logic (LPL). I say "so to speak" because although the publication date was 1999, the date that appears on the first edition is 2000, a little tidbit of information that Etchemendy revealed was intentional, as both he and Barwise wanted its publication to symbolically coincide with the new millennium. The presentations were divided into six sections. Etchemendy began the day with a description of the history of the project; David Barker-Plummer followed with a description of the LPL package, including some of the new features that are going to be added to the next edition; this was followed by a roundtable discussion with three professors currently using the LPL courseware packages; then Richard Cox, one of the principal OpenProof researchers, presented some findings from data-mining the Grade Grinder corpus; Eric Pacuit, a modal logician currently at Stanford, presented on Kripke's World, a program intended to supplement work in modal logic; and, finally, Barker-Plummer ended the day with a description of OpenProof's main current research program, namely, HyperProof and OpenBox. I'll discuss a bit of the history, and some of the new features being added to LPL in the near future, and then describe just two of the presentations a bit. More info can be found here, including slides from each talk.

In the late '80s, Jon Barwise and John Etchemendy undertook work that attempted to blend different types of reasoning, primarily diagrammatic and sentential. Their work had two main aims, one theoretical, and the other pedagogical. On the theoretical side, Etch and Barwise were interested in challenging the "hegemony" of first-order predicate logic by arguing that reasoning with diagrams could be as rigorous as reasoning with a standard formal language. To this end, they developed so-called "heterogeneous" systems, formal systems that capture the structure of sentential or predicate reasoning (as in, e.g., sentential logic), and the structure of diagrammatic and visual reasoning (as in, e.g., reasoning with maps or Venn diagrams). On the pedagogical side, they were interested in using heterogeneous systems to enhance logic education, primarily at the college level, and so began to develop software packages that acted as supplements to the textbooks. By the mid-1990's, their work led to Hyperproof (1994) , a textbook and package of programs that implemented sentential reasoning alongside diagrammatic reasoning, making it possible to reason, say, with maps (or visual information more generally), and first-order sentences in the same contexts. Along with Tarski's World's first incarnation (1987), Turing's World (1986), and their The Language of First-Order Logic (1991), Hyperproof led to the first incarnation of LPL, a book that is nominally a course in first-order logic, but for which one of the programs allows students to evaluate the truth-values of sentences and the consequence relations between them, in a fully interpreted language called the "Blocks Language," by using the spatial and visual relationships between tetrahedra, cubes, and dodecahedra in the Tarski's World program.

Tarski's World is one of three programs designed to supplement a student's learning. The other two are Boole, a program designed to allow students to construct truth tables and test for truth-functionality and first-order consequence, and Fitch, a formal system for constructing proofs that includes the ability for teachers to allow and disallow certain rules to be used, and which includes a proof checker for students to verify their constructions. Of course, the software package also includes the Grade Grinder, which is like a very programmatic, 24-hour, mini-TA for students and instructors alike, giving some feedback to students who submit incorrect answers to it, and allowing teachers to relegate the more menial, possibly non-conceptual problems to the machine. (It includes, for students, the option of submitting solely to themselves in order to check if their answers are correct before submitting to the instructor.) Now, anyone who has used LPL knows how enormously helpful these programs are, both in terms of saving time for the professor using it, and pedagogically for the student, especially Tarski's World. Understanding how to abstract away from the meanings of the terms, and regard them as entirely uninterpreted has been, in my experience, the first road block for students. Tarski's World, though, acts as a kind of happy middle between the uninterpreted languages of first-order logic, and the interpreted kind we all grow up speaking.

However, anyone who has used LPL for anything more than an intro course also knows that software support drops off at chapter fifteen, the chapter in which we are introduced to first-order set theory, and after that, mathematical induction, and some of FOL's metatheory. In his presentation, Barker-Plummer noted that new editions of LPL rectify this. So, new editions enhance Fitch by adding the possibility of constructing inductive and set-theoretic proofs, the ability to "flag" lemmas, so that students do not have to reprove instances of, say, excluded middle, improved Henkin-Hintikka game play in Tarski's World, and a feature they're calling "goggles," in which the distinctions between tautological consequence, first-order consequence, and logical consequence are given a "visual" component. Thus, for example, if you're using your TautCon Goggles, only the sentential connectives are visible, and each instance of the same sentential letter gets assigned the same color, allowing the student to visualize the underlying logical structure of the argument. (Footnote: You might worry, as one audience member did, about how this might work for the (partially) colorblind or blind. An effective way to deal with this might be to have "goggled" areas shaded with variations in grey. For the blind, the problem is more general, obviously. For some recent work dealing with it see Jesse Alama, Patrick Girard, and Elizabeth Phillips's project on "brailling logic" here.) Finally, new editions of LPL will also include an ability for instructors to input their own exercises that are then gradable via the Grade Grinder, an addition, I think, that enhances the interaction between instructor and LPL, allowing instructors a bit more freedom in what they stress in their courses.

One of the most interesting presentations of the day was Cox's. Along with a few others (including Barker-Plummer), Cox has been data mining the results of the Grade Grinder in order to find the most common mistakes, and then attempting to give some explanation to those mistakes. Not only does this have interest in itself, since it's possible that such research leads to a better understanding of some of the cognitive processes underlying logical and, in at least one case as I'll explain in a second, visual reasoning. It also assists with updates to the LPL software, since by isolating the source of common errors in problem-solving, better feedback can be automatically generated by the Grade Grinder. They looked at two different exercises, one dealing with translations from English to FOL, and one dealing with the graphical interface between Tarski's World and the Blocks Language. For the first, the team selected an exercise of mid-range difficulty by looking at the number of submissions from beginning of data from the Grade Grinder (1999), rank ordering those submissions, and then choosing one with a high error rate, which turned out to be exercise 7.12 from chapter 7. (Footnote: Specifically, of 46,200 submissions, 27,473 were incorrect (59%), taken from a sample size of 4912 students, representing 5.6 incorrect sentences (out of 20).) Consider the following sentence:

- if a is a tetrahedron, then it is in front of d.

On this problem (7.12.1), students were in error 43%. But now consider:

- c is to the right of a, provided it (i.e., c) is small.

On this problem (7.12.4), students were in error 66%, reflecting the fact that when word order between natural language and first-order languages is not preserved in translation, the error rate rises. One frequent example that logic instructors everywhere will recognize immediately is the "only if" construction in English. As LPL points out, "only if" introduces a necessary condition. Even after much instruction, however, students are apt to translate "S only if P" as:

- P ? S.

Cox and his team found that, across all twenty sentences in problem 7.12, the frequency of error in translating from "only if" to FOL was 75.43%, a far higher error rate than any other conditional translation error. While many of their results dealing with translations from natural language into FOL are unsurprising, it is nice to see some statistics backing up anecdotal experience.

On the other hand, the third error the data miners canvassed was one dealing with the interface between Tarski's World and translations from natural language to FOL, this time with an unexpected result. Again choosing a problem of medium difficulty, 7.15, they found that one subproblem in particular, 7.15.7, suggested that students have a harder time with processing visual (sizes, etc.), as opposed to spatial (shapes, etc.) information. In the problem you are asked to start a sentence file in Tarski's World, and translate:

- d is a small dodecahedron unless a is small.

Note again the intuitively problematic conditional. Once the student has translated the sentence into FOL, she is asked to figure out the sizes and shapes of the objects named in all 12 subproblems. Then, the student is asked to build a world in Tarski's World where all of the sentences are jointly true. The point is that the student is asked to translate from English to FOL, then to determine, based on her translations, the relevant visual and spatial information, and then, based on her classification of that information, actually produce the required visual and spatial arrangement. In other words, the exercise takes the student from linguistic processing to visual and spatial processing. Cox and company found that for the above sentence, 92% of errors involved the size of d. But only 24% of errors involved its shape. (16% involved both.) So, given that such a high error rate was not found in cases involving translations between English and FOL that did not also involve the graphical interface, Cox suggested, based on research by Knauff (2001), that the information about an object's size may have negative effects on reasoning when it's not relevant to the problem. (Footnote: Of course, there are other interpretations of the data here, and Cox was careful to go through a few. I found this the most interesting for the purposes of making a distinction between linguistic, visual, and spatial types of reasoning. But see his slides (on the website) for more.)

Pacuit's presentation was on another new, but currently in progress, feature of the OpenProof project. Kripke's World, which the developers hope to have ready to accompany an as of yet unwritten text, is a means of evaluating modal formulae that is, in most respects, just like Tarski's World. Salient differences are that rather than using a propositional modal language, the developers have chosen a first-order modal language over the Blocks Language. Hence, upon opening Kripke's World, one is able to form sentences such as:

- ?? x Tet(x).

The states at which modal formulae are evaluated are Blocks Worlds. The interface is essentially the same as the Tarski's World interface, the difference being that multiple Blocks Worlds are constructible where there is an accessibility relation (reflexive, symmetric, Euclidean, and so on, selected from a useful drop down scroll list) between the various Kripke's Worlds that one constructs. So, for example, if one starts in a world where an object a is a cube, then in order for:

- ?Cube(a)

to be true, the object named by a must be a cube in all Kripke Worlds accessible from the initial world, reflecting the fact that names are rigid designators. Moreover, because the developers use a first-order modal logic, in Kripke's World objects have haecceity, a fact which is reflected in the software as well, as the "thisness" (represented in Kripke's World by Greek lettering) for an object in the initial world carries over to all subsequent worlds in which the formula containing it is evaluated. One feature, or problem--depending on who's looking--of their approach is that Kripke's World seems to be a nice approach for philosophers who are trying to emphasize the philosophical aspects of modal logic. But for logicians, who commonly emphasize the metatheoretic properties of modal logics, and its relation to (fragments of) first-order logic, it might not be as useful. For example, it doesn't touch on the myriad applications of modal logic, such as epistemic or deontic logic. Moreover, in my opinion another drawback of Kripke's World is that it uses the same graphical interface as Tarski's World. The salient difference is that more than one Tarski World is constructible, given an accessibility relation, but that only seems to visually complicate matters, whereas one of the nice things about Tarski's World is that, visually, it's so easy to use. Surely there's some happy middle, here. In any event, Pacuit brought up some very nice questions about Kripke's World, including one that has received much airtime at Stanford lately, namely, how best to integrate an introduction to modal logic within a standard course on first-order logic. Suffice it to say that this discussion is ongoing.

One final note on Barker-Plummer's final presentation, on OpenProof's OpenBox project. The OpenBox, a direct descendent of Barwise and Etchemendy's theoretical work that led to Hyperproof, is due to appear soon, and, as emerged from the discussion, is the most extant and up-to-date version of the original Hyperproof platform. As such, the intention is to integrate diagrammatic and sentential reasoning into a single software package. Now, however, the architecture of the program allows users to modify programs by plugging in "components," new interfaces that are uploaded by the users themselves, making the project entirely interactive. Hence, for example, an architect who wants to plan his next project might upload his design specifications, and then use the reasoning environment given by OpenBox to find his available possibilities, given his specifications. Or, as Etchemendy pointed out, one might use it to modify a picture, for example, in Adobe Photoshop, but use Openbox to save the history of all possibilities that had been available before a given modification to the picture. Of course, more theoretical uses are available, but the point of the components is to allow users to build their own reasoning specifications into different contexts, visual, spatial, sentential, and various combinations of the three. Barker-Plummer intends this to be a generalization of the notion of justification, and to the extent that it captures the reason for which an inference is made, whether in logical, architectural, or other contexts, this is correct. Indeed, it must be emphasized that maximal interaction between interface and user, and the systematic investigation of different types of reasoning, have been theoretical goals of the OpenProof Project since its inception, for it's led to a book, that led to a software and textbook package, that led to today's LPL, that led to OpenProof. So I hope, given their stress on interaction and the commemoration's fruitfulness, that more meetings like this take place.

- Read more about Report on OpenProof Day 2009
- Richard Zach's blog
- Log in to post comments

Submitted by Richard Zach on Thu, 04/16/2009 - 2:58pm

Jake Chandler at Leuven's Centre for Logic and Analytic Philosophy, and Jonah Schupbach, currently at Tilburg's Center for Logic and Philosophy of Science, have started a new group blog, Choice & Inference:

Welcome to the new group blog, Choice & Inference! This blog provides a platform for dialogue and news within the fields of formal epistemology and decision theory, broadly construed. Topics include (but are not limited to) uncertain and ampliative inference, coherence, paradoxes of belief and / or action, belief revision, disagreement and consensus, causal discovery, epistemology of religion, etc. And the formal tools used to pursue questions within these topics include (but are not limited to) game theory and decision theory, formal learning theory, probability theory and statistics, networks and graphs, and formal logic.

- Read more about Choice & Inference: New Group Blog
- Richard Zach's blog
- Log in to post comments

- Open Logic Project
- The LogBlog is Moving!
- Academic Genealogy Graphed
- CfP: Hilbert’s Epsilon and Tau in Logic, Informatics and Linguistics
- In Memoriam: Grigori Mints
- Previously Unknown Turing Manuscript Going to Auction
- Carnap (and Goodman and Quine) and Linguistics (Guest post by Darin Flynn)
- Carnap on "Syntax" vs "Semantics"