Modal Logic! Propositional Logic! Tableaux!

Lots of new stuff in the Open Logic repository! I’m teaching modal logic this term, and my ambitious goal is to have, by the end of term or soon thereafter, another nicely organized and typeset open textbook on modal logic. The working title is Boxes and Diamonds, and you can check out what’s there so far on the builds site. This project of course required new material on modal logic.  So far this consists in revised and expanded notes by our dear late colleague Aldo Antonelli. These now live in content/normal-modal-logic and cover relational models for normal modal logics, frame correspondence, derivations, canonical models, and filtrations. So that’s one big exciting addition. Since the OLP didn’t cover propositional logic separately, I just now added that part as well so I can include it as review chapters. There’s a short chapter on truth-value semantics in propositional-logic/syntax-and-semantics. However, all the proof systems and completeness for them are covered as well. I didn’t write anything new for those, but rather made the respective sections for first-order logic flexible. OLP now has an FOL “tag”: if FOL is set to true, and you compile the chapter on the sequent calculus, say, you get the full first-order version with soundness proved relative to first-order structures. If FOL is set to false, the rules for the quantifiers and identity are omitted, and soundness is proved relative to propositional valuations. The same goes for the completeness theorem: with FOL set to false, it leaves out the Henkin construction and constructs a valuation from a complete consistent set rather than a term model from a saturated complete consistent set. This works fine if you need only one or the other; if you want both, you’ll currently get a lot of repetition. I hope to add code so that you can first compile without FOL then with, and the second pass will refer to the text produced by the first pass rather than do everything from scratch. You can compare the two versions in the complete PDF. Proofs systems for modal logics are tricky; and many systems don’t have nice, say, natural deduction systems. The tableau method, however, works very nicely and uniformly. The OLP didn’t have a chapter on tableaux, so this motivated me to add that as well. Tableaux are also often covered in intro logic courses (often called “truth trees”), so having them as a proof system included has the added advantage of tying in better with introductory logic material. I opted for prefixed tableaux (true and false are explicitly labelled, rather than implicit in negated and unnegated formulas), since that lends itself more easily to a comparison with the sequent calculus, but also because it extends directly to many-valued logics. The material on tableaux lives in first-order-logic/tableaux. Thanks to Clea Rees for the the prooftrees package, which made it much easier to typeset the tableaux, and to Alex Kocurek for his tips on doing modal diagrams in Tikz.

Making an Accessible Open Logic Textbook (for Dyslexics)

In the design and layout of the Open Logic Project texts as well as the Calgary Remix of the intro text forall x, we’ve tried to follow the recommendations of the BC Open Textbook Accessibility Toolkit already. Content is organized into sections, important concepts are highlighted (e.g., colored boxes around definitions and theorems), chapters have summaries, etc. We picked an easily readable typeface and set line and page lengths to enhance readability according to best (text)book design practices and research. We’ve started experimenting specifically with a version of forall x that is better for dyslexic readers (see issue 22). Readability for dyslexics is affected by typeface, type size, letter and line spacing. Charles Bigelow gives a good overview of the literature here. Some typefaces are better for dyslexic readers than others. Generally, sans-serif fonts are preferable, but individual letter design is also relevant. The British Dyslexia Association has a page on it: the design of letters should make it easy to distinguish letters, not just when they are close in shape (e.g., numeral 1, uppercase I and lowercase l; numeral 0, uppercase O and lowercase o, lowercase a) but also when they are upside-down or mirror images (e.g., p and q, b and d; M and W). In one study of reading times and reported preference, sans-serif fonts Arial, Helvetica, and Verdana ranked better than other fonts such as Myriad, Courier, Times, and Garamond, and even the specially designed Open Dyslexic typeface. Although it would be possible to get LaTeX to output in any available typefaces, it’s perhaps easiest to stick to those that come in the standard LaTeX distributions. The typeface that strikes me as best from the readability perspective seems to me to be Go Sans. It was designed by Bigelow & Holmes with readability in mind and does distinguish nicely between p and q; b and d; I, l, and 1, etc. Other things that improve readability:
  • larger type size
  • shorter lines
  • increased line spacing
  • increased character spacing, i.e., “tracking” (although see Bigelow’s post for conflicting evidence)
  • avoid ALL CAPS and italics
  • avoid word hyphenation and right justified margins
  • avoid centered text
The accessible version of forall x does all these things: Type size is set to 12 pt (not optimal on paper, but since this PDF would mainly be read on a screen, it looks large enough). Lines are shorter (about 40 instead of 65 characters per line). Line spacing is set at 1.4 line heights. Tracking is increased slightly, and ligatures (ff, fi, ffi) are disabled. Emphasis and defined terms are set in boldface instead of italics and small caps. Lines are set flush left/ragged right and words not hyphenated. The centered part headings are now also set flush left. The changes did break some of the page layout, especially in the quick reference, which still has to be fixed. There is also some content review to do. In “Mhy Bib I Fail Logic? Dyslexia in the Teaching of Logic,” Xóchitl Martínez Nava suggests avoiding symbols that are easily confused (i.e., don’t use ∧ and ∨), avoid formulas that mix letters and symbols that are easily confused (e.g., A and ∀, E and ∃), and avoid letters in the same example that are easily confused (p, q). She also recommends to introduce Polish notation in addition to infix notation, which would not be a bad idea anyway. Polish notation, I’m told, would also be much better for blind students who rely on screen readers or Braille displays. (The entire article is worth reading; h/t to Shen-yi Liao.) Feedback and comments welcome, especially if you’re dyslexic! There’s a lot more to be done, of course, especially to make the PDFs accessible to the vision-impaired. LaTeX and PDF are very good at producing visually nice output, but not good at producing output that is suitable for screen readers, for instance. OLP issue 82 is there to remind me to get OLP output that verifies as PDF/A compliant, which means in particular that the output PDF will have ASCII alternatives to all formulas, so that a screen reader can read them aloud. Even better would be a good way to convert the whole thing to HTML/MathML (forall x issue 23). forallxyyc-accessible

Logic Courseware?

