Logblog: Richard Zach's Logic Blog

University of Calgary

UofC Navigation

Submitted by Richard Zach on Wed, 06/11/2008 - 11:19am

The first issue of the Review of Symbolic Logic will be out soon (Cambridge UP page here). The Review, like the Journal and Bulletin of Symbolic Logic will be mailed to all members of the Association for Symbolic Logic. So if you're not a member (and you probably should be, if you're reading this!), join now! (Only 76$ per year--38$ for students-- for three of the most important journals in logic, plus all the other benefits of membership)

Table of contents:

A Cut-Free Simple Sequent Calculus for Modal Logic S5

FRANCESCA POGGIOLESI . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3

How Applied Mathematics Became Pure

PENELOPE MADDY . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16

The Closing of the Mind: How the Particular Quantifier Became Existentially Loaded Behind Our Backs

GRAHAM PRIEST . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42

Recognizing Strong Random Reals

DANIEL OSHERSON AND SCOTT WEINSTEIN. . . . . . . . . . . . . . . . 56

Truth-Functionality

BENJAMIN SCHNIEDER . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64

Probabilistic Conditionals are Almost Monotonic

MATTHEW P. JOHNSON AND ROHIT PARIKH . . . . . . . . . . . . . . . . 73

On Adopting Kripke Semantics in Set Theory

LUCA INCURVATI . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 81

The Iterative Conception of Set

THOMAS FORSTER . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 97

A Decision Procedure for Probability Calculus with Applications

BRANDEN FITELSON . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 111

Ultimate Truth vis-à-vis Stable Truth

P.D. WELCH . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 126

Submitted by Richard Zach on Mon, 06/09/2008 - 9:09am

Last week, Brian Leiter posted about possibly re-drawing the dividing lines between the specialty areas ranked in the Philosophical Gourmet Report

In a comment, Cian asks:

Philosophical Logic and Mathematical Logic. While there is a fair amount of divergence between the two rankings, I also see, for example, that NYU gets ranked at 4.5 in mathematical logic even though as far as I can see, almost everything the relevant people have written about logic is more naturally classified as philosophical logic than as mathematical logic. Is that a sign that the borderline between these two areas is too wide and fuzzy for the distinction to be worth making by the PGR?

If one thinks of mathematical logic as "formal logic motivated by mathematical concerns"---roughly, this is the conception according to which mathematical logic consists of model theory, set theory, recursion theory, and proof theory--then it is indeed puzzling why NYU gets ranked at the top of group 2 in the mathematical logic ranking, in addition to the top in the philosophical logic ranking. But one might also think of mathematical logic the way it's defined in the AMS Mathematics Subject Classification (03). Now how do we take "philosophical logic"? But if we take the now-standard (at least in North America) definition of "philosophical logic", then it's that part of formal logic that paradigmatically includes: "various versions of modal, temporal, epistemic, and deontic logic; constructive logics; relevance and other sub-classical logics; many-valued logics; logics of conditionals; quantum logic; decision theory, inductive logic, logics of belief change, and formal epistemology; defeasible and nonmonotonic logics; formal philosophy of language; vagueness; and theories of truth and validity" (from editorial description of the Journal of Philosophical Logic). Almost all of that is included in MSC 03Bxx! Clearly, for the purpose of the PGR at least, it would be better to define "mathematical logic" as "formal logic, but not philosophical logic".

I don't know if the evaluators for the PGR "mathematical logic" and "philosophical logic" categories get instructions on the intended scope of the category. It probably also makes a big difference--bigger than in other specialty areas--if faculty with appointments in the mathematics (or computer science) departments get included in the PGR faculty lists. As the note at the bottom of the ranking says, "much work in mathematical logic goes on in Mathematics and Computer Science departments."

Then there's also the confusion between the definition of "philosophical logic" as "formal logic motivated by philosophy" and the older (British) use of "philosophical logic" to mean "philosophy motivated by logic" (and including philosophical study of notions such as reference, necessity, truth, analyticity, etc.) Maybe a better term for that is "philosophy of logic". Leiter's proposed restructuring would have a category "philosophy of language & logic" (but no philosophical logic category).

