I consider a familiar argument for two-boxing in Newcomb's Problem and find it defective because it involves a type of divergence from standard Baysian reasoning, which, though sometimes justified, conflicts with the stipulations of the Newcomb scenario. In an appendix, I also find fault with a different argument for two-boxing that has been presented by Graham Priest.

My subject is the theory of blame recently propounded by George Sher in his book, In Praise of Blame. I argue that although Sher has succeeded in capturing a number of genuine features of the concept of blame, there is an important element that he has omitted, which is the fact that necessarily, when A blames B for something and expresses this to B, A will realise that B is likely to find this unpleasant. The inclusion of the latter element (...) renders the question of whether any agent ever deserves blame a more open one than Sher allows. (shrink)

Mathematics is about proofs, that is the derivation of correct statements; and calculations, that is the production of results according to well-defined sets of rules. The two notions are intimately related. Proofs can involve calculations, and the algorithm underlying a calculation should be proved correct. The aim of the author is to explore this relationship. The book itself forms an introduction to simple type theory. Starting from the familiar propositional calculus the author develops the central idea of an applied lambda-calculus. (...) This is illustrated by an account of Gödel's T, a system which codifies number-theoretic function hierarchies. Each of the book's 52 sections ends with a set of exercises, some 200 in total. These are designed to help the reader get to grips with the subject, and develop a further understanding. An appendix contains complete solutions of these exercises. (shrink)

Each Girard quantale (i.e., commutative quantale with a selected dualizing element) provides a support for a semantics for linear propositional formulas (but not for linear derivations). Several constructions of Girard quantales are known. We give two more constructions, one using an arbitrary partially ordered monoid and one using a partially ordered group (both commutative). In both cases the semantics can be controlled be a relation between pairs of elements of the support and formulas. This gives us a neat way of (...) handling duality. (shrink)

I answer an argument from Charles Travis to the conclusion that minimalism about truth cannot cope with the context sensitivity of words. To do this, I construct a thought experiment involving a community whose language does not manifest context sensitivity, but whose statements do seem to be subject to truth in a minimalist sense.

This work is derived from the SERC "Logic for IT" Summer School Conference on Proof Theory held at Leeds University. The contributions come from acknowledged experts and comprise expository and research articles which form an invaluable introduction to proof theory aimed at both mathematicians and computer scientists.

Each Girard quantale (i.e., commutative quantale with a selected dualizing element) provides a support for a semantics for linear propositional formulas (but not for linear derivations). Several constructions of Girard quantales are known. We give two more constructions, one using an arbitrary partially ordered monoid and one using a partially ordered group (both commutative). In both cases the semantics can be controlled be a relation between pairs of elements of the support and formulas. This gives us a neat way of (...) handling duality. (shrink)

Each Girard quantale provides a support for a semantics for linear propositional formulas. Several constructions of Girard quantales are known. We give two more constructions, one using an arbitrary partially ordered monoid and one using a partially ordered group. In both cases the semantics can be controlled be a relation between pairs of elements of the support and formulas. This gives us a neat way of handling duality.

I modify the standard coverage construction of the reals to obtain the irrationals. However, this causes a jump in ordinal complexity from ω+1 to Ω.

The standard method of generating countable ordinals from uncountable ordinals can be replaced by a use of fixed point extractors available in the term calculus of Howard’s system. This gives a notion of the intrinsic complexity of an ordinal analogous to the intrinsic complexity of a function described in Gödel’s T.

In Simmons (Arch Math Logic 43:65–83, 2004), I described a method of producing ordinal notations ‘from below’ (for countable ordinals up to the Howard ordinal) and compared that method with the current popular ‘from above’ method which uses a collapsing function from uncountable ordinals. This ‘from below’ method employs a slight generalization of the normal function—the fruitful functions—and what seems to be a new class of functions—the helpful functions—which exist at all levels of the function space hierarchy over ordinals. Unfortunately, (...) I was rather sparing in my description of these classes of functions. In this paper I am much more generous. I describe the properties of the helpful functions on all finite levels and, in the final section, indicate how they can be used to simplify the generation of ordinal notations. The main aim of this paper is to fill in the details missing from [7]. The secondary aim is to indicate what can be done with helpful functions. Fuller details of this development will appear elsewhere. (shrink)

This book argues that moral desert should be excluded as a consideration in normative and applied ethics, as it is likely that no-one ever morally deserves anything for their actions and, if they do, it is in most cases impossible to know what. I also explain how moral deliberation in relation to punishment, distributive justice and personal morality can proceed without appeals to moral desert.

This is a response to a paper by N.M.L. Nathan in which he argues that the attempt to provide a global justification of our entire set of beliefs necessarily leads to an infinite regress, in contrast with cases of local uncertainty, which he thinks can be resolved without regress. I argue that if he is right about the local uncertainty case, then he should not fear a regress in the global case, as the two situations are more similar than he (...) supposes. (shrink)

I survey the syntactic technique of tiering which can be used to restrict the power of a recursion scheme. I show how various results can be obtained entirely proof theoretically without the use of a model of computation.

By taking a closer look at the construction of an Ackermann function we see that between any primitive recursive degree and its Ackermann modification there is a dense chain of primitive recursive degrees.