Kit Fine asked me for suggestions of online logic materials that have some interactive component, i.e., ways for students to build truth-tables, evaluate arguments, translate sentences, build models, and do derivations; ideally it would not just provide feedback to the student but also grade problems and tests. There is of course Barwise & Etchemendy’s Language, Proof, and Logic, which comes with software to do these things very well and also has a grading service. But are there things that are free, preferably online, preferably open source?

  • UPDATE: Carnap is an open source framework for writing webapps for teaching logic written by Graham Leach-Krouse and Jake Ehrlich. It comes with a (free, but not openly licensed) online book, and currently can check truth tables, translations, and Kalish-Montague derivations (and they are working on first-order models). can check truth tables, symbolizations/translations, models/interpretations, and proofs in a variety of natural deduction proof systems. You can use it with the textbook you know and love; see here (Update 2020). Students can have accounts and submit exercises. The software is written in Haskell and is open-source (see Github). It’s used at Kansas Sate and the University of Birmingham.
    [Free software Free book Online Open source ]
  • First we have David Kaplan’s Logic 2010. It’s written in Java, runs on Windows and Mac, is free but not open source, and has a free online grading component. It goes with Terry Parson’s An Exposition of Symbolic Logic, which is also free. To use the software and grading service, you’d have to make arrangements with David. The text does propositional and first-order logic including models and Kalish-Montague derivations. I haven’t tried the software, but it’s used in a number of places.
    [Free software Free book Online ✗ Open source ✗]
  • Kevin Klement is teaching logic from the (free) book by Hardegree, Symbolic Logic: A First Course. (There’s a newer version that doesn’t seem to be freely available.) He has an online component (exercises and practice exams) with multiple-choice questions, truth tables, translations, and Fitch-style derivations. I’m not sure if the backend code for all of this is available and could be adapted to your own needs. He has provided a version of the proof checker that works with the Cambridge and Calgary versions of forall x, and that code is open source, however. I’m not sure if it’s possible to add the functionality he has on the UMass site for saving student work. Neither the book nor the online exercises cover models for first-order logic.
    [Free software ✓ Free book ✓ Online ✓ Open source ?]
  • The Logic Daemon by Colin Allen and Chris Menzel accompanies Allen and Michael Hand’s Logic Primer. It can check truth-tables, models, and Suppes-Lemmon derivations, and generate quizzes. The interface is basic but the functionality is extensive. There doesn’t seem to be a grading option, however. Software seems to be written in Perl, I didn’t see the source code available.
    [Free software ✓ Free book ✗ Online ✓ Open source ✗]
  • Then there is Ray Jennings and Nicole Friedrich’s Project Ara, which includes Simon, a logic tutor, and Simon Says, a grading program. The textbook is Proof and Consequence, published by Broadview (ie, not free). It does truth-tables, translations, and Suppes-style derivations, and also no models. It requires installing software on your own computer, but it’s free and runs on Windows, Mac, and Linux. The software is free but not open source. I haven’t tried it out. (That website though!)
    [Free software ✓ Free book ✗ Online ✗ Open source ✗]
  • Wilfried Sieg’s group has developed AProS, which includes proof and counterexample construction tools. I don’t think these are openly available, however. It’s used in Logic & Proofs, offered through CMU’s Open Learning Initiative. According to the description, it’s available both as a self-paced course and for other academic institutions to use for a self-paced format or for a traditional course with computer support. Not sure what the conditions are, whether it’s free or not, and have inspected neither the texts nor tried out the software.
    [Free software ? Free book ? Online ✗ Open source ✗]

Do you know of anything else that could be used to teach a course with an online or electronic component? Any experience with the options above?

Graphing Survey Responses

As I reported last year, we’ve been running surveys in our classes that use open logic textbooks. We now have another year of data, and I’ve figured out R well enough to plot the results. Perhaps someone else is in a similar situation, so I’ve written down all the steps. Results aren’t perfect yet. All the data and code is on Github, and any new discoveries I make will be updated there.

What follows is the content of the HOWTO:

As part of two Taylor Institute Teaching & Learning Grants, we developed course materials for use in Calgary’s Logic I and Logic II courses. In the case of Logic I, we also experimented with partially flipping the course. One of the requirements of the grants was to evaluate the effectiveness of the materials and interventions. To evaluate the textbooks, we ran a survey in the courses using the textbooks, and in a number of other courses that used commercial textbooks. These surveys were administered through SurveyMonkey. To evaluate the teaching interventions, we designed a special course evaluation instrument that included a number of general questions with Likert responses. The evaluation was done on paper, and the responses to the Likert questions were entered into a spreadsheet.

In order to generate nice plots of the results, we use R. This documents the steps taken to do this.

Installing R, RStudio, and likert

We’re running RStudio, a free GUI frontend to R. In order to install R on Ubuntu Linux, we followed the instructions here, updated for zesty:

  • Start “Software & Updates”, select add a source, enter the line
    http://cran.rstudio.com/bin/linux/ubuntu zesty/
    

    Then in the command line:

    $ sudo apt-get install r-base r-base-dev
    
  • We then installed RStudio using the package provided here. The R packages for analyzing Likert data and plotting them require devtools, which we installed following the instructions here:
    $ sudo apt-get install build-essential libcurl4-gnutls-dev libxml2-dev libssl-dev
    $ R
    > install.packages('devtools')
    
  • Now you can install the likert package from Github:
    > install_github('likert', 'jbryer')

Preparing the data

The source data comes in CSV files, teachingevals.csv for the teaching evaluation responses, and textbooksurvey.csv for the textbook survey responses.

Since we entered the teaching evaluation responses manually, it was relatively simple to provide them in a format usable by R. Columns are Respondent ID for a unique identifier, Gender (M for male, F for female, O for other), Major, Year, Q1 through Q9 for the nine Likert questions. For each question, a response of one of Strongly Agree, Agree, Neutral, Disagree, or Strongly Disagree is recorded.

