## Category Archives: Talks

I recently (May 1) gave a short presentation touching on ethics and technology, as well as the ethics of Internet pornography.  I am sharing the slides here.  Sadly, most of the references on the seemingly unending list of harms and evils associated with pornography are behind paywalls, although the article by Max Waltman is freely available.  As always when reading about this topic, please be aware that some of the material can be quite upsetting for people who have experienced sexual assault, abuse, childhood assault, or other traumatic experiences, as well as for young readers.

Last week I had the great pleasure of visiting the amazing PL group at Indiana University.  They are doing so much inspiring research in many different areas of programming languages research.  It was great.  The collective knowledge there was very impressive, and I got a lot of great references to follow up on now that I am back.

I gave two talks: one in the logic seminar, and one for the PL group.  In the first talk, one issue I was discussing was an argument, originally sketched by Michael Dummett and developed more fully by Charles Parsons in a paper called “The Impredicativity of Induction” (you can find a revised version of this paper in a book called “Proof, Logic, and Formalization” edited by Michael Detlefsen) — this argument claims to show that induction is impredicative.  Impredicativity, as many QA9 readers well know, is the property of a definition D of some mathematical object x that D refers to some collection or totality of which x is a member.  Philosophical constructivists must reject impredicative definitions, because they believe that the definition are constructing or creating the entities defined, and hence cannot presuppose that those entities already exist in the course of defining them.  This kind of philosophical constructivism must be distinguished from a kind of formal constructivism a type theorist is likely to care about, which I identify with a canonical forms property: every inhabitant of a type A should have a canonical form which is part of the essential nature of type A.  Computational classical type theory violates this formal canonicity property, because types like $A \vee \neg A$ are inhabited by terms which are neither left nor right injections.

Here is Parsons’s argument as I understand (or maybe extrapolate?) it.  A philosophical constructivist must reject impredicative definitions, such as the kind one gives for the natural numbers in second-order logic (see my talk slides for this example definition).  As an alternative, one may try to say that the meaning of the natural number type is determined by introduction and elimination rules (similarly to the meanings of logical connectives).  The introduction rules are about the constructors of the type.  And the elimination rule is an induction principle for the type.  But then, Parsons and Dummett point out, this explanation of the natural number (or other) inductive type is not any better off with respect to impredicativity than the second-order definition, because the induction principle allows us to prove any property P of n, assuming as premises that Nat n holds and that the base and step cases of induction are satisfied for P.  But the predicate P could just as well be Nat itself, or some formula which quantifies over Nat.  The latter seems to provoke worries, which I do not understand.  It seems already bad enough that P could be Nat.  So just moving from a single formula defining Nat to a schematic rule defining Nat cannot save one from the charge of impredicativity.  Hence, for avoiding impredicativity, there is no reason to prefer one approach (specifically, the rule-based approach) over the other.

The alternative to this is to reject the idea that we must give a foundational explanation of the natural-number type (or predicate).  We just accept the idea of numbers and other datatypes as given, and then induction is a consequence — not part of some definition of numbers, which we are refusing to give.  This is a coherent way to avoid impredicativity, but at the cost of having to accept numbers with no deeper analysis — something that a logicist might not like, for example (though I do not know for sure how a logicist would likely view this situation).

I am giving a talk this afternoon titled “From Logic with Love” as part of a special class organized by U. Iowa English Prof. Judith Pascoe, where professors from different departments give talks from the perspective of their discipline on the topic “What We Talk About When We Talk About Love”.  The slides are here.  I am also including some links and notes below, for students interested in further reading.

The short story Beginners, by Raymond Carver, can be found here.  This is the original version of the story that was published as “What We Talk About When We Talk About Love”.

Ray Monk’s biography of Bertrand Russell, while loathed by admirers of Russell, is extremely interesting and revealing reading.

Constance Reid’s biography of David Hilbert is also very interesting and enjoyable reading.  It includes a reprint of much of the text of his famous 1900 Paris lecture on future problems of mathematics.

Some Computer Science news articles related to the talk:

Other related articles:

A Man For Others by Patricia Treece is an excellent read about Maximilian Kolbe.  It contains first-hand reports and recollections from many different people who knew the saint.

I am driving over this morning to the Computer and Information Sciences department at St. Ambrose University in nearby Davenport, Iowa, to give a brief talk (slides here) and talk to students and faculty about graduate study at The University of Iowa.

Anyhow, I had a great time talking with Kevin, Mark, and Gary, and learning more about St. Ambrose.   The school has around 3300 (full-time equivalent) students, of whom  around 2600 are undergraduates.  I got the impression that most are from Davenport or nearby, with a significant percentage of nontraditional (age) students and commuters who don’t live on campus.  The CS department has something like 80 students in a number of different majors the department offers.  The campus itself is very nice: it occupies something like a 4-block by 4-block square in Davenport.  The building we were in for my talk, the Rogalski Center, is very nice and quite new.  Kevin walked me around campus, including the lovely chapel; there was a beautiful Madonna and Child by Fr. Catich, founder of the art department at St. Ambrose and known for beautiful art works on slate of religious scenes (like this).

Our department has sent faculty out to I think it is 8 or 9 colleges in the region this fall, to try to increase our domestic applicant pool for graduate study.  I very much hope this succeeds — that’s the kind of extra work on grad admissions we want to have!

I am driving what Google Maps tells me are the three hours down to Kirksville, Missouri, from Iowa City, to visit the Math & CS department at Truman State.  I am hoping to meet some more fantastic potential graduate students like Truman alum Ben Delaware (whose paper was just accepted to POPL 2013 — congratulations, Ben!).

The slides for my talk on “Programs, Proofs, and Classical Logic” are here.  I am planning to update this post with a little more about the trip once I get back.

[Updated the day after the trip:]

It was a very interesting trip down to Kirksville, on some quiet rural highways through eastern Iowa.  The Truman State campus is very nice, quite charming actually.  I met up with Jon Beck, a CS faculty member who coincidentally turns out to have ties to Iowa (David Eichmann, of U. Iowa Biomedical Informatics, was his advisor, at another institution).  We had a very engaging conversation about CS, CS education, and CS at Truman State.  The school transformed itself a couple decades back from what Jon described as a “sleepy teachers’ college” (presumably that phrase associates to the right), into a highly selective public liberal arts college.  They actually got the Missouri legislature to agree to let them be as selective in their admissions as they want.  This makes a huge difference, since it means they can focus on admitting just people who are adequately prepared and seriously motivated for college study.  The same cannot be said about U. Iowa, for example.  I also got a little tour of the campus, which again is really idyllic.  I like U. Iowa, but I was a bit jealous of the campus there, truly.

I got to talk informally with a few other folks, and then gave my talk and made my grad-school pitch in the afternoon.  The talk was really well attended — solely by undergrads, and no one would confess to any bribery to get them there.  I was impressed.  I got some great questions about both the research I was discussing, and about grad school in general.  The students seemed sharp and engaged.  I am certainly hoping that we get a couple applications from Truman Math & CS this season!

In a couple weeks I am going to do another of these, at St. Ambrose in Davenport, Iowa.  Other colleagues from U. Iowa CS are making similar trips to nearby colleges.  We are hoping these will bear some fruit in more domestic applications for grad school here.