Desktop version

Home arrow Philosophy arrow Advances in Proof-Theoretic Semantics

Conclusions and Further Work

In this paper we have argued for two central claims: (1) that the apparent consensus that the Kreisel-Goodman paradox is engendered by the adoption of Kreisel's second clause interpretations of →, ¬ and ∀ is mistaken; and (2) that the ability of a formal system to internalize reasoning about its own proofs plays a larger role in the paradox than is customarily acknowledged. Taken in conjunction, these observations point towards the possibility of responding to the paradox by developing a system which retains as many of the features of the unstratified theory T + as possible while seeking a conceptually motivated means of limiting the scope of the internalization principle Int.

The evident question is what form such a delimitation might take. Taken together with the observations we have recorded about the role of free variables and reflection principles in the paradox, one obvious proposal would be to consider subsystems of formalisms similar to QLP in which the scope of Lift is limited by the exclusion of quantifier or substitution rules akin to Eug. Although such a proposal may be justifiable in terms of Kreisel and Goodman's original foundational goals, a variety of questions remain open: (i) is a consistency proof similar to that described by Goodman [16] available for an appropriate subsystem of T +? (ii) is it possible to prove the soundness and completeness of HPC in the sense of Val for such a system?

(iii) are the second clause interpretations of the intuitionistic connectives required for such a result? (iv) is it possible to formulate a version of Goodman's interpretation of Heyting arithmetic relative to the relevant system? Needless to say, these questions will have to wait for another occasion.

References

1. Artemov, S.N.: Explicit provability and constructive semantics. Bull. Symb. Log. 7(1), 1–36 (2001)

2. Barendregt, H.P.: The Lambda Calculus. North Holland, Amsterdam (1984)

3. Beeson, M.: Foundations of Constructive Mathematics: Metamathematical Studies. Springer, Berlin (1985)

4. Benacerraf, P.: Mathematical truth. J. Philos. 70(19), 661–679 (1973)

5. Dean, W.: Montague's paradox, informal provability, and explicit modal logic. Notre Dame J. Form. Log. 55(2), 157–196 (2014)

6. Dean, W., Kurokawa, H.: The paradox of the Knower revisited. Ann. Pure Appl. Log. 165(1),

199–224 (2014)

7. Dummett, M.: Elements of Intuitionism. Oxford University Press, Oxford (2000)

8. Feferman, S. et al. (eds.): Kurt Gödel Collected Works. Unpublished Lectures and Essays, vol.

III. Oxford University Press, Oxford (1995)

9. Fitting, M.: A quantified logic of evidence. Ann. Pure Appl. Log. 152(1–3), 67–83 (2008)

10. Fletcher, P.: Truth, Proof and Infinity: A Theory of Constructive Reasoning. Kluwer, Dordrecht (1998)

11. Gentzen, G.: The Collected Papers of Gerhard Gentzen. Studies in Logic and the Foundations

of Mathematics. North-Holland, Amsterdam (1969)

12. Girard, J., Lafont, Y., Taylor, P.: Proofs and Types. Cambridge University Press, Cambridge (1989)

13. Gödel, K.: The present situation in the foundations of mathematics. In: Feferman et al. [8], pp.

36–53 (1933)

14. Gödel, K.: Lecture at Zilsel's. In: Feferman et al. [8], pp. 62–113 (1938)

15. Gödel, K.: An interpretation of the intuitionistic propositional calculus. In: Feferman, S., et al. (eds.) Kurt Gödel Collected Works, vol. I. Publications 1929–1936, pp. 301–303. Oxford University Press, Oxford (1986)

16. Goodman, N.: Intuitionistic arithmetic as a theory of constructions. Ph.D. thesis, Stanford

(1968)

17. Goodman, N.: A theory of constructions equivalent to arithmetic. In: Kino, J.M.A., Vesley, R. (eds.) Intuitionism and Proof Theory, pp. 101–120. Elsevier, Amsterdam (1970)

18. Goodman, N.: The arithmetic theory of constructions. Cambridge Summer School in Mathe-

matical Logic, pp. 274–298. Springer, Berlin (1973)

19. Heyting, A.: Die formalen Regeln der intuitionistischen Mathematik II. Sitzungsberichte der Preussischen Akademie der Wissenschaften, pp. 57–71 (1930)

20. Heyting, A.: Mathematische Grundlagenforschung: Intuitionismus. Springer, Beweistheorie

(1934)

21. Heyting, A.: Intuitionism. An Introduction. North-Holland, Amsterdam (1956)

22. Hindley, J.R., Seldin, J.P.: Introduction or Combinators and Lambda Calculus, London Mathematical Society Student Texts, vol. 1. Cambridge University Press, Cambridge (1986)