For the textbook survey we collected a whole lot of responses more, and the data SurveyMonkey provided came in a format not directly usable by R. We converted it to a more suitable format by hand.

  • SurveyMonkey results have two header lines, the first being the question, the second being the possible responses in multiple-response questions. We have to delete the second line. For instance, a question may have five different possible responses, which correspond to five columns. If a box was checked, the corresponding cell in a response will contain the answer text, otherwise it will be empty. In single-choice and Likert responses, SurveyMonkey reports the text of the chosen answer. For analysis, we wanted a simple 1 for checked and 0 for unchecked, and a number from 1 to 5 for the Likert answers. This was done easily enough with some formulas and search-and-replacing.
  • Since the question texts in the SurveyMonkey spreadsheet don’t make for good labels for importing from CSV, we replaced them all by generic labels such as Q5 (or Q6R2, for Question 6, Response 2, for multiple-choice questions).
  • We deleted data columns we don’t need such as timestamps and empty colums for data we didn’t collect such as names and IP addresses.
  • We added columns so we can collate data more easily: Section to identify the individual course the data is from, Course for which course it is (PHIL279 for Logic I, PHIL379 for Logic II), Term for Fall or Winter term, Open to distinguish responses from sections using an open or a commercial text, and Text for the textbook used. Text is one of SLC (for Sets, Logic, Computation, BBJ (for Boolos, Burgess, and Jeffrey, Computability and Logic), ForallX (for forall x: Calgary Remix, Chellas (for Chellas, Elementary Formal Logic), or Goldfarb (for Goldfarb, Deductive Logic). This was done by combining multiple individual spreadsheets provided by SurveyMonkey into one. (One spreadsheet contained responses from three different “Email Collectors”, one for each section surveyed.) Q27GPA contains the answer to Question 27, “What grade do you expect to get?”, converted to a 4-point grade scale.
  • Question 23, “Is the price of the textbook too high for the amount of learning support it provides?”, had the same answer scale as other questions (“Not at all” to “Very much so”), but the “Not at all” is now the positive answer, and “Very much so” the negative answer. To make it easier to produce a graph in line with the others, I added a Q23Rev column, where the values are reversed (i.e., Q23Rev = 6 – Q23).
  • Q26 is the 4-letter code of the major reported in the multiple-choice question 26, and Q26R1 to Q26R8 are responses to the checkboxes corresponding to options “Mathematics”, “Computer Science”, “Physics”, “Philosophy”, “Engineering”, “Neuroscience”, “Other”, and the write-in answer for Other. These responses don’t correspond to the questions asked: we offered “Lingustics” as an answer but noone selected it. A number of “Other” respondents indicated a Neuroscience major. So Q26R6 is NEUR in Q26. Question 26 allowed multiple answers, Q26 is the first answer only.

Loading data into R

In order to analyze the Likert data, we have to tell R which cells contain what, set the levels in the right order, and rename the columns so they are labelled with the question text instead of the generic Q1 etc. We’ll begin with the teaching evaluation data. The code is in teachingevals.R. Open that file in RStudio. You can run individual lines from that file, or selections, by highlighting the commands you want to run and then clicking on the “run” button.

First we load the required packages. likert is needed for all the Likert stuff; plyr just so we have the rename function used later; and reshape2 for the melt function.

require(likert)
require(plyr)
library(reshape2)

Loading the data from a CSV value file is easy:

data <- read.csv("teachingeval.csv",
                na.string="")

Now the table data contains everything in our CSV file, with empty cells having the NA value rather than an empty string. We want the responses to be labelled by the text of the question rather than just Q1 etc.

data <- rename(data, c(
  Q1 = "In-class work in groups has improved my understanding of the material", 
  Q2 = "Collaborative work with fellow students has made the class more enjoyable", 
  Q3 = "Being able to watch screen casts ahead of time has helped me prepare for class", 
  Q4 = "Having lecture slides available electronically is helpful", 
  Q5 = "I learned best when I watched a screencast ahead of material covered in class", 
  Q6 = "I learned best when I simply followed lectures without a screencast before", 
  Q7 = "I learned best studying material on my own in the textbook", 
  Q8 = "This course made me more likely to take another logic course", 
  Q9 = "This course made me more likely to take another philosophy course"))

The Likert responses are in colums 5-13, so let’s make a table with just those:

responses <- data[c(5:13)]

The responses table still contains just the answer strings; we want to tell R that these are levels, and have the labels in the right order (“Strongly Disagree” = 1, etc.)

mylevels <- c('Strongly Disagree', 'Disagree', 'Neutral', 'Agree', 'Strongly Agree')

for(i in seq_along(responses)) {
  responses[,i] <- factor(responses[,i], levels=mylevels)
}

Analyzing and Plotting

Now we can analyze the likert data.

lresponses <- likert(responses)

You can print the analyzed Likert data:

> lresponses
  Item
1          In-class work in groups has improved my understanding of the material
2      Collaborative work with fellow students has made the class more enjoyable
3 Being able to watch screen casts ahead of time has helped me prepare for class
4                      Having lecture slides available electronically is helpful
5  I learned best when I watched a screencast ahead of material covered in class
6     I learned best when I simply followed lectures without a screencast before
7                     I learned best studying material on my own in the textbook
8                   This course made me more likely to take another logic course
9              This course made me more likely to take another philosophy course
  Strongly Disagree  Disagree   Neutral    Agree Strongly Agree
1          1.785714  5.357143 10.714286 37.50000      44.642857
2          1.785714  0.000000 10.714286 37.50000      50.000000
3          8.928571 14.285714 26.785714 28.57143      21.428571
4          1.785714  1.785714  5.357143 37.50000      53.571429
5          7.142857 10.714286 37.500000 33.92857      10.714286
6          3.571429 19.642857 51.785714 21.42857       3.571429
7          3.571429 12.500000 23.214286 33.92857      26.785714
8         20.000000 10.909091 32.727273 27.27273       9.090909
9         16.363636 18.181818 38.181818 18.18182       9.090909

And now we plot it:

plot(lresponses,
  ordered=FALSE,
  group.order=names(responses),
  colors=c('darkred','darkorange','palegoldenrod','greenyellow','darkgreen')) +
  ggtitle("Teaching Evaluations")

The group.order=names(responses) makes the lines of the plot sorted in the order of the questions, you need ordered=FALSE or else it’ll be ordered alphabetically. Leave those out and you get it sorted by level of agreement. You can of course change the colors to suit.

In textbooksurvey.R we do much of the same stuff, except for the results of the textbook survey. Some sample differences:

Here’s how to group charts for multiple questions by textbook used:

lUseByText <- likert(items=survey[,27:31,drop=FALSE],
                 grouping=survey$Text)
plot(lUseByText, 
  ordered=TRUE,
  group.order=c('SLC','BBJ','ForallX','Chellas','Goldfarb'),
  colors=c('darkred', 'darkorange', 'palegoldenrod','greenyellow','darkgreen')
  ) + 
  ggtitle("Textbook Use Patterns")

To plot a bar chart for a scaled question, but without centering the bars, use centered=FALSE:

lQ5byText <- likert(items=survey[,26,drop=FALSE],
                   grouping=survey$Text)
plot(lQ5byText, 
  ordered=TRUE,
  centered= FALSE,
  group.order=c('SLC','BBJ','ForallX','Chellas','Goldfarb'),
  colors=c('darkred','darkorange', 'gold', 'palegoldenrod','greenyellow','darkgreen')
  ) +
  ggtitle("Textbook Use Frequency")

Plotting Bar Charts for Multiple-Answer Questions

Some of the questions in the textbook survey allowed students to check multiple answers. We want those plotted with a simple bar chart, grouped by, say, the textbook used. To do this, we first have to the data for that. First, we extract the responses into a new table.

Q1 <- survey[,c(6,7:13)]

Now Q1 is just the column Text and Q1R1 through Q1R7. Next, we sum the answers (a checkmark is a 1, unchecked is 0, so number of mentions is the sum).

Q1 <- ddply(Q1,.(Text),numcolwise(sum))

Next, we convert this to “long form”:

Q1 <- melt(sumQ1,id.var="Text")

Now Q1 has three columns: Text, variable, and value. Now we can plot it:

ggplot() + 
  geom_bar(
    aes(x=Text,fill=variable,y=value),
    data=Q1,
    stat="identity") + 
  coord_flip() +
  ggtitle("01. How do you access the textbook?") +
  theme(legend.position = "bottom",
        axis.title.x = element_blank()) +
  guides(fill=guide_legend(title=NULL,ncol=1))

This makes a bar chart with Text on the x-axis, stacking variable, and using values for the value of each bar. stat="identity" means to just use value and not count. coord_flip() makes it into a horizontal chart. ggtitle(...) adds a title, theme(...) puts the legend on the bottom and removes the x axis label, and guides(...) formats the legend in one column.

UPDATE: Better Visualization of Multiple-Answer Responses

I figured out a better way to visualize multiple-answer responses (thanks to Norbert Preining for the help!). You don’t want the number of respondents which checked a box, but the percentage of all respondents (in a category) who did, so instead of adding up a column you compute the mean for it. Also, aggregate is an easier way to do this, and it doesn’t make sense to stack the responses, so I’m going to graph them side-by-side.

Here’s the code:

# load responses for question 4 into df Q4
Q4 <- survey[,c(6,20:25)]

# aggregate by Text, computing means = percent respondents who checked box
Q4 <- aggregate( . ~ Text, data=Q4, mean)

# make table long form for ggplot
Q4 <- melt(Q4,id.var="Text")

ggplot() + 
  geom_bar(
    aes(x=variable,fill=Text,y=value),
    data=Q4,
    stat="identity", position="dodge") + 
  coord_flip() +
  ggtitle("04. When using the text in electronic form, do you....") +
  theme(legend.position = "bottom",
        axis.title.x = element_blank()) +
  guides(fill=guide_legend(title=NULL,ncol=1)) +
  scale_fill_brewer(palette="Dark2") +
  scale_y_continuous(labels = scales::percent)

Illuminated Manuscript of Aristotle, Averroes, and Ramon Llull Charging the Tower of Falsehood

Jonathan Greig (LMU Munich) posted the picture above to Twitter the other day, crediting Laura Castelli with finding it. It’s from a 14th Century illuminated manuscript by Thomas Le Myésier, Breviculum ex artibus Raimundi Lulli electum, and depicts Aristotle, Averroes, and Ramon Llull leading an army charging the Tower of Falsehood. I put a full resolution version here. It’s really amazing.

Here’s the (Google translated, too lazy to thoroughly revise, maybe I’ll get back to it if anyone needs me to) description from the university library at the University of Freiburg  (complete German original):

Miniature VI shows the army of Aristotle, which is advancing to destroy the tower of untruth, together with the commentator of Aristotle, Averroes (Exercitus Aristotillis ad destruendum turrim falsitatis cum suo commentatore). The tower of untruth is occupied by the messengers of untruth: left wickedness, inactivity, ignorance, weakness, confusion, fall, futility, nothingness; Right smallness, impossibility, hatred, untruth, punishment, contrast, emptiness, inflexibility, abundance, diminution (malitia, cessatio, ignorantia, debilitas, confusio, casus, frustra, nihil and parvitas, impossibilitas, odiositas, falsitas, poena, contrarietas, vacuum, difformitas, superfluum, diminutum). To the left of the tower, at the vanguard, the goal is stated: to take down the tower by destruction or distinction (Per interemptionem aut per distinctionem oportet dissolvere turrim). The shield affirms credible reasoning, the text above above the archer, excellent proof (Probabiliter arguo, Potissime demonstro).  The horse of Aristotle is rational reasoning (ratiocinatio), his lance represents “instruments abundunt in syllogisms”, the banner mentions the methods: consideration of the similar, exploring differences, use of proposition, distinction of diversity (consideratio similitudinum, inventio differentiarum , Sumptio propositionum, multiplicis distinctio). In the chariot, the five predicates or general statements of logic are found in the front: general genus, special kind, universal difference, peculiarity, accidental property (genus generalissimum, species specialissima, differentia generalis, proprietas, accidens). Behind this are the ten categories of ontology, ten simple principles of things (Decem rerum principia incomplexa). The text beside the lance of substance specifies “by itself, originally, first, by virtue of itself: per se, principaliter, primo, propter se subsistens.” The rest of the categories are characterized summarily on the banner by the fact that they are not in themselves, but are the substance in itself (Non sumus propter nos, sed ut sit substantia, see Ideo, quia ab ea dependemus, sibimet inhaeremus).

The following banner is carried by Averros riding on his horse, which represents the imagination (imaginatio). The principles of his philosophy of nature are listed on the banner: purpose, effect, form, material, deficiency (finis, efficiens, forma, materia, privatio). The three texts next to his lance read: To be perfect in speculation and to train in them is the highest happiness (Esse perfectum in speculativis and in ice exerceri summa est felicitas); The faith of the heretic Averroes is in every law (Fides Averrois haeretici in omni lege); The next to the lance of the first warrior it reads: body in its quantity, movement, time, external appearance, place, natural observation (Corpus quantum, motus, tempus, superficies , Locus, consideratio naturalis), next to that of the second, the Aristotelian saying (according to Metaphysics, 993b): just as the eye of the night owl is to sunlight, our intellect is related to what is evident in its nature. The Pope with a cross in his hands and the abbreviated “Te Deum” text, a bishop with a prayer (Deus misereatur nostri et benedicat nobis) and below a cardinal, restraining Averroes, with the texts: “Because the phenomena can not exceed the physical nature, your intellect is obscured for what is recognizable in the purely spiritual, Averroes! So that you do not lead us into temptation, we will curb your course, for it is a sacred duty that, when one must be elected among several friends, the truth is preferable.” The banner reads,”Socrates is a friend, but truth is more a friend” (Socrates amicus, sed magis amica veritas). In the lecture of the cardinal, which follows below, this is further elaborated by referring to the limits of Averroistic philosophy and the spiritual power of the Church with the pope, episcopate, clergy, religious and theologians. He concludes with the sentence: “Nevertheless, in physical and metaphysical truths, they allow you to advance on the tower of untruth, to destroy it together with others who wish to free truth from the dungeon of untruth with the help of God.”

The text at the bottom left of the page is a lamentation of the truth: “In the dungeon of this tower, truth was incarcerated against its nature, and it languishes to be free from all the world and cry, crying and crying horribly:” Have mercy, have mercy With me, at least you, my friends! The hand of ignorance touched me, and in my place the unreliable opinion was crowned in public; I, on the other hand, which I fear from every angle, is entirely hidden from my will in the darkness and without light in the depths of the dungeon. Sad, deserted and almost desperate I die! There is no one to help me or give me comfort. On the contrary, many are more inclined to support the wrong opinion than to free me from the dungeon. All your philosophers, apart from God, I place all my trust in you, because you are true lovers of wisdom and truth, come to my aid, I beg you; Otherwise I must perish by inaction. Oh, Christian lords, how can you bear to be so oppressed by Jews and Saracens that I should fall from the top of the tower, which I should even pass, into the dungeon of this tower of untruth? ”

The miniature VII shows the approaching substitute army of Raimundus for the destruction of the tower of untruth and ignorance (Retrobellum et succursus exercitus domini Raimundi Lul de Maioricis ad corruendum turrim falsitatis et ignorantiae). The three trumpeters symbolize the three forces of the rational soul: recognizing, loving, honoring, referring to God, to the triads, to the Creator and the Savior, each in a permutating order (Deum cognoscamus, diligamus, recolamus, Unum Deum trinum diligamus, recolamus, Cognoscamus, Creatorum nostrum recolamus, cognoscamus, diligamus, nostrum redemptorem). Beside the trumpets are the three soul-forces: reason, memory of the will (intellectus, voluntas, memoria). The addition of another hand in the lower left shows that only one horse is represented here (Deberet esse unus equus tantum). An example of how Thomas Le Myésier inspected the finished images and corrected them in this case.

Lull’s horse bears the name of the right or good intent (recta intentio). The motto next to his lance reads: “He who wants to recognize the spiritual must pass over the senses and the imagination, and often himself” (Intelligent spiritualia oportet sensus et imaginationem transcendere et multotiens seipsum). On the banner, “we love God through the first intention and the greater goal” (Per primam intentionem et miioritatem finis Deum diligimus, Per secundam intentionem et minoritatem finis meritum spectamus). The eighteen principles of the Lullian Ars are recorded in the car: the nine absolute principles: goodness, greatness, duration, power, wisdom, will, virtue, truth, glory, bonitas, magnitudo, duratio, potestas, sapientia, voluntas, virtus, veritas, gloria).

To the absolute follow the nine relative principles: difference, agreement, opposition, beginning, middle, goal, greaterness, equality, minority (differentia, concordantia, contrarietas, principium, medium, finis, maioritas, aequalitas, minoritas); In the latter three the inscriptions and lances are missing. The fire column between the two groups, in reference to Exodus 13: 20-22, could symbolize the presence of God in the battle. The commentary text under the figure is: “Raimundus rides on the horse” good intention “(recta intentio) and follows the cross and the holy Catholic faith.) He sends three trumpeters ahead: the three forces of the reasoning elegans And the Son of God, Jesus Christ, who was crucified, who sought to recognize, love, glorify, and glorify God through His Ars For it is much appreciated by him, lovable, venerable, and worthy of gratitude, which must be our basic intention, a true intention, in contrast to that of Averroes, who did not know the truth, Not because he has disapproved of it as much as he can, but denies eternal life, asserts that the happiness is in the observation that it is perfect in the speculative sciences. He does not turn to the inner activity of God; As well as not of his creative outward activity, not taking care of the fact that every activity is directed towards the goal and the perfection. Neither did he care to recognize the nature of divine dignities or their activities, neither their unity, nor their personal distinction of activity, without which God would forever remain inactive in himself, and without any dignity. Consequently, in his whole nature he would be imperfect and ultimately unworthy to be God. But he himself has revealed himself as the most perfect, simple, uniquely, and purest act recognizing himself; But without one who knows, one can recognize one who is recognizable and the act of cognition, namely, the cognition itself, which can not be recognized by the one who recognizes eternally. Through this activity, we recognize necessarily the personal trinity as a unity in essence. Through their external activity, we recognize the creation of the world and the order of their parts, which God did not create infinite wisdom for no purpose and without goal, but arranged for the greater attainment of the goal. For God and nature do nothing in vain, as even the ancient philosophers and their first confess.”

