The Unnameable

Frege has a puzzling doctrine that functions are unsaturated entities. This paper is devoted to an attempted elucidation of the dark and mysterious metaphors surrounding this doctrine. I advocate a minimalistic interpretation of Frege's doctrine, namely that unsaturated things are entities of higher type, no more, no less. Further aspects of the Fregean doctrine, particularly those which give a stronger reading to the notion of incomplete entities, are rejected as irrelevant excrescences. In particular, the idea that functions are unnameable is consigned to the flames as both unnecessary and incoherent.

The Expressivity and Frame Definability of H(@, \downarrow)

The talk will be about the expressivity and frame definability of the hybrid logic extended with the satisfaction operator @ and the downarrow operator \downarrow. We will start by seeing the characterization result for the expressivity: H(@, \downarrow)-formulas are invariant under generated submodels. We will then go on to see the characterization result for frame definability, which is given by the equivalence of the following three clauses: (1) K is definable by a set of H(@, \downarrow)-sentences; (2) K is definable by a single pure H(@, \downarrow)-sentences; and (3) K is closed under generated subframes and reflects finitely generated subframes, where K is an elementary frame class. At the end, we will obtain a syntactic condition for a H(@, \downarrow)-sentence to define an elementary frame class by extending the definition of Sahlqvist formulas to the language of H(@, \downarrow). In the light of the frame definability result, the fragment obtained by the revised notion of Sahlqvist formulas is the fragment of formulas that are equivalent (on the level of frames) to pure formulas.

Godel: Missed Connections, Alternate Directions

I'll point out a number of ways in which Skolem and Godel talked past each other in the early 1930s. Finally, in a more speculative vein, I'll explore a suggestion Godel made in his Gibbs Lecture from which he later decisively distanced himself.

The Paradox of Confirmation

Does the observation of a white shoe confirm that all ravens are black? Hempel and Goodman thought so (for at least one clarification of this question). Quine disagreed. Surprisingly, most contemporary discussions of the paradox (here, I have in mind probabilistic, i.e., Bayesian treatments) tend to follow Hempel and Goodman on this question (even though that is not really their aim).

My aims in this talk will be three: (1) to carefully retrace the history of the paradox, (2) to clarify the structure of the paradox, within a contemporary, probabilistic framework, and (3) to provide an improved Bayesian analysis of the clarified paradox (this new Bayesian analysis is drawn from recent joint work with Jim Hawthorne).

Empiricism and semantics: Neurath's critique of Tarski's theory of truth

It is well known that Tarski's theory of truth had a lasting impact on some members of the Vienna circle, such as Carnap. Less known is that Tarski's work appeared in the midst of a debate on the nature of truth which involved several members of the Vienna circle. This debate sets the stage for Neurath's unrelenting criticism of Tarski's theory of truth. In my talk I reconstruct the nature of Neurath's criticisms and his positive account of what truth consists in ('acknowledgement theory'). As Neurath did not publish on his criticisms of Tarskian semantics, the reconstruction will make extensive use of unpublished archival sources from the Neurath Nachlass.

Computers and the Future of Mathematical Proofs

It is relatively common for the mathematical proof of a single theorem to run hundreds of pages. It has also become common for mathematical proofs to rely on computer calculations. An editor of one of the most prestigious mathematical journals has recently declared that it has become impossible to find peers who are willing to review computer code. As a result, the journal has started to publish theorems without any meaningful review of the underlying computer code. My response has been to turn to formal proofs, where every logical inference of a proof is checked by computer. What do these developments mean for computers and the future of mathematical proofs?