University of Calgary
UofC Navigation

All LogBlog Posts

New Blogs

Submitted by Richard Zach on Thu, 02/05/2009 - 6:35pm

I'm a bit late with this, but if you haven't heard, here are a couple of interesting new blogs:

Floridi Wins Barwise Prize

Submitted by Richard Zach on Thu, 02/05/2009 - 2:53am

Luciano Floridi has been awarded the Barwise Prize in philosophy of computing, given out annually by the APA.

Formalization Exercise

Submitted by Richard Zach on Wed, 01/14/2009 - 10:44pm

Logic I exercise: Formalize "Every day each of us says the dumbest thing we are going to say that day." Is it logically true?

"Computability" Deadline Approaching

Submitted by Richard Zach on Wed, 01/14/2009 - 4:04pm

The submission deadline for the July conference Computability in Europe is drawing near (Jan 20). I hope there will be at least a few papers on history and philosophy of computability--the PC chair tells me that so far there are none!

Arne Naess, 1912-2009

Submitted by Richard Zach on Tue, 01/13/2009 - 6:30pm

Arne Næss has died at the age of 96. He was the last surviving member of the "periphery" of the Vienna Circle.

Notice here.

More on Ciabattoni, Galatos, and Terui

Submitted by Richard Zach on Wed, 12/17/2008 - 9:03am

Here's a more detailed summary of the paper I just mentioned, (Ciabattoni, Galatos, and Terui, From axioms to analytic rules in nonclassical logics, LICS 2008) courtesy of Agata:

The paper contains a first step towards the definition of a general procedure to turn Hilbert axioms into analytic structural rules in various formalisms. The result is based on the substructural hierarchy — a new classification (Nn, Pn) of formulas of Full Lambek calculus with exchange (FLe) which is similar to the arithmetic hierarchy except that it tracks polarity alternations instead of quantification alternations.

The paper contains an algorithm which allows for the automated generation of a) analytic sequent structural rules equivalent to axioms up to the class N2 b) analytic hypersequent structural rules equivalent to axioms up to the class P3 (modulo a technical issue about weakening)

Given any axiom up to P3, the algorithm consists of the following two steps: 1. structural rules equivalent in power with the original axiom are generated and 2. they are afterwards completed (in the sense of Knuth-Bendix) in order to preserve cut-elimination once added to (the hypersequent version of) FLe.

Examples of axioms in N2 are ¬(A ? ¬A) or An ? Am, for arbitrary n, m, while e.g. (A ? B) ? (B ? A), ¬A ? ¬¬A are in P3.

In the same paper it was also shown that (single-conclusion) structural rules in sequent calculus can only capture properties (axioms) which already hold in intuitionistic logic and hence, e.g. to characterize (A ? B) ? (B ? A) hypersequents are needed.

The question of identifying the appropriate formalisms, beyond hypersequents, for dealing in a uniform way with axioms at levels higher than P3 is open.

If you know of related or similar work, please comment at the previous post.

Bleg: Systematic Approaches to Generation of Logical Calculi

Submitted by Richard Zach on Wed, 12/17/2008 - 8:31am

Over lunch the other day, my friend and colleague Agata Ciabattoni told me about her paper at this year's LICS, "From axioms to analytic rules in nonclassical logics". In it, she and her co-authors Nikolaos Galatos and Kazushige Terui present an intriguing and very general result: Suppose you have a logic which can be axiomatized in full Lambek calculus with exchange (that's intuitionistic logic without weakening or contraction, but with exchange) by adding axioms. If the additional axioms aren't too complex, there's a systematic way of generating an analytic hypersequent calculus for your logic, i.e., a systematic way of converting the additional axioms into a structural rule for a hypersequent calculus in such a way that cut is eliminable. This procedure applies to a wide range of substructural logics but also superintuitionistic logics. (UPDATE: more detail in the next post.) So that got us thinking: what other general, systematic approaches to generation of calculi are there? Agata's approach generates calculi of a specific form (hypersequent calculi) from other calculi (Hilbert-style calculi). Then I know of two approaches that systematically generate calculi from a semantics. Arnon Avron, Beata Konikowska, and Anna Zamansky have been doing a lot of work on logics given by what they call non-deterministic matrices. I wrote a while ago about the approach I detailed in my undergraduate thesis, which goes back to work by Rousseau in the 1960s: systematic (i.e., automatic) generation of sequent, tableaux, natural deduction calculi for a logic given by finite truth tables. These are the only systematic results I know of, but that just shows my ignorance! There must be others! I'm sure there are general results in modal correspondence theory, for instance, to obtain axioms and perhaps tableaux systems, etc., for modal logics from conditions on frames. Can anyone help me (and Agata) out here?

