Abstract

In this paper, we will be interested in the notion of a computable proposition. It allows for feasible computational semantics of empirical sentences, despite the fact that it is in general impossible to get to the truth value of a sentence through a series of effective computational steps. Specifically, we will investigate two approaches to the notion of a computable proposition based on constructive type theory and transparent intensional logic. As we will see, the key difference between them is their accounts of denotations of empirical sentences.