Desktop version

Home arrow Philosophy arrow Advances in Proof-Theoretic Semantics


Theorem Let F and G be sentential formulas such that the inference from F to G is not intuitionistically valid. Then there are instances Fand Gof F and G, a set S of boundary rules, and a set α of atomic sentences such that α f-S Fbut not α f-S G∗.

Proof Let Σ be the set of atomic sentences occurring in F or in G. Since the inference from F to G is not intuitionistically valid, there is a Kripke tree (W,, I ) with root w such that (W,, I ) Fw F but not (W,, I ) Fw G. Here (W,) is a tree (we take the root as being at the bottom), and I is a mapping from W to subsets of Σ : for each uW , I (u) is the set of atomic sentences true at u. I is subject to the constraint that if uv then I (u)I (v). We wish to obtain sets of atomic sentences that “mimic” (W,, I ). For this we shall need additional atomic sentences for there may be distinct nodes in W making the same atomic sentences of Σ true, but to these nodes we want to have correspond distinct sets of atomic sentences. For each u in W let u∗ be a distinct atomic sentence not in Σ , and for each u in W let ϕ(u) = {v∗ | vW and vu}. ϕ(u) will be the set of atomic sentences corresponding to the node u. We now so formulate boundary rules that the only Sclosed sets that do not contain ⊥ are precisely the sets ϕ(u) for uW . In fact, let S be the following set of boundary rules:

“Infer ⊥ from A1,..., An whenever { A1,..., An } ⊆ ϕ(u) for no uW ; ” “Infer v∗ from u∗ whenever u, vW and v < u.

Now, for each pΣ , let D( p) be the disjunction of all atomic sentences u∗ such that p is in I (u). Finally, for any sentence H constructed from members of Σ , let H ∗ be obtained from H by replacing each atomic sentence p with D( p).

It is a routine matter to show by induction on the construction of formulas that, for any H and any uW , (W,, I ) Fu H iff ϕ(u) f-S H ∗. It then follows from the supposition that ϕ(u) f-S F ∗ but not ϕ(u) f-S G∗, so that the inference from F ∗ to G∗ is not valid, in the revised sense. D

Author's Postscript, January 2015

From 1999 to 2007 I presented this paper at various universities and conferences. Often audience members raised stimulating points, particularly about my suggestions in Sect. 4, which I hoped to address in an expanded version, but I never managed to do so to my satisfaction. However, the basic issues still seem to me to be well-framed in the original version that is printed here.

The last presentation I gave was in September 2007 at the Oxford philosophy of mathematics seminar led by Daniel Isaacson. I was delighted that Michael Dummett was able to attend, despite infirmities of age. (Sir Michael and I had been on warm terms since his spring semester 1976 residence at Harvard, when he delivered the William James Lectures from which The Logical Basis of Metaphysics [3] evolved, and I was in my first year on the Harvard faculty.) It was particularly pleasing that at the 2007 seminar one of the younger Oxford philosophers, Ofra Magidor, raised the same objection that Sir Michael had framed nine years earlier in a letter to me, namely that Counterexamples 1 and 2 (from Sect. 1) are really not worrisome at all. In his 1998 letter he wrote, “I do not accept that your counter-examples are genuinely such.” His point and Magidor's was that if G and F have no atomic sentences in

common, and F has no occurrences of ⊥, then the only reason to assert FG

would be that one had independent reason for thinking that F were false or G were true, and since the former is ruled out by F not containing ⊥, it isn't at all surprising that we can infer G.

However this point seems to me mistaken: for if the rule (infer G from FG, when F does not contain ⊥ and G and F contain no atomic parts in common) is justified, it is justified in application not just to assertions but also to suppositions. On the ordinary understanding of what it is to suppose FG, this is simply untenable. So if the rule is to be accepted, it would have to be argued that the ordinary understanding of supposition is incorrect, and in fact to suppose FG is to suppose something like “every canonical argument for F can be transformed into a canonical argument for G”. But this is clearly wrong if F and G are empirical. (It might be maintained for mathematical F and G, but in this case it would again appear that a bias in favor of intuitionistic logic were being built in at the ground level.)

Even though I was criticizing his position, Sir Michael clearly enjoyed my presentation at the seminar, no doubt because he thought the issues needed more discussion. Despite his infirmities, he maintained his famously cheerful humour as well as his robust sense of what philosophy could aspire to do. I dedicate this publication to his memory.


1. Dummett, M.: The Justification of Deduction. Oxford University Press, Oxford (1974). Reprinted in M. Dummett, Truth and Other Enigmas, Duckworth, London (1978), 290–318

2. Dummett, M.: Elements of Intuitionism. Oxford University Press, Oxford (1977)

3. Dummett, M.: The Logical Basis of Metaphysics. Harvard University Press, Cambridge (1991)

4. Dummett, M.: Frege: Philosophy of Language, 2nd edn. Harvard University Press, Cambridge (1993)

5. Frege, G.: Collected Papers on Mathematics, Logic and Philosophy. Basil Blackwell, New York.

Translated by M. Black, V. Dudman, P. Geach, H. Kaal, E.-H.W. Kluge, B. McGuinness & R.H. Stoothoff(1984)

6. Gentzen, G.: Untersuchungen über das logische Schließen. Mathematische Zeitschrift 39, 176– 210, 405–431 (1934/35). Translated in M.E. Szabo (ed.), The Collected Papers of Gerhard Gentian, 68–131. North-Holland, Amsterdam (1969)

7. Prawitz, D.: Towards a foundation of a general proof theory. In: Suppes, P., Henkin, L., et al. (eds.) Logic, Methodology, and Philosophy of Science IV, 225–250. North-Holland, Amsterdam (1973)

Found a mistake? Please highlight the word and press Shift + Enter  
< Prev   CONTENTS   Next >

Related topics