23. Kaplan, D., Montague, R.: A paradox regained. Notre Dame J. Form. Log. 1(3), 79–90 (1960)

24. Kolmogorov, A.: Zur Deutung der intuitionistischen Logik. Mathematische Zeitschrift 35(1), 58–65 (1932)

25. Kreisel, G.: Foundations of intuitionistic logic. In: Nagel, E., Suppes, P., Tarski, A. (eds.) Logic,

Methodology and Philosophy of Science, Proceedings of the 1960 International Congress, pp. 198–210. Stanford University Press, Stanford (1962)

26. Kreisel, G.: Mathematical logic. In: Saaty, T. (ed.) Lectures on Modern Mathematics, vol. III. Wiley, New York (1965)

27. Kreisel, G., Newman, M.H.A.: Luitzen Egbertus Jan Brouwer. 1881–1966. Biogr. Mem. Fellows R. Soc. 15, 39–68 (1969)

28. Martin-Löf, P.: A theory of types. Technical report, pp. 71–3, University of Stockholm (1971)

29. Martin-Löf, P.: Intuitionistic Type Theory. Bibliopolis, Naples (1984)

30. Martin-Löf, P.: An intuitionistic theory of types. In: Sambin, G., Smith, J.M. (eds.) Twenty Five Years of Constructive Type Theory. Clarendon Press, Oxford (1998)

31. McCarty, C.: Intuitionism: an introduction to a seminar. J. Philos. Log. 12(2), 105–149 (1983)

32. McCarty, C.: Constructive validity is nonarithmetic. J. Symb. Log. 53(4), 1036–1041 (1988)

33. Montague, R.: Syntactical treatments of modality, with corollaries on reflexion principles and finite axiomatizability. Acta Philos. Fenn. 16, 153–167 (1963)

34. Myhill, J.: Some remarks on the notion of proof. J. Philos. 57, 461–471 (1960)

35. Prawitz, D.: Meaning and proofs: on the conflict between classical and intuitionistic logic.

Theoria 43(1), 2–40 (1977)

36. Russell, B.: The Principles of Mathematics. Cambridge University Press, Cambridge (1903)

37. Scott, D.: Constructive validity. Symposium on Automatic Demonstration, pp. 237–275.

Springer, Berlin (1970)

38. Sørensen, M.H., Urzyczyn, P.: Lectures on the Curry-Howard Isomorphism. Elsevier Science, Philadelphia (2006)

39. Sundholm, G.: Constructions, proofs and the meaning of logical constants. J. Philos. Log.

12(2), 151–172 (1983)

40. Sundholm, G.: Demonstrations versus proofs, being an afterword to constructions, proofs, and the meaning of the logical constants. In: der Schaar, M. (ed.) Judgement and the Epistemic Foundation of Logic, pp. 15–22. Springer, Berlin (2013)

41. Tait, W.W.: Gödel's interpretation of intuitionism. Philos. Math. 14(2), 208–228 (2006)

42. Tarski, A.: The concept of truth in formalized languages. Logic. Semantics, Metamathematics, vol. 2, pp. 152–278. Clarendon Press, Oxford (1956)

43. Troelstra, A.S.: Principles of Intuitionism. Lecture Notes in Mathematics, vol. 95. Springer, Berlin (1969)

44. Troelstra, A.S.: Aspects of constructive mathematics. In: Barwise, J. (ed.) Handbook of Mathematical Logic, vol. 90, pp. 973–1052. Elsevier, Amsterdam (1977)

45. Troelstra, A.S.: The interplay between logic and mathematics: intuitionism. In: Agazzi, E. (ed.) Modern Logic—A Survey: Historical, Philosophical, and Mathematical Aspects of Modern Logic and Its Applications. Synthese Library, vol. 149, pp. 197–221. Reidel, Dordrecht (1980)

46. Troelstra, A.S., van Dalen, D.: Constructivism in Mathematics, An Introduction, vol. 1. NorthHolland, Amsterdam (1988)

47. van Atten, M.: The development of intuitionistic logic. In: Zalta, E.N. (ed.) The Stanford Encyclopedia of Philosophy (2009)

48. van Dalen, D.: Lectures on intuitionism. Cambridge Summer School in Mathematical Logic, pp. 1–94. Springer, Berlin (1973)

49. Weinstein, S.: The intended interpretation of intuitionistic logic. J. Philos. Log. 12(2), 261–270 (1983)

50. Zermelo, E.: Über Grenzzahlen und Mengenbereiche: Neue Untersuchungen über die Grundlagen der Mengenlehre. In: Ebbinghaus, H., Kanamori, A. (eds.) Ernst Zermelo—Collected Works, pp. 390–429. Springer, Berlin (2010)

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