Epistemology Job at Calgary

We’re looking for an epistemologist:

The Department of Philosophy at the University of Calgary invites applications for a tenure-track position at the rank of Assistant Professor. The position will commence, subject to budgetary approval, on July 1, 2006. A PhD or equivalent, and a strong research and teaching record are required.

The area of specialization for this position is epistemology. Areas of competence should include logic and philosophy of science.

The successful candidate will develop and co-ordinate a university course on the nature of evidence. This will be a broad based course covering a range of areas including logic, scientific method, and moral and legal reasoning, and it will use teaching resources from various faculties in the university. The succesful candidate will also have research interests that fit this teaching responsibility.

Deadline is November 25, see the full job ad.

That course on “evidence” is actually going to be taught as a pilot by Dennis McKerlie and myself next term, and we got a grant to play with incorporating blogs and wikis into the course. I’ll let y’all know how it goes.

I have a previous post about taking a job in canada which you might want to look at.


This is scary. Apparently someone in the next building over received a mystery envelope containing a white powder. When I got to campus there were police and hazmat people all over the place:

At 11:30 a.m. today the Bio Sciences building was evacuated as a precaution due to a concern involving an envelope sent to an office in that building. Since that time another envelope has been discovered in the same office and we are now in the process of investigating whether or not these packages pose any harm.

Please be on the alert that if you receive an envelope or package with no return address or a return address of anyone you do not recognize or in particular has a return address of North York, Ontario DO NOT OPEN the envelope.

Many-sided Sequent Calculi and Many-valued Logics

Since Greg asked, I thought I’d give a brief survey of many-sided sequent calculi. The basic idea is simple and quite old (the first paper on it, by Kurt Schröter, is from 1955 [8]; the most detailed early papers is [6]). In the standard semantics for classical sequents, Γ ⇒ Δ means that either one of the formulas in Γ is false or one of the formulas in Δ is true. Now if you have more than the truth values true and false, say, a set of truth values V = {v1, … vn}, you can analogously introduce an n-sided sequent Γ1 | … | Γn which means “for some i between 1 and n, and some A ∈ Γi, A has value vi.”

Once you’ve generalized the sequent notation and its semantics, you can also generalize the other usual stuff: introduction rules for connectives and quantifiers for the i-th position, n-sided axiom sequents, cut rules; based on more or less the same idea you can also get many-sided natural deduction [3] and clause transformation calculi for many-valued resolution. If you do it right, you also get soundness, completeness, cut elimination, Maehara lemma, midsequent theorem, jadda jadda jadda. The neat thing is that the process of constructing the sequent calculus can be completely automatized. In fact, the MUltlog system [5] lets you enter the truth tables for connectives and quantifiers of your n-valued logic L, and out comes a paper about sequent calculus and resolution for L (e.g., here’s a paper about 3-valued Gödel logic). Exercise: try it out with Belnap’s 4-valued bilattice logic (aka FDE; solution in [4]).

I worked out the details of this approach to proof-theory of finite-valued logics in excruciating detail in my undergraduate thesis, imaginatively entitled Proof Theory of Finite-valued Logics [9], but much if not most of the credit goes to my supervisor Matthias Baaz and colleagues at the TU Vienna, Chris Fermüller and Gernot Salzer. Gernot is mainly responsible for implementing MUltlog, and its companion MUltseq, a propositional finite-valued resolution prover (the latter jointly with Angel Gil). The thesis works out the calculi for the interpretation above, and also for its dual interpretation where Γ1 | … | Γn means “for some i between 1 and n, and some A ∈ Γi, A does not have value vi.” (In other words, such a sequent is valid if no interpretation makes every A ∈ Γi have value vi.) This also generalizes the two-valued case (if you switch left and right side).

The four of us also generalized the approach to sequent calculi with arbitrary labels (instead of sides) in [2]: so instead of having a label for each truth-value, e.g., you can have a label for every subset of the set of truth values, or labels for every set of truth values but one (the dual interpretation mentioned above), etc. We showed that every finite-valued logic can be given a labelled sequent calculus which is sound and complete and enjoys cut elimination for certain sets of subsets of V as labels. In fact, we showed a converse to that as well: under suitable conditions, any labelled sequent calculus which enjoys cut-elimination and has all structural rules can be given a finite-valued semantics.