New in Print: forall x (Summer 2017 edition), and Incompleteness and Computability

New on Amazon: the print version of the Summer 2017 edition of forall x: Calgary Remix, as well as the text I made for Phil 479 (Logic III) last term, Incompleteness and Computability. The new edition of forall x includes a number of corrections submitted by Richard Lawrence, who taught from it at Berkeley in the Spring term. I’ve also noticed that if you don’t want Amazon to distribute the book to libraries and bookstores, you can make it a lot cheaper: USD 7.62 instead of USD 11.35.  Of course, the PDF is still free. (There’s now also a version for printing on letter-sized paper.) With Richard’s and Aaron’s help, the solutions manual now matches the text and has fewer errors.

Links to Amazon: US UK Canada Germany

The print version of Incompleteness and Computability incorporates a number of corrections and improvements suggested by my Logic III students. Compared to the version announced earlier, it also includes the two new chapters on Models of Arithmetic and on Second-order Logic. It, too, is still available free in both PDF and source code.

Links to Amazon: US UK Canada Germany

Aldo Antonelli’s last paper

Aldo Antonelli’s last paper, “Completeness and Decidability of General First-Order Logic (with a Detour Through the Guarded Fragment)” is now out in the most recent issue of the Journal of Philosophical Logic.

This paper investigates the “general” semantics for first-order logic introduced to Antonelli (Review of Symbolic Logic 6(4), 637–58, 2013): a sound and complete axiom system is given, and the satisfiability problem for the general semantics is reduced to the satisfiability of formulas in the Guarded Fragment of Andréka et al. (Journal of Philosophical Logic 27(3):217–274, 1998), thereby showing the former decidable. A truth-tree method is presented in the Appendix.

