Definite Descriptions and Hybrid Tense Logic

TL;DR

This paper develops a first-order hybrid tense logic incorporating predicate abstracts and definite descriptions as non-rigid terms, with a tableau calculus and a constructive proof of the interpolation theorem.

Contribution

It introduces a novel formalization of hybrid tense logic with definite descriptions as genuine terms, extending Russellian approaches and providing a tableau calculus with interpolation proof.

Findings

Formalization of hybrid tense logic with definite descriptions

Development of a tableau calculus for the logic

Constructive proof of the interpolation theorem

Abstract

We provide a version of first-order hybrid tense logic with predicate abstracts and definite descriptions as the only non-rigid terms. It is formalised by means of a tableau calculus working on sat-formulas. A particular theory of DD exploited here is essentially based on the approach of Russell, but with descriptions treated as genuine terms. However, the reductionist aspect of the Russellian approach is retained in several ways. Moreover, a special form of tense definite descriptions is formally developed. A constructive proof of the interpolation theorem for this calculus is given, which is an extension of the result provided by Blackburn and Marx.