Paul Bernays at 120

Submitted by Richard Zach on Thu, 11/27/2008 - 1:16am

In addition to the new special issue celebrating the 50th anniversary of Gödel's Dialectica interpretation, Wiley-Blackwell has made the original Dialectica issue in which it appeared freely available. That issue itself was a Festschrift in honour of Paul Bernays's 70th birthday. (I'm sorry I'm late to herewith commemorate the 120th birthday of Bernays, who was born October 17, 1888.) The issue also includes the classics "Hilbert's programme" by Kreisel, "80 years of foundational studies" by Wang, and "Observation language and theoretical language" by Carnap, in addition to papers by Ackermann, Beth, Curry, Heyting, Fraenkel, Gonseth, Goodstein, Hermes, Péter, A. Robinson, Schütte, Schmidt, Skolem, and Specker.

The 50th Birthday of the Dialectica Interpretation

Submitted by Richard Zach on Tue, 11/18/2008 - 3:39am

Gödel's paper containing his so-called Dialectica interpretation was published 50 years ago in, well, Dialectica. And so Dialectica has a special issue on Gödel's Dialectica interpretation, edited by Thomas Strahm. It looks like all the articles are freely available. Here's (most of) the introduction:

Gödel's famous dialectica paper (1958), entitled 'Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes', was published in a special issue of this journal in 1958 in honour of Paul Bernays' 70th birthday. In the past fifty years, the dialectica interpretation proposed by Gödel has become one of the most fundamental conceptual tools in logic and the foundations of mathematics. This special issue traces some of the fundamental issues and applications of Gödel's interpretation. The ideas of Gödel'sdialectica interpretation date back at least as far as 1941, when Gödel presented them in a lecture to the mathematics and philosophy clubs at Yale University. The Yale lecture was entitled 'In What Sense is Intuitionistic Logic Constructive?' and can be found in Volume III of the Collected Works (1994). Prior to the Yale lecture, Gödel had delivered two addresses where he raised important thoughts towards the dialectica interpretation: an invited lecture given in 1933 in Cambridge, Massachusetts entitled 'The Present Situation in the Foundations of Mathematics' and an informal seminar in 1938 'Vortrag bei Zilsel' delivered in Vienna. The full history of the dialectica paper is presented by Feferman (1993) and Troelstra (1990).

Let us briefly summarize the main rationale of Gödel's dialectica interpretation. In its most elementary form, it provides an interpretation of intuitionistic number theory in a quantifier-free theory of functionals of finite type. Together with Gödel's double-negation interpretation from classical arithmetic into its intuitionistic counterpart, the dialectica interpretation also provides a reduction of classical arithmetic. Gödel's functional interpretation can be seen as a possible realization of the so-called modified Hilbert program in the sense that it enables a reduction of a classical system to a quantifier-free theory of functionals of finite type, thereby reducing the consistency problem for the classical theory to the consistency of a quantifier-free system of higher-type recursion, the latter being informally more finitistic and sufficiently well understood.

Gödel's interpretation of arithmetic has been substantially extended in the past fifty years both to stronger and weaker theories. In particular, versions of the dialectica interpretation have been proposed for impredicative classical analysis, subsystems of classical arithmetic, theories of ordinals, predicative subsystems of second order arithmetic, analysis with game quantifiers, systems of feasible arithmetic and analysis, admissible and constructive set theories, as well as iterated arithmetical fixed point theories. A comprehensive survey of many of these results can be found in Avigad and Feferman (1995) as well as Troelstra (1973). In more recent years, work on functional interpretations has shifted from purely foundational purposes to applications to concrete proofs in mathematics in the sense of Kreisel's unwinding program. In connection with this, Kohlenbach's proof mining program provides very impressive results making use of variants of Gödel's dialectica interpretation, see his article in this special issue.

Let us now give a brief survey of the articles contained in this special issue.

The paper by Justus Diller gives a broad survey of functional interpretations in the context of constructive set theories and elaborates in detail on the logical problems one has to solve in order to provide such interpretations of set theory. In addition, a new simplified interpretation, the so-called ?-interpretation, is proposed and analyzed. It is rooted in the Diller-Nahm interpretation of 1974.

