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)

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)

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.

This book is a defense of the view that the distinctive feature of a normative statement is the expression of an attitude. Moral statements are a sub-class of normative statements: (roughly) those that express both an attitude AND the proposition that this attitude is of a certain type (related to such things as kindness, compassion and honesty). Much attention is devoted to the 'Frege/Geach problem', and an 'inferentialist' approach is developed to deal with this. As far as the truth and (...) falsity of normative statements is concerned, it is argued that they may be regarded as truth-apt in a broad sense, but not (always) in a narrower sense, pertaining to 'mind-to-world fit'. The book considers alternatives to the expressivist theory, but finds them all wanting. It also considers how we should view the practice of attempting to develop moral theories in light of the truth of expressivism. The concluding chapter looks at such issues as the nature of normative disagreement and the relevance of expressivism to belief in God. (shrink)

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.