In a recent talk I argued that the computational reverse mathematics suggested by Richard Shore in his 2010 paper, ‘ Reverse mathematics: the playground of logic ’, was not suitable for the job of analysing which theorems of ordinary mathematics are assertible by proponents of foundational systems such as predicativism or finitistic reductionism. This is because the relation of computable…
The Bristol Formal Methods Seminar is aimed at teaching new postgraduates some of the formal methods used in much of modern philosophy. During the first term we’ve concentrated on logic: thus far the sessions have covered introductory set theory, basic metatheorems of first order logic, and the incompleteness of arithmetic. Next up are modal and temporal logic, while after Easter the focus will…
In December 2011 I gave a presentation on reverse mathematics to the local logic seminar. Having neglected this site for so long, it seemed like a good idea to publish my handout from the presentation here. Here’s a teaser: In ordinary mathematical practice, mathematicians prove theorems, reasoning from a fixed set of axioms to a logically derivable conclusion. The axioms in play are usually…
This year I’ve been running a reading group on type theory. Our primary text is Proofs and Types by Jean-Yves Girard, Yves Lafont and Paul Taylor. The focus of the book is the development of the typed λ-calculus, with a strong proof-theoretic slant, these two perspectives being unified by the Curry-Howard correspondence . It begins by exploring the connections between intuitionistic logic and the…
Firmin is a JavaScript animation library that uses CSS transforms and transitions to create smooth, hardware-accelerated animations. Firmin is fundamentally very simple: all it does is parse descriptions of animations and then execute them by manipulating the style property of the animated element. Here’s an example: moving an element right 200 pixels and down 100 pixels in half a second, while…
Every few months I upgrade my server’s Nginx and Passenger installations, and whenever I do, it takes me a minute to remember how it all goes. This article explains how to compile them from scratch, and also how to upgrade either or both programs. My server runs Ubuntu 10.04, but it should be straightforward to modify these instructions to work on any Linux distribution or other POSIX-compliant…
There are few languages as simple yet as widely used as classical propositional logic—perhaps only elementary arithmetic can claim a similar status. The propositional calculus , as it is also known, is a staple of first-year university logic courses. As I recall from when I did just such a course, one of the most tedious parts was calculating truth tables for various complex logical expressions.…
JavaScript’s dynamic nature makes it hard to straightforwardly apply many functional programming idioms. One example of this is currying : any function may be passed an arbitrary number of arguments, making it impossible to write a truly general currying function. To recap, currying is a technique for transforming a function which accepts n parameters into a nest of partially applicable functions.…