I don't think that "philosophical logic" and "mathematical logic" should be combined in the PGR ranking. But as it currently stands--with the scope of these categories so unclear--the rankings aren't particularly informative. I'm not sure what would be more informative, but getting clarity on the definitions would be one step. Maybe it wouldn't be such a bad idea to include "philosophy of logic" in the "philosophy of language" category, and reserve "philosophical logic" for the formal work you find in the JPL or the Review of Symbolic Logic. Maybe it wouldn't even be a bad idea to merge mathematical logic into the philosophy of mathematics category. What do others think?

Submitted by Richard Zach on Mon, 06/02/2008 - 5:41pm

What more do we know about a theorem if we have a proof (by restricted means) than merely that it is true? That's an old question of Kreisel's that motivated his "unwinding program": extract additional information from proofs of theorems in constructive theories, such as bounds on y in theorems of the form ?x?y A(x, y).

Ulrich Kohlenbach has worked on problems like this more than anyone else, and his book Applied Proof Theory: Proof Interpretations and Their Use in Mathematics is now out from Springer.

Ulrich Kohlenbach presents an applied form of proof theory that has led in recent years to new results in number theory, approximation theory, nonlinear analysis, geodesic geometry and ergodic theory (among others). This applied approach is based on logical transformations (so-called proof interpretations) and concerns the extraction of effective data (such as bounds) from prima facie ineffective proofs as well as new qualitative results such as independence of solutions from certain parameters, generalizations of proofs by elimination of premises.The book first develops the necessary logical machinery emphasizing novel forms of Goedel's famous functional (Dialectica) interpretation. It then establishes general logical metatheorems that connect these techniques with concrete mathematics. Finally, two extended case studies (one in approximation theory and one in fixed point theory) show in detail how this machinery can be applied to concrete proofs in different areas of mathematics.

1 Introduction

2 Unwinding proofs (‘Proof Mining’)

2.1 Introductory remark

2.2 Informal treatment of ineffective proofs

2.3 Herbrand’s theorem and the no-counterexample interpretation

2.4 Exercises, historical comments and suggested further reading3 Intuitionistic and classical arithmetic in all finite types

3.1 Intuitionistic and classical predicate logic

3.2 Intuitionistic (‘Heyting’) arithmetic HA and Peano arithmetic PA

3.3 Extensional intuitionistic (‘Heyting’) and classical (‘Peano’)

arithmetic in all finite types

3.4 Fragments of (W)E-HA^? and (W)E-PA^?

3.5 Fragments corresponding to the Grzegorczyk hierarchy

3.6 Models of E-PA^?

3.7 Exercises, historical comments and suggested further reading4 RepresentationofPolish metric spaces

4.1 Representation of real numbers

4.2 Representation of complete separable metric (‘Polish’) spaces

4.3 Special representation of compact metric spaces

4.4 Fragments, exercises, historical comments and suggested further

reading5 Modified realizability

5.1 The soundness and program extraction theorems

5.2 Remarks on fragments of E-HA^?

5.3 Exercises, historical comments and suggested further reading6 Majorizability and the fan rule

6.1 A syntactic treatment of majorization and the fan rule

6.2 Exercises, historical comments and suggested further reading7 Semi-intuitionistic systems and monotone modified realizability

7.1 The soundness and bound extraction theorems

7.2 Fragments, exercises, historical comments and suggested further

reading8 Gödel’s functional (‘Dialectica’) interpretation

8.1 Introduction

8.2 The soundness and program extraction theorems

8.3 Fragments, exercises, historical comments and suggested further

reading9 Semi-intuitionistic systems and monotone functional interpretation

9.1 The soundness and bound extraction theorems

9.2 Applications of monotone functional interpretation

9.3 Examples of axioms ? : Weak König’s lemmaWKL

9.4 WKL as a universal sentence ?

9.5 Fragments, exercises, historical comments and suggested further

reading10 Systems based on classical logic and functional interpretation

10.1 The negative translation

10.2 Combination of negative translation and functional interpretation

10.3 Application: Uniform weak König’s lemma UWKL

10.4 Elimination of extensionality

10.5 Fragments of (W)E-PA^?

10.6 The computational strength of full extensionality