It is published together with a note on it by Hajnal Andréka, Johan van Benthem, and István Németi in the same issue.

Association for Symbolic Logic at the Pacific APA

The ASL Spring Meeting will take place on Wednesday and Thursday at the Pacific APA in Seattle! Note that the ASL Reception will take place on Thursday, April 13, 5:00–7:00 p.m. There will be snacks and wine!

Here’s the program:

WEDNESDAY MORNING, APRIL 12, 9:00 A.M.–12:00 P.M.

Invited Speaker Session: MODALITY AND MODAL LOGIC
Chair: Audrey Yap

Peter Fritz (Universitetet i Oslo), A philosophical perspective on algebraic models for modal logics.

Fenrong Liu (Tsinghua University), Social epistemic logic.

Tamar Lando (Columbia University), Topology and measure in logics for point-free spaces.

WEDNESDAY AFTERNOON, APRIL 12, 1:00–4:00 P.M.

Invited Speaker Session: INTUITONISTIC MATHEMATICS AND LOGIC
Chair: Valeria de Paiva

Mark van Atten (Centre National de la Recherche Scientifique and Université Paris 4), Intuitionism and impredicativity.

Rosalie Iemhoff (Universiteit Utrecht), Quantifiers and functions in intuitionistic logic.

Joan Rand Moschovakis (Occidental College), Realizable extensions of Brouwer’s analysis.

