Sense, reference, and computation

TL;DR

This paper revisits Frege's sense and reference within type theory, proposing a computational identity criterion for senses that aligns with Frege's principles and extends previous work on sense-reference analysis.

Contribution

It introduces a computational identity criterion for senses in type theory, sharpening the understanding of Frege's sense-reference relationship in a constructive setting.

Findings

Proposes a computational identity criterion for senses.

Validates Frege's equipollence principle in a formal setting.

Extends sense-reference analysis within type theory.

Abstract

In this paper, I revisit Frege's theory of sense and reference in the constructive setting of the meaning explanations of type theory, extending and sharpening a program--value analysis of sense and reference proposed by Martin-L\"of building on previous work of Dummett. I propose a computational identity criterion for senses and argue that it validates what I see as the most plausible interpretation of Frege's equipollence principle for both sentences and singular terms. Before doing so, I examine Frege's implementation of his theory of sense and reference in the logical framework of Grundgesetze, his doctrine of truth values, and views on sameness of sense as equipollence of assertions.