10.7 Exercises, historical comments and suggested further reading11 Functional interpretation of full classical analysis

11.1 Functional interpretation of full comprehension

11.2 Functional interpretation of dependent choice

11.3 Functional interpretation of arithmetical comprehension

11.4 Functional interpretation of (IPP) by finite bar recursion

11.5 Models of bar recursion

11.6 Exercises, historical comments and suggested further reading12 A non-standard principle of uniform boundedness

12.1 The ?^0_1 -boundedness principle

12.2 Applications of ?^0_1 -boundedness

12.3 Remarks on the fragments E-G_nA^?

12.4 Exercises, historical comments and suggested further reading13 Elimination of monotone Skolem functions

13.1 Skolem functions of type degree 1 in fragments of finite type

arithmetic

13.2 Elimination of Skolem functions for monotone formulas

13.3 The principle of convergence for bounded monotone sequences

of real numbers (PCM)

13.4 ?^0_1 -CA and ?^0_1 -AC

13.5 The Bolzano-Weierstraß property for bounded sequences in R^d

13.6 Exercises, historical comments and suggested further reading14 The Friedman A-translation

14.1 The A-translation

14.2 Historical comments and suggested further reading15 Applications to analysis: general metatheorems I

15.1 A general metatheorem for Polish spaces

15.2 Applications to uniqueness proofs

15.3 Applications to monotone convergence theorems

15.4 Applications to proofs of contractivity

15.5 Remarks on fragments of T^?

15.6 Historical comments and suggested further reading16 Case study I: Uniqueness proofs in approximation theory

16.1 Uniqueness proofs in best approximation theory

16.2 Best Chebycheff approximation I

16.3 Best Chebycheff approximation II

16.4 Best L_1-approximation

16.5 Exercises, historical comments and suggested further reading17 Applications to analysis: general metatheorems II

17.1 Introduction

17.2 Main results in the metric and hyperbolic case

17.3 The case of normed spaces

17.4 Proofs of theorems 17.35, 17.52 and 17.69

17.5 Further variations

17.6 Treatment of several metric or normed spaces X_1 . . . , X_n

simultaneously

17.7 A generalized uniform boundedness principle ?-UB^X

17.8 Applications of ?-UB^X

17.9 Fragments of A^? [. . .]

17.10 Exercises, historical comments and suggested further reading18 Case study II: Applications to the fixed point theory of nonexpansive

mappings

18.1 General facts

18.2 Applications of the metatheorems from chapter 17

18.3 Logical analysis of the proof of the Borwein-Reich-Shafrir

theorem

18.4 Asymptotically nonexpansive mappings

18.5 Applications of proof mining in ergodic theory

18.6 Exercises, historical comments and suggested further reading19 Final comments

Submitted by Richard Zach on Mon, 05/19/2008 - 10:07am

From my colleague up north, Rob Wilson:

The What Sorts of People blog is now up and running: check it out. This is the blog for the What Sorts of People Should There Be? network, a collaborative blog with regular contributions from around 10 team members. Short, recent posts are available on double-amputee Oscar Pistorius's bid to compete Olympically, and on a so-recent-it's-still-forthcoming piece by Steve Pinker in The New Republic on the concept of dignity and its use in a recent President's Council on Bioethics report. Biella Coleman, who was a Killam Postdoc at Alberta last year and now teaches at NYU, has just posted a tempered rant on the blog on medical genetics and eugenics.

Submitted by Richard Zach on Sat, 05/17/2008 - 11:44am

Rob Loftis has a roundup of open access introductory logic textbooks. And Hans von Ditmarsch has a list of logic course software.

Submitted by Richard Zach on Wed, 05/14/2008 - 10:07am

Submitted by Richard Zach on Wed, 05/14/2008 - 8:09am

You probably all know the result that Peano Arithmetic is not finitely axiomatizable (a result due to Ryll-Nardzewski), and a similar result for ZFC (due to Richard Montague, I believe). The standard axiom system for PA is not finite since the axiom scheme of induction stands for infinitely many sentences. Ryll-Nardzewski showed that there is no finite set S of sentences in the language of PA so that S ? ? iff PA ? ?. I don't know how widely known this is,^{*} but by contrast it is possible to finitely axiomatize (almost) any theory T, if you allow new predicate symbols in the axiomatization. This is a result due to Kleene:

Stephen Cole Kleene, Finite axiomatizability of theories in the predicate calculus using additional predicate symbols, in: Two Papers on the Predicate Calculus. Memoirs of the American Mathematical Society, no. 10, Providence, 1952, 27-68.

The "almost" above, as you might have guessed, applies to the theory itself: it has to be recursively enumerable and, if the language includes identity, must have only infinite models (Kleene's original paper does not deal with identity). The basic idea is that you use the new predicate symbols to finitely axiomatize a weak arithmetic in which you can formalize semantics and do primitive recursion. The first part gives you a truth predicate for the language of T, the second part gives you a predicate that's satisfied of exactly the Gödel numbers of sentences of T. Then you say that all the axioms of the (r.e.) theory T are true. Kleene's result was later strengthened by Craig and Vaught in:

William Craig and Robert L. Vaught, Finite axiomatizability using additional predicates. The Journal of Symbolic Logic 23 (1958) 289-308.

A sketch of Craig and Vaught's proof is given in Michael Makkai's review.

^{*}According to Google Scholar, Kleene's monograph is cited a lot, but as far as I can tell overwhelmingly for the other paper, which is another classic logic paper: "Permutation of inferences in Gentzen’s calculi LK and LJ."

Submitted by Richard Zach on Sat, 04/26/2008 - 2:17pm

So the colloquium honoring the recipients of the Gödel Research Fellowships is tomorrow. There should be a live feed. It starts at 9:00 CDT (that's midnight tonight on the West Coast, and 3 am Eastern). I'll try to find out if the lectures will be archived.

Submitted by Richard Zach on Tue, 04/22/2008 - 7:55am

Erich Reck's entry on Richard Dedekind in the SEP is now online. I'm particularly happy about this one: It's time Dedekind gets some of the attention for his philosophy of math that Frege's been getting for his, and Erich's entry as well as his other work, I hope, will help bring that about.

While many of Dedekind's contributions to mathematics and its foundations are thus common knowledge, they are seldom discussed together. In particular, his mathematical writings are often treated separately from his foundational ones. This entry provides a broad survey of his contributions. The main focus will be on his foundational writings, but they will be related to his other mathematical work. Indeed, it will be argued that foundational concerns are at play throughout Dedekind's work, so that any attempt to distinguish sharply between his “mathematical” and “foundational” writings is artificial and misleading. Another goal of the entry is to establish the continuing relevance of his contributions to the philosophy of mathematics. Indeed, their full significance has only started to be recognized, as should become evident along the way. This is especially so with respect to methodological and epistemological aspects of Dedekind's work, which shape and ground the logical and metaphysical views that emerge in his writings.

I also recommend: "Dedekind's Structuralism: An Interpretation and Partial Defense", *Synthese *137:3, 2003, pp. 369-419 (paper)

Submitted by Richard Zach on Thu, 04/17/2008 - 12:18am

Two more new entries in the Stanford Encyclopedia of interest to logicians:

The Development of Proof Theory by Jan von Plato and Non-wellfounded Set Theory by Larry Moss.

From Jan's entry I see that his translation of the interesting third chapter of Genzen's thesis--wherein Gentzen proved normalization of natural deduction derivations--is out in the next issue of the Bulletin.

Submitted by Richard Zach on Mon, 04/14/2008 - 3:09am

Submitted by Richard Zach on Sun, 04/13/2008 - 7:45pm

There's a very laudable enterprise: Blogging on Pseudoscience (at BPSDB.org) aggregates blog posts debunking or pointing out pseudo-scientific nonsense such as Intelligent Design. Lots of good stuff, PZ Meyers is part of it, etc. But, look at the logo they use:

Yes, that's a sequent calculus for linear logic. I know Girard has an idiosyncratic style, and that ludics paper may look a bit hokey. Probably only Girard can get a logic paper published in a respectable journal which contains quotes like this:

Jurassic logic keeps celebrating the wedding of Semantics and Syntax through the intercession of the Holy Meta, and, of course, every ritual deserves its own mockery, the Cross upside down, the Gospel in reverse order… In paralogics, there is no syntax, no semantics (or, better, the semantics is called syntax and vice versa). These mockeries, religious or logical, betray a paradoxical respect for a tradition that the protagonists never understood.

as well as pictures of skunks:

I mean, those two appendices are weird. But the proof theory is ok, isn't it? And there's nothing wrong with linear logic, is there?

Submitted by Richard Zach on Fri, 04/11/2008 - 2:10am

New SEP entry on Definitions by Anil Gupta.

Submitted by Richard Zach on Sun, 04/06/2008 - 4:36pm

Paolo's Stanford Encyclopedia entry on explanation in mathematics is online.

Submitted by Richard Zach on Thu, 04/03/2008 - 4:56pm

Ok, that was faster than I expected: The winners of the Kurt Gödel Centenary Research Fellowships have been announced. They are:

- David Fernández Duque (Stanford): Non-deterministic semantics for dynamic topological logic
- Pavel Hrubeš (Czech Academy of Sciences): On lengths of proofs in non-classical logics

- Andrey Bovykin (Steklov/Liverpool): Independence results in concrete mathematics
- Peter Koellner (Harvard): On reflection principles

- Thierry Coquand (Göteborg): Space of valuations

All great logicians, with great projects. Congratulations!

All applicants submitted papers on their research projects. Papers by the winners (and the finalists) will shortly appear in a special issue of the Annals. There will be a colloquium honoring the winners on April 27 (the eve of Kurtele's 101st birthday)

Submitted by Richard Zach on Thu, 04/03/2008 - 4:53pm

Hi, I promise to post something logic-related very soon. In the meantime, please enjoy this funny video:

[youtube=http://www.youtube.com/watch?v=Ahg6qcgoay4&hl=en]

Please look in the mirror before you open your car door!

Submitted by Richard Zach on Tue, 02/26/2008 - 9:24am

Shawn at Words and Other Things asks about good books on philosophy of logic. If you have suggestions, comment there, please.

Submitted by Richard Zach on Sat, 02/02/2008 - 5:19pm

Nice! Andrej Bauer has implemented the Hydra Game in a Java applet. The Hydra Game, like Goodstein sequences, is a way of coding ordinals ? ?_{0} ... hence they provide independence results from Peano Arithmetic. Andrej has all the deets. (A Java applet for Goodstein sequences is here.)

Submitted by Richard Zach on Mon, 01/28/2008 - 7:11pm

The finalists for the Kurt Gödel Centenary Research Prizes have been announced. They are:

- David Fernández: Non-Deterministic Semantics for Dynamic Topological Logic
- Ekaterina Fokina: Index Sets for Some Classes of Structures
- Pavel Hrubes: On lengths of proofs in non-classical logics
- Maryanthe Malliaris: Realization of phi-types and Keisler's order
- Kentaro Sato: The Strength of Extensionality - Weak Weak Set Theories with Infinity
- Henry Towsner: Ordinal Analysis by Transformations

- Andrey Bovykin: Independence results in concrete mathematics
- Vasco Brattka: A Computable Version of Banach's Inverse Mapping Theorem
- Andreas Fischer: O-minimal analytic separation of sets in dimension two
- Stefan Geschke: Low distortion embeddings of infinite metric spaces into the real line
- James Hirschorn: A strong antidiamond principle compatible with CH
- Peter Koellner: On Reflection Principles

- Jeremy Avigad: The metamathematics of ergodic theory
- Thierry Coquand: Space of valuations
- Fernando Ferreira: Injecting uniformities into Peano arithmetic
- Yuri Matiyasevich: Finite-fold Diophantine representations
- Andreas Weiermann: Phase transitions for Goedel incompleteness

Final decisions are expected April 9. The prizes will be awarded on Kurtele's birthday, April 28, in Vienna.

Submitted by Richard Zach on Mon, 01/28/2008 - 9:05am

John Burgess has a draft of a book on Philosophical Logic up on his website. It focusses on logics with direct philosophical relevance. It starts with temporal and modal logic, deals with conditional logics, "relevantistic" logics, and intuitionistic logic. It will be a relatively slim volume, but there's still a lot of interest in here: a nice little book. (HT: Kai von Fintel)