THURSDAY MORNING, APRIL 13, 9:00 A.M.–12:00 P.M.

CONTRIBUTED TALKS
Chair: Richard Zach

Joachim Mueller-Theys, Defining and simplifying the second incompleteness theorem.

Valeria de Paiva and Harley Eades III, Dialectica categories for the Lambek calculus.

Ronald Fuller, First-order logic in 13th-century accounting systems.

Rachel Boddy (University of California, Davis), Fruitful definitions.

Michael McGrady, Garbage collection (GC), Gödel numbering, and periodicity in mathematical logic.

Fabio Lampert (University of California, Davis), On the expressive power of propositional two-dimensional modal logic.

Alexei Angelides (University of San Francisco), Weak arithmetics and the bar rule.

THURSDAY AFTERNOON, APRIL 13, 1:00 P.M.–4:00 P.M.

Special Session organized by the Committee on Logic Education: INCLUSIVENESS IN LOGIC EDUCATION
Chair: Alexei Angelides

Audrey Yap (University of Victoria), Symbolic logic, accessibility, and accommodation.

Fenrong Liu (Tsinghua University), Experiences and difficulties in teaching logic at Tsinghua University.

Nicole Wyatt (University of Calgary), The Open Logic Textbook.

Maureen Eckert (University of Massachussetts, Dartmouth), The Summer Program for Diversity in Logic: Some reflections.

Panel discusssion.

THURSDAY EARLY EVENING, APRIL 13, 5:00 P.M.–7:00 P.M.
ASL Reception

CfP: Quantifiers and Determiners (part of ESSLI 2017)

QUAD: QUantifiers And Determiners

http://www.lirmm.fr/quad

Toulouse, Monday  July 17 — Friday July 21:  17:00-18:30

ESSLLI 2017 workshop

Schedule:

deadline for submissions:  17 March 2017
submission website: https://easychair.org/conferences/?conf=quad2017
notification to authors:  15 April 2017
final version due: 19 May 2017
conference: 17-21 July 2017

Presentation:

The compositional interpretation of determiners relies on quantifiers  — in a general acceptation of this later term which includes generalised quantifiers, generics, definite descriptions i.e. any operation that applies to one or several formulas with a free variable, binds it  and yields a formula or possibly a generic term  (the operator is then called a subnector, following Curry). There is a long history of quantification in the Ancient and Medieval times at the border between logic and philosophy of language, before the proper formalisation of quantification by Frege.

A common solution for natural language semantics is the so-called theory of generalised quantifiers. Quantifiers like « some, exactly two, at most three, the majority of, most of, few, many, … » are all described in terms of functions of two predicates viewed as subsets.

Nevertheless, many mathematical and linguistic questions remain open.

On the mathematical side, little is known about generalised , generalised and vague quantifiers, in particular about their proof theory. On the other hand, even for standard quantifiers, indefinites and definite descriptions, there exist alternative formulations with choice functions and generics or subnectors (Russell’s iota, Hilbert-Bernays, eta, epsilon, tau). The computational aspects of these logical frameworks are also worth studying, both for computational linguistic software and for the modelling of the cognitive processes involved in understanding or producing sentences involving quantifiers.

On the linguistic side, the relation between the syntactic structure and its semantic interpretation, quantifier raising, underspecification, scope issues,…  are not fully satisfactory. Furthermore extension of linguistic studies to various languages have shown how complex quantification is in natural language and its relation to phenomena like generics, plurals,  and mass nouns.

Finally, and this can be seen as a link between formal models of quantification and natural language,  there by now exist psycholinguistic experiments that connect formal models and their computational properties to the actual way human do process sentences with quantifiers, and handle their inherent ambiguity, complexity, and difficulty in understanding.

All those aspects are connected in the didactics of mathematics and computer science: there are specific difficulties to teach (and to learn) how to  understand, manipulate,  produce and  prove quantified statements, and to determine  the proper level of formalisation between bare logical formulas and written or spoken natural language.