Solomon Feferman's paper gives a vivid account of Gödel's views on finitism, constructivity and Hilbert's program, using unpublished articles and lectures as well as Gödel's correspondence with Paul Bernays. Feferman's article contains a full section on the dialectica interpretation and on Gödel's influential Cambridge lecture mentioned above.

Fernando Ferreira's article gives an informal analysis of Gödel's dialectica interpretation and presents a balanced mixture between philosophical discussions and technical issues. The paper starts off by a discussion of Gödel's use of higher types and the relationship to his set-theoretic realism. Further investigations of the paper include the validation of additional principles, higher order equality and monotone functional interpretations.

As already mentioned above, Ulrich Kohlenbach's article is centred on recent topics in applied proof theory and, in particular, his recent program of proof mining. His paper focuses on the logical aspects of his program and, in particular, on the systematic design and study of variants of the dialectica interpretation, which have been used in applications to concrete proofs from various areas of mathematics.

Finally, Paulo Oliva's article provides a detailed analysis of Gödel's dialectica interpretation via linear logic. The latter comes naturally into the picture of Gödel's interpretation, since contraction is the main source of its asymmetry. The paper analyses various properties of the dialectica interpretation, e.g. the characterization theorem, within the context of linear logic.

New SEP Entry: Bimbó on Combinatory Logic

Submitted by Richard Zach on Mon, 11/17/2008 - 6:11pm

Papers by Konrad Zdanowski

Submitted by Richard Zach on Mon, 11/17/2008 - 5:57pm

Via Theorem(e), I've come across the webpage of Konrad Zdanowski, a logician at the Polish Academy and Paris 7. His papers (mostly on arithmetic) all look incredibly interesting, he has lecture notes on Peano arithmetic, and there's also a paper on 2nd order intuitionistic propositional logic, which is somewhat related to my own research. If I only weren't so much behind in grading papers!

Tait, Cut-Elimination for Predicative Systems

Submitted by Richard Zach on Tue, 11/11/2008 - 5:10pm

Sitting in a talk at CMU by Bill Tait on cut elimnation for predicative systems. His approach, in contrast to Rathjen and Takeuti, is to try to get the cut-elimination proof to be mostly (or even, only) about the proofs, and not about proofs and (mostly) ordinal notation systems. He's using the original Tait calculus, in which formulas are all propositional, but infinitary. His cut-elimination theorem applies in all kinds of cases (essentially up through predicative arithmetic), which I hadn't realized before. But then I don't think the original paper actually emphasizes that. The main point in that regard is that when you translate axioms from a theory, you can assign the right kinds of ordinals.

Rick Statman made an interesting point, viz., that it's also important to verify that the infinitary derivations that you get when you translate derivations into Tait calculus are (primitive) recursively described, and that this is preserved when you eliminate the cuts--if this weren't the case, you wouldn't be able to carry out the cut-elimination proof in extensions of PRA.

Taxonomy for Logic and Philosophy of Mathematics

Submitted by Richard Zach on Fri, 11/07/2008 - 2:28pm

David Chalmers and David Bourget are setting up a new online resource for papers in philosophy, for which they're designing a taxonomy of philosophical topics to be used for classifying papers in the database. David asks

For now, I'm calling for feedback from the philosophical community, either via e-mail or via comments on this blog. Especially valuable will be thoughts on categories that we've missed, on ways to structure categories that don't yet have much structure, and on better ways of structuring things in tricky cases.

Please post responses at Dave's blog. The logic and philosophy of math part of the taxonomy right now looks like this:


Logic and Philosophy of Logic
Logics
Classical Logic
Aristotelian Logic
Propositional Logic
Predicate Logic
Deontic Logic
Epistemic Logics
Doxastic and Epistemic Logic
Inductive Logic
Nonmonotonic Logic
Higher-Order Logics
Second-Order Logic
Higher-Order Logics, Misc
Modal and Intensional Logic
Intensional Modal Logic
Modal Logic
Provability Logics
Quantified Modal Logic
Semantics for Modal Logic
Nonclassical Logics
Fuzzy Logics
Infinitary Logics
Intuitionistic Logic
Many-Valued Logics
Paraconsistent Logics
Quantum Logic
Relevance Logics
Substructural Logics
Temporal Logic
Logics, Misc
Logical Pluralism
Logical Consequence and Entailment
Logical Expressions
Logical Constants
Logical Connectives
Quantifiers*
Variables
Logical Paradoxes
Sorites Paradox*
Liar Paradox
Russell's Paradox*
Logical Semantics and Logical Truth
Model Theory and Proof Theory
Philosophy of Logic, Misc
Dialetheism
Epistemology of Logic
Informal Logic
Logical Pluralism
Logic in Philosophy