All these calculi have weakening and contraction, so there’s still room for more work (e.g., for Greg): generalize all this to substructural logics. Chris and Matthias have a paper [1] on finite-valued intuitionistic calculi (i.e., many-sided sequents, but some sides restricted to only one formula).


  1. Matthias Baaz, Christian G. Fermüller, Intuitionistic Counterparts of Finitely-Valued Logics.
    In: 26th International Symposium on Multiple-valued Logic (IEEE Press, Los Alamitos, 1996), pp. 136–143
  2. Matthias Baaz, Christian G. Fermüller, Gernot Salzer, Richard Zach, Labeled calculi and finite-valued logics, Studia Logica 61 (1998) 7–33
  3. Matthias Baaz, Christian G. Fermüller, Richard Zach, Systematic construction of natural deduction systems for many-valued logics, 23rd International Symposium on Multiple Valued Logic. Sacramento. (IEEE Press, Los Alamitos, 1993) 208–213
  4. Matthias Baaz, Christian G. Fermüller, Richard Zach, Elimination of cuts in first-order many-valued logics, Journal of Information Processing and Cybernetics 29 (1994) 333–355
  5. Matthias Baaz, Christian G. Fermüller, Gernot Salzer, Richard Zach, MUltlog 1.0: towards an expert system for many-valued logics. International Conference on Automated Deduction (CADE’96), LNCS (LNAI) 1104, (Springer, 1996) 226-230.
  6. G. Rousseau, Sequents in many-valued logic I. Fundamenta Mathematicae 60 (1966) 23-33. Errata 61 (1967), 313.
  7. G. Rousseau, Sequents in many-valued logic II. Fundamenta Mathematicae 67 (1970) 125-131.
  8. Karl Schröter. Methoden zur Axiomatisierung beliebiger Aussagen- und
    Prädikatenkalküle. Zeitschrift für mathematische Logik und Grundlagen der Mathematik 1 (1955) 241-251.
  9. Richard Zach, Proof Theory of Finite-Valued Logics, Diploma Thesis, Technische Universität Wien, Vienna, 1993
  10. MUltlog homepage: http://www.logic.at/multlog/

Caldon and Ignjatović on Mathematical Instrumentalism

The most recent issue of The Journal of Symbolic Logic contains the long-awaited (well, by me) article on “On mathematical instrumentalism” by Patrick Caldon and Aleks Ignjatović. It presents the results from Chapters 2 and 3 of Aleks’s excellent 1990 Berkeley PhD thesis. Here is the abstract:

In this paper we devise some technical tools for dealing with problems connected with the philosophical view usually called mathematical instrumentalism. These tools are interesting in their own right, independently of their philosophical consequences. For example, we show that even though the fragment of Peano’s Arithmetic known as IΣ1 is a conservative extension of the equational theory of Primitive Recursive Arithmetic (PRA), IΣ1 has a super-exponential speed-up over PRA. On the other hand, theories studied in the Program of Reverse Mathematics that formalize powerful mathematical principles have only polynomial speed-up over IΣ1.

The material from Chapter 4 of the thesis appeared in 1994 also in the JSL: “Hilbert’s program and the omega-rule“. Here’s what’s in that paper:

In the first part of this paper we discuss some aspects of Detlefsen’s attempt to save Hilbert’s Program from the consequences of Godel’s Second Incompleteness Theorem. His arguments are based on his interpretation of the long standing and well-known controversy on what, exactly, finitistic means are. In his paper [1] Detlefsen takes the position that there is a form of the ω-rule which is a finitistically valid means of proof, sufficient to prove the consistency of elementary number theory Z. On the other hand, he claims that Z with its first-order logic is not strong enough to allow a formalization of such an ω-rule. This would explain why the unprovability of Con(Z) in Z does not imply that the consistency of Z cannot be proved by finitistic means. We show that Detlefsen’s proposal is unacceptable as originally formulated in [1], but that a reasonable modification of the rule he suggest leads to a partial program already studied for many years. We investigate the scope of such a program in terms of proof-theoretic reducibilities. We also show that this partial program encompasses mathematically important theories studied in the “Reverse Mathematics” program. In order to investigate the provability with such a modified rule, we define new consistency and provability predicates which are weaker than the usual ones. We then investigate their properties, including a few that have no apparent philosophical significance but compare interestingly with the properties of the program based on the iteration of our ω-rule. We determine some of the limitations of such programs, pointing out that these limitations partly explain why partial programs that have been successfully carried out use quite different and substantially more radical extensions of finitistic methods with more general forms of restricted reasoning.

Together, these papers contain some of the most interesting recent technical results about Hilbert’s program and mathematical instrumentalism of the sort put forward by Mic Detlefsen.

Synthese special issue on Frege and Hilbert

The October issue of Synthese, edited by Bernd Buldt, Volker Halbach, and Reinhard Kahle, contains a bunch of exciting papers on Frege and Hilbert:

  • Amending Frege’s Grundgesetze der Arithmetik, by Fernando Ferreira
  • Real numbers and set theory – Extending the Neo-Fregean Programme Beyond Arithmetic, by Bob Hale
  • Frege’s permutation argument revisited , by Kai Wehmeier and Peter Schroeder-Heister
  • Problems and riddles: Hilbert and the du Bois-Reymonds, by D. C. McCarty
  • The constructive Hilbert Program and the limits of Martin-Löf Type Theory, by Michael Rathjen
  • Dedekind’s analysis of number: systems and axioms, by Wilfried Sieg and Dirk Schlimm
  • Against Against Intuitionism, by Dirk Schlimm