This workshop aims at gathering  mathematicians, logicians, linguists, computer scientists  to present their latest advances in the study of quantification.

Among the topics that wil be addressed are the following :

  • new ideas in quantification in mathematical logic, both model theory and proof theory:
    • choice functions,
    • subnectors (Russell’s iota, Hilbert’s epsilon and tau),
    • higher order quantification,
    • quantification in type theory
  • studies of the lexical, syntactic and semantic of quantification in various languages
  • semantics of noun phrases
  • generic noun phrases
  • semantics of plurals and mass nouns
  • experimental study of quantification and generics
  • computational applications of quantification and polarity especially for question-answering.
  • quantification in the didactics of mathematics and computer science.

Some recent relevant references:

  • Anna Szabolcsi Quantification Cambridge University Press 2010
  • Stanley Peters and Dag Westerstahl Quantifiers in Language and Logic Oxford Univ. Press 2010
  • Mark Steedman Taking Scope – The Natural Semantics of Quantifiers MIT Press 2012
  • Jakub Szymanik. Quantifiers and Cognition, Studies in Linguistics and Philosophy, Springer, 2015.
  • Vito Michele Abrusci, Fabio Pasquali, and Christian Retoré. Quantification in ordinary language and proof theory. Philosophia Scientae, 20(1):185–205, 2016.

Submissions:

The program committee is looking for  contributions introducing new viewpoints on quantification and determiners,  the novelty being either in the mathematical logic framework or in the linguistic description  or in the cognitive modelling. Submitting purely original work is not mandatory, but authors should clearly mention that the work is not original, and why they want to present it at this workshop (e.g. new viewpoint on already published results)

Submissions should be

In case the committee thinks it is more appropriate, some papers can be accepted as a poster with a lightning talk.

Final versions of accepted papers may be slightly longer. They will be published on line. We also plan to publish postproceedings

Programme committee:

  • Christian Retoré (Université de Montpellier & LIRMM-CNRS)
  • Mark Steedman (University of Edinburgh)
  • Vito Michele Abrusci (Università di Roma tre)
  • Mathias Baaz (University of Technology, Vienna)
  • Daisukke Bekki (Ochanomizu University, Tokyo)
  • Oliver Bott (Universität Tübingen)
  • Francis Corblin (Université Paris Sorbonne)
  • Martin Hakl (Massachusetts  Institute of Technology, Cambridge MA)
  • Makoto Kanazawa (National Institute of Informatics, Tokyo)
  • Dan Lassiter (Stanford University)
  • Zhaohui Luo (Royal Holloway College, London)
  • Alda Mari (CNRS Institut Jean Nicod, Paris)
  • Wilfried Meyer-Viol (King’s college, London)
  • Michel Parigot (CNRS IRIF, Paris)
  • Anna Szabolcsi (New-York University)
  • Jakub Szymanik (Universiteit van Amsterdam)
  • Dag Westerstahl (Stockholm University)
  • Bruno Woltzenlogel Paleo  (University of Technology, Vienna)
  • Richard Zach (University of Calgary)
  • Roberto Zamparelli (Università di Trento)

Jack Howard Silver, 1942-2016

From the Group in Logic and the Methodology of Science:

It is with great sadness that we announce that Professor Jack Howard Silver died on Thursday, December 22, 2016. Professor Silver was born April 23, 1942 in Missoula, Montana. After earning his A.B. at Montana State University (now the University of Montana) in 1961, he entered graduate school in mathematics at UC Berkeley. His thesis, Some Applications of Model Theory in Set Theory, completed in 1966, was supervised by Robert Vaught. In 1967 he joined the mathematics department at UC Berkeley where he also became a member of the Group in Logic and the Methodology of Science. He quickly rose through the ranks, obtaining promotion to associate professor in 1970 and to full professor in 1975. From 1970 to 1972 he was an Alfred P. Sloan Research Fellow. Silver retired in 2010. At UC Berkeley he advised sixteen students, three of whom were in the Group in Logic (Burgess, Ignjatovich, Zach).

 

His mathematical interests included set theory, model theory, and proof theory. His production was not extensive but his results were deep. Professor Silver was skeptical of the consistency of ZFC and even of third-order number theory. As Prof. Robert Solovay recently put it: “For at least the last 20 years, Jack was convinced that measurable cardinals (and indeed ZFC) was inconsistent. He strove mightily to prove this. If he had succeeded it would have been the theorem of the century (at least) in set theory.”

 

He will be greatly missed.

Jack’s contributions to set theory, according to Wikipedia (used under CC-BY-SA):

Silver has made several deep contributions to set theory. In his 1975 paper “On the Singular Cardinals Problem,” he proved that if κ is singular with uncountable cofinality and 2λ = λ+ for all infinite cardinals λ < κ, then 2κ = κ+. Prior to Silver’s proof, many mathematicians believed that a forcing argument would yield that the negation of the theorem is consistent with ZFC. He introduced the notion of master condition, which became an important tool in forcing proofs involving large cardinals. Silver proved the consistency of Chang’s conjecture using the Silver collapse (which is a variation of the Levy collapse). He proved that, assuming the consistency of a supercompact cardinal, it is possible to construct a model where 2κ++ holds for some measurable cardinal κ. With the introduction of the so-called Silver machines he was able to give a fine structure free proof of Jensen’s covering lemma. He is also credited with discovering Silver indiscernibles and generalizing the notion of a Kurepa tree (called Silver’s Principle). He discovered 0# in his 1966 Ph.D. thesis. Silver’s original work involving large cardinals was perhaps motivated by the goal of showing the inconsistency of an uncountable measurable cardinal; instead he was led to discover indiscernibles in L assuming a measurable cardinal exists.

[Photo ©Steven Givant. Picture taken on the occasion of the Tarski Symposium at UC Berkeley in 1971.]

Semantics and Proof Theory of the Epsilon Calculus

In Logic and Its Applications. ICLA 2017, edited by Sujata Ghosh and Sanjiva Prasad, 27–47. LNCS 10119. Berlin, Heidelberg: Springer.