Philosophy of Mathematics
Epistemology of Mathematics
Apriority in Mathematics
Epistemology of Mathematics, Misc
Mathematics and the Causal Theory of Knowledge
Mathematical Intuition
Mathematical Proof
Godel's Theorem
Computer Proof
Probabilistic Proof
Undecidability
Mathematical Proof, Misc
Revisability in Mathematics
Mathematical Objects
Fictionalism
Indeterminacy
Nominalism
Platonism
Structuralism
Neo-Fregean Approaches
Indispensability Arguments
Numbers
The Nature of Sets*
Mathematical Truth
Analyticity in Mathematics
Axiomatic Truth
Objectivity Of Mathematics
Philosophy of Set Theory
The Nature of Sets
The Iterative Conception of Set
Ontology of Sets
Axioms of Set Theory
Axiomatic Truth*
The Axiom of Choice
The Axiom of Constructibility
The Axiom of Determinacy
The Axiom of Infinity
New Axioms
Independence Results
Cardinals and Ordinals
The Continuum Hypothesis
Large Cardinals
Set Theory as a Foundation
Russell's Paradox
Set Theory and Logicism
Set-Theoretic Constructions
Areas of Mathematics
Algebra
Analysis
Category Theory
Geometry
Logic*
Number Theory
Topology
Theories of Mathematics
Logicism
Formalism
Intuitionism and Constructivism
Predicativism
Mathematical Naturalism
Philosophy of Mathematics, Misc
Explanation in Mathematics
The Infinite
The Application of Mathematics

Logic in the M&E part of the taxonomy:

Metaphysics and Epistemology
Philosophy of Language
Specific Expressions
Conditionals
Truth-Conditional Accounts of Indicative Conditionals
Epistemic Accounts of Indicative Conditionals
Pragmatic Accounts of Indicative Conditionals
Indicative Conditionals and Conditional Probabilities
Indicative Conditionals, Misc
Counterfactuals and Possible Worlds
Subjunctive Conditionals, Misc
Conditionals, Misc
Truth and Vagueness
Theories of Truth
Coherence Theory of Truth
Correspondence Theory of Truth
Minimalism and Deflationism about Truth
Pragmatism about Truth
Tarskian Theories of Truth
Theories of Truth, Misc
Truth, Misc
Relativism about Truth
Truth Bearers
Truth and Justification
Truthmakers*
The Liar Paradox
Theories of Vagueness
Contextual Theories of Vagueness
Degree-Theoretic Theories of Vagueness
Epistemic Theories of Vagueness
Incoherentism about Vagueness
Nihilism about Vagueness
Many-Valued Logic
Supervaluationism
Theories of Vagueness, Misc
Vagueness, Misc
Higher-Order Vagueness
Vague Objects*
Vagueness in Ethics and the Law

C. B. Martin, 1924-2008

Submitted by Richard Zach on Tue, 10/28/2008 - 4:17pm

My former colleague C. B. Martin died last Thursday.

Obituary here.

C. B. Martin, 1924-2008

Submitted by Richard Zach on Tue, 10/28/2008 - 4:17pm

My former colleague Charlie Martin died last Thursday. He was a major figure in metaphysics, one of the first to talk about truthmakers.

Obituaries here and here.

Theoria Online (Including Back Issues!)

Submitted by Richard Zach on Tue, 10/21/2008 - 3:00pm

The venerable Swedish philosophy journal Theoria is published by Blackwell since this past March, and that means it is online, including the back issues. I'm not sure of the exact dates, but in the 70s, when Krister Segerberg was the editor-in-chief of that journal, Theoria was the place to publish modal logic and formal philosophy. Just go and browse the back issues, lots of interesting stuff there!

(The latest issue has a new paper by Kripke.)

Tarski on Gödel's Theorem and the Deductive Method

Submitted by Richard Zach on Fri, 10/17/2008 - 4:09pm

