Proof-Theoretic Semantics

So far, we gave some kind of answer to what we called Frege's questions stressing the epistemic character of a possibly incomplete set of proven equalities of an agent, in contrast to identity in a model. We will now turn to the idea of proof-theoretic semantics.

According to ([8], p. 503),

[p]roof-theoretic semantics [assigns] proofs or deductions an autonomous semantic role from the very onset, rather than explaining this role in terms of truth transmission. In prooftheoretic semantics, proofs are not merely treated as syntactic objects […], but as entities in terms of which meaning and logical consequence can be explained.

This approach is already quite successfully pursued for the usual logical operations (see [7, 12] and this volume). It is our aim to extend it to some further concepts, like equalities here or necessity in [6].

In the case of equality a proof-theoretic semantics requires that, from the very onset, one would have to dispense with any (model-theoretic) notion of identity. From a technical point of view, one could say that the proof-theoretic semantics of the equality relation is given by the axioms involving this relation. But what would be the proof-theoretic semantics of a particular equation? The terms in such an equation have now, where any model-theoretic interpretation is gone, of course, an autonomous status.

From a proof-theoretic perspective, “morning star” and “evening star” should, of course, be different. Their mode of presentation is given by the way the axioms introduce them as terms. This includes implicitly the full axiomatic framework which now makes part of the mode of presentation.

Whatever the concrete axioms might be, they should state that the “morning star” is visible (on some days) in the morning, and the “evening star” in the evening, respectively. As discussed above, the equality between them needs a proof. For the proof-theoretic semantics of the terms it should not even be relevant whether such a proof is performed or not—its sheer need gives rise to consider the proof-theoretic semantics as different for the two terms, determined only by the axioms governing them. Only in the case of “immediate” (“trivial” or maybe “elementary”) equalities— like in the case of the symmetry of Intsec—a term might be manipulated without changing its sense.

As related approaches we would like to mention here Tichý's Transparent Intensional Logic (TIL), [1, 13] and Moschovakis's Sense and Denotation as Algorithm and Value, [11].

TIL does not dispense with possible worlds, but assigns them a secondary rôle in the analysis of senses. These are introduced as abstract procedures, called constructions, which are applied to an object, in dependence of a possible world, to decide whether this object (for instance, Venus) fulfills the intension (e.g., being the morning star). With respect to our approach one can ask whether, and if so, in which way the abstract procedures can be related to the proofs we take as a basis.

Such a relation would be given, at least partly, by the Curry–Howard correspondence for Moschovakis's approach. He introduces senses as algorithms which compute (denotational) values. Based on the well-known correspondence of algorithms and proofs, we could adapt Moschovakis's slogan by describing our (broader) approach to intensionality as Sense and Denotation as Proof and Truth. Conversely, Moschovakis's account could also be dubbed a recursion-theoretic semantics.

References

1. Duží, M., Jespersen, B., Materna, P.: Procedural Semantics for Hyperintensional Logic. Logic, Epistemology, and the Unity of Science, vol. 17. Springer, Berlin (2010)

2. Frege, G.: Begriffsschrift, Nebert, Halle a.d.s. (English translation [4])

3. Frege, G.: Über Sinn und Bedeutung. Zeitschrift für Philosophie und philosophische Kritik, NF 100 pp. 25-50 (1892) (English translation [5])

4. Frege, G.: Concept script. In: van Heijenoort, J. (ed.) From Frege to Gödel, Harvard University Press, Cambridge (1967) (English translation of [2])

5. Frege, G.: On sense and meaning. In: McGuiness, B. (ed.) Collected Papers on Mathematics, Logic, and Philosophy, p. 157-177. Basil Blackwell (1974) (English translation of [3] by M. Black)

6. Kahle, R.: A proof-theoretic view of necessity. Synthese 148(3), 659–673 (2006)

7. Kahle, R., Schroeder-Heister, P. (eds.) Proof-Theoretic Semantics. Springer (2006). Special issue of Synthese 148(3), 503-743

8. Kahle, R., Schroeder-Heister, P.: Proof-theoretic semantics-introduction. Synthese 148(3), 503506 (2006)

9. Kripke, S.: Naming and Necessity. Harvard University Press, Cambridge (1980)

10. LaPorte, J.: Rigid Designators. In: Zalta, E.N. (ed.) The Stanford Encyclopedia of Philosophy (Summer 2011 edn.) (2011), plato.stanford.edu/archives/sum2011/entries/rigid- designators/

11. Moschovakis, Y.: Sense and denotation as algorithm and value. In: Väänänen, J., Oikkonen,

J. (eds.) Logic Colloquium '90, pp. 210-249. Lecture Notes in Logic, vol. 2, Association for Symbolic Logic (1994)

12. Schroeder-Heister, P.: Proof-theoretic semantics. In: Zalta, E.N. (ed.) The Stanford Encyclopedia of Philosophy (Winter 2012 edn.) (2012), plato.standard.edu/archives/win2012/ enties/proof-theoretic-semantic/

13. Tichý, P.: The Foundations of Frege's Logic. De Gruyter, Berlin (1988)

14. Wehmeier, K.F.: How to live without identity–and why. Australas. J. Philos. 90(4), 761–777 (2012)