The epsilon operator is a term-forming operator which replaces quantifiers in ordinary predicate logic. The application of this undervalued formalism has been hampered by the absence of well-behaved proof systems on the one hand, and accessible presentations of its theory on the other. One significant early result for the original axiomatic proof system for the 𝜀-calculus is the first epsilon theorem, for which a proof is sketched. The system itself is discussed, also relative to possible semantic interpretations. The problems facing the development of proof-theoretically well-behaved systems are outlined.

DOI 10.1007/978-3-662-54069-5_4
Preprint

Bjarni Jónsson, 1920-2016

Sad news via the FOM list today:

Published in Tennessean on Nov. 6, 2016

Bjarni Jónsson, originally of Draghals, Iceland, passed away in Cincinnati, OH on
Friday, September 30, 2016 at the age of 96. Beloved husband of the late Harriet P.
(nee Parkes) Jonsson. Devoted father of Eric (Kaye) Jonsson, Meryl (Bob) Runion Rose
and Kristin (Rick) Porotsky. Loving grandfather of Elisabeth (Terry) Winslow, David
Runion, and Brent, Gena, Aaron, Billy and Cole Porotsky. Former resident of Nashville,
Tennessee. He was Vanderbilt’s first Distinguished Professor of Mathematics. A leader
in his field and author of 89 technical papers, he received many commendations for his
work, including the Earl Sutherland Prize for Academic Research as well as the Knights
Cross awarded by the President of Iceland.

Please send donations in his honor to:

Bjarni Jonsson Research Prize
Department of Mathematics
1326 Stevenson Center
Vanderbilt University
Nashville, TN 37240.

Noted algebraist Bjarni Jónsson dies
by David Salisbury, Oct. 12, 2016
https://news.vanderbilt.edu/2016/10/12/noted-algebraist-bjarni-jonsson-dies/

Bjarni Jónsson, Vanderbilt’s first Distinguished Professor of Mathematics, died Sept.
30 at the age of 96.

Born in Iceland, Jónsson earned his bachelor’s and doctoral degrees from the
University of California-Berkeley and also received an honorary degree from the
University of Iceland. He was internationally recognized as a leading authority on
universal algebra, lattice theory and algebraic logic.

In his career, Jónsson authored 89 technical papers and served on the editorial board
of several major mathematics journals, including Algebra Universalis. He presented
numerous invited talks at mathematics conferences around the world. In 1974, he was an
invited speaker at the International Congress of Mathematicians. In 2012 he was
elected an inaugural fellow of the American Mathematical Society. He was also the
recipient of Vanderbilt’s Harvie Branscomb Distinguished Professor Award in 1974 and
the Earl Sutherland Prize for Achievement in Research in 1982.

“Bjarni Jónsson was a remarkable mathematician who made field-defining and path-
breaking contributions in universal algebra, lattice theory and algebraic logic.
Anyone who had the fortune to know him admired his integrity, kindness and immense
respect for colleagues and friends. His influence on my personal and mathematical life
has been enormous, and it is a great privilege that I have had the opportunity to work
with and learn from him,” said Professor Constantine Tsinakis, a long-term colleague
and a former chair of the mathematics department.

“To me Bjarni will always be a legend, who in his quiet, sincere, unassuming ways
continues to inspire uncountably many algebraists, raising questions and re-examining
areas that he feels would benefit from an algebraic approach,” wrote Peter Jipsen, one
of the doctoral students that Jónsson advised, on the occasion of his 70th birthday.
“While some mathematicians almost revel in stringing together long complex arguments,
Bjarni has constantly sought to simplify and illuminate the subjects dear to him,” the
professor of mathematics at Chapman University added.

Jónsson came to Vanderbilt in 1966 and taught here until his retirement in 1993. When
he arrived, mathematics was mostly an undergraduate teaching department. He was
instrumental in establishing the department’s graduate program, which presently ranks
among the top departments in the nation, according to the latest evaluation by the
National Research Council. Jónsson also formed a research group in algebra that
attracted mathematicians from around the world and contributed substantially to the
high research profile that the department currently enjoys.

Algebra is the study of mathematical objects and the rules for manipulating them.
Jónsson made his most important contributions in the area of universal algebra. It is
one of the most abstract subfields of algebra because it studies algebraic structures
in general, as opposed to specific classes of algebras, such as groups and fields. The
importance of his contributions is reflected by the fact that a number of mathematical
objects are named for him, including Jónsson and Jónsson-Tarski algebras, Jansson
cardinals, Jónsson terms, the Jónsson lemma and the Jónsson-Tarski duality.

During his tenure, Jónsson supervised 14 Ph.D. students. In letters they wrote for a
symposium in honor of his 70th birthday, which took place in Iceland in 1990, his
former students all expressed a deep appreciation for him as a “respected mathematical
guide and personal friend.”

One of the first students he supervised, Steven Monk, now professor emeritus at the
University of Washington, recalled advice that he received from Jónsson regarding
teaching: “Adventure is not in the guidebook and beauty is not on the map. The best
one can hope for is to be able to persuade some people to do some traveling on their
own.”

“Bjarni’s work and scholarly contributions will have a lasting legacy. His name will
forever be interwoven in the history of our department. We are honored to have had
him as a colleague,” noted the current department chair, Professor Mike Neamtu.

[Photo ©Steve Givant]

(SEP ∧ SSHAP) → Calgary

In May 2017, both the Society for Exact Philosophy and the Society for the Study of the History of Analytic Philosophy will hold their annual meetings at the University of Calgary. Come for one, stay for the other, or come for both and stay for Banff National Park in the Canadian Rockies! Keynotes will be given by Juliet Floyd, Robin Jeshion, and Bernie Linsky at SSHAP and Catarina Dutilh Novaes, Louise McNally, and Dorit Ganson at SEP.

 

Immediately before SEP, the Calgary Graduate Student Conference will also be held; the topic will be “Ethics in the Age of Science.” Keynote speakers will be Katrina Sifferd and Gregg Caruso.

Interview with Hao Wang and Robin Gandy

In 1991, I videotaped talks at the Kurt Gödel Colloquium in Kirchberg (it was supposed to be held jointly with the Wittgenstein Symposium, that got cancelled). I also videotaped a conversation with Hao Wang and Robin Gandy, students and friends, respectively, of Gödel and Turing.  I can’t for the life of me remember who the interviewer was. Anyway, you may find it interesting:

[Photo credit: San and Jane Wang]