One very common informal statement of Gödel's theorem is that it shows that for any (sufficiently strong consistent blah blah) formal system, there are truths that it can't prove. And if you don't formulate Gödel's incompleteness theorem that way, at least you state this as a corollary: Gödel's theorem shows that truth and provability (in any one formal system) come apart. But if you read Gödel''s original paper(s) on incompleteness, you are probably struck by the fact that Gödel doesn't say this. In fact, the word "wahr" doesn't even appear in Gödel's 1931 paper. I think Gödel doesn't note this consequence until the 1934 Princeton lectures (p. 363 of Collected Works I). A number of reasons have been offered for this: a) he was reacting against Hilbert, so he wanted to keep everything purely finitary, b) he was working in the context of the Vienna Circle, and they considered "truth" to be a suspect, metaphysical notion. This is an aspect that people interested in Gödel's platonism have written extensively about, since Gödel claimed that even at the time of writing the 1931 paper he was a platonist.

So who was the first to note this consequence in print? My money is on the guy who made truth respectable among the logical empiricists. Here's the end of Tarski's "Einige Betrachtungen über die Begriffe der ?-Widerspruchsfreiheit und der ?-Vollständigkeit", Monatshefte für Mathematik und Physik 40 (1933) 97-112 (the paper was received in July 1932), translated as "Some observations on the concepts of ?-completeness and ?-consistency", Logic, Semantics, Metamathematics, 2nd ed., pp. 279-295:

[T]he following is worthy of emphasis: the profound analysis of Gödel's investigations shows that whenever we have undertaken a sharpening of the rules of inference, the facts, for the sake of which this sharpening was felt to be necessary, still persist, although in a more complicated logical structure. The formalized concept of consequence will, in extension, never coincide with the ordinary one, the consistency of that system will not prevent the possibility of 'structural falsehood'. However liberally we interpret the concept of the deductive method, its essential feature has always been (at least hitherto) that in the construction of the system and in particular in the formulation of its rules of inference, use is made exclusively of general logical and structurally descriptive concepts. If now we wish to regard as the ideal of deductive science the construction of a system in which all the true statements (of the given language) and only such are contained, then this ideal unfortunately cannot be combined with the above view of the deductive method.

Now here's something puzzling. The translation has a footnote to this passage which is not in the original:

The validity of the remarks stated in the last paragraph essentially depends on the decision not to use in metamathematical discussion any devices which cannot be formalized within the framework of the theory of types of Principia Mathematica. But as soon as we abandon this decision and allow ourselves to use stronger devices in metamathematical discussion, most of the remarks as originally formulated lose their validity and the whole paragraph requires a thorough revision.

What in the passage quoted depends for its validity on metamathematics being formalizable in PM? Maybe that if the metatheory is stronger than PM, you can define a "formalized notion of consequence" which characterizes the true statements of PM, e.g., using an ? rule. But Tarski just did that immediately before the quoted passage and says that the resulting formalized notion of consequence is not "in harmony with the current view of the deductive method". So what can he have in mind here?

Zeno's Paradox at Dinosaur Comics

Submitted by Richard Zach on Fri, 10/17/2008 - 2:47pm

Today's Dinosaur Comics was written by xkcd's Randall Munroe:


Ryan North, the author of Dinosaur Comics, has used philosophical/logical themes in his comic as well, e.g., the Twin Earth comic, or the Post Hoc Ergo Propter Hoc comic, or the one on pragmatism. This one is pretty funny, too.

Of course, you've all seen the xkcd comic on Gödel and Russell's Paradox.

New Modal Logic Books

Submitted by Richard Zach on Fri, 10/17/2008 - 2:06am

Update on my old post on modal logic textbooks: Two new modal logic books I have recently come across:

Anyone already read these and have an opinion? The Carnielli/Pizzi text looks especially interesting--and the full text is available online! (Not free, of course. It's Springer, after all.)

I also noticed that a few classic books/collections of classical papers on modality are now online at Oxford Scholarship Online, including:

Carnap Reception at PSA

Submitted by Richard Zach on Thu, 10/16/2008 - 6:35am

If you're going to be in Pittsburgh (at the PSA) in three weeks, please come to the Carnap Reception that Open Court is going to throw on Friday, Nov 7. I think it'll be at 5:30. Vol. 1 of Carnap's Collected Works will be presented. I expect there will be free drinks, too!

Pages