Springer Nature is making SARS-CoV-2 and COVID-19 research free. View research | View latest news | Sign up for updates

Propositions as games as types

  • 66 Accesses

  • 17 Citations


Without violating the spirit of Game-Theoretical semantics, its results can be re-worked in Martin-Löf's Constructive Type Theory by interpreting games as types of Myself's winning strategies. The philosophical ideas behind Game-Theoretical Semantics in fact highly recommend restricting strategies to effective ones, which is the only controversial step in our interpretation. What is gained, then, is a direct connection between linguistic semantics and computer programming.

This is a preview of subscription content, log in to check access.


  1. Dummett, Michael: 1973,Frege: Philosophy of Language, Duckworth, London.

  2. Dummett, Michael: 1976, ‘What Is a Theory of Meaning’, in G. Evans and J. McDowell (eds.),Truth and Meaning, Oxford University Press, Oxford, pp. 67–137.

  3. Dummett, Michael: 1978,Truth and Other Enigmas, Duckworth, London.

  4. Gödel, Kurt: 1958, ‘Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes’,Dialectica 12 (1958), 280–87.

  5. Hintikka, Jaakko: 1979, ‘Language Games’, in Saarinen (1979), pp. 1–26.

  6. Hintikka, Jaakko and Lauri Carlson: 1979, ‘Conditionals, Generic Quantifiers, and Other Applications of Subgames, in Saarinen (1979), pp. 179–214.

  7. Hintikka, Jaakko and Jack Kulas: 1983,The Game of Language, D. Reidel, Dordrecht.

  8. Martin-Löf, Per: 1982, ‘Constructive Mathematics and Computer Programming’, in Cohen, Los, Pfeiffer, and Podewski (eds.),Logic, Methodology and Philosophy of Science VI, North-Holland, Amsterdam, pp. 153–75.

  9. Martin-Löf, Per: 1983, ‘On the Meanings of the Logical Constants and the Justifications of the Logical Laws’, lectures held at the meetingTeoria della dimostrazione e filosofia della logica in Siena, April 6–9th, 1983.

  10. Martin-Löf, Per: 1984,Intuitionistic Type Theory, notes by Giovanni Sambin of a series of lectures given in Padua, June 1980, Bibliopolis, Naples.

  11. Pagin, Peter: 1987,Ideas for a Theory of Rules (Diss.), a preprint from University of Stockholm, Department of Philosophy, Stockholm.

  12. Prawitz, Dag: 1971, ‘Ideas and Results in Proof Theory’, in J. E. Fenstad (ed.),Proceedings of the Second Scandinavian Logic Symposium, North-Holland, Amsterdam, pp. 235–303.

  13. Prawitz, Dag: 1977, ‘Meaning and Proofs: on the Conflict Between Classical and Intuitionistic Logic’,Theoria 43, 2–40.

  14. Prawitz, Dag: 1980, ‘Intuitionistic Logic: a Philosophical Challenge’, in G. H. von Wright (ed.),Logic and Philosophy, Martinus Nijhoff, The Hague, pp. 1–10.

  15. Saarinen, Esa (ed.): 1979,Game-Theoretical Semantics, D. Reidel, Dordrecht.

  16. Stenius, Erik: 1967, ‘Mood and Language-Game’,Synthese 17, 254–74.

  17. Sundholm, Göran: 1986, ‘Proof Theory and Meaning’, in D. Gabbay and F. Guenther (eds.),Handbook of Philosophical Logic, Vol. 3, D. Reidel, Dordrecht, pp. 471–506.

  18. Tennant, Neil: 1979, ‘Language Games and Intuitionism’,Synthese 42, 297–314.

Download references

Author information

Additional information

The idea of re-working the results of Game-Theoretical Semantics in Martin-Löf's Type Theory dates back to a seminar on constructive logic led by Jan von Plato in the Department of Philosophy, University of Helsinki, since Spring 1986. I have gained a lot from discussions in the seminar and personally with Jan von Plato. The essential content of this paper has also been presented in the Departments of Mathematics and Philosophy, University of Stockholm, in seminars led by Per Martin-Löf and Dag Prawitz, respectively, and in this case also I have enjoyed personal conversation with the seminar leaders. Other persons I wish to thank are Jaakko Hintikka and Göran Sundholm.

Rights and permissions

Reprints and Permissions

About this article

Cite this article

Ranta, A. Propositions as games as types. Synthese 76, 377–395 (1988). https://doi.org/10.1007/BF00869607

Download citation


  • Computer Programming
  • Direct Connection
  • Type Theory
  • Winning Strategy
  • Constructive Type