Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Definite Descriptions and Hybrid Tense Logic

Andrzej Indrzejczak, Michał Zawidzki

TL;DR

This paper extends first-order hybrid tense logic by incorporating predicate abstracts and tensal definite descriptions within a Russellian-inspired framework, and provides a constructive sat-tableau calculus for $FOHL^{\mathsf{F,P}}_{\lambda,\iota}$. It establishes soundness and completeness of the tableau system and proves a constructive Craig interpolation theorem, adapting existing interpolation techniques to handle definite descriptions and lambda-terms. The work advances the treatment of non-rigid description terms in temporal semantics, and demonstrates how tensal descriptions and downarrow binders interact in a proof-theoretic setting, with potential extensions to stronger frame classes and description-logics-inspired formalisms. The results yield a robust, implementable method for reasoning about temporal descriptions and predicate abstraction in a rigorous logical framework, with implications for automated reasoning and semantic analysis in natural language and formal ontology contexts.

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.

Definite Descriptions and Hybrid Tense Logic

TL;DR

This paper extends first-order hybrid tense logic by incorporating predicate abstracts and tensal definite descriptions within a Russellian-inspired framework, and provides a constructive sat-tableau calculus for . It establishes soundness and completeness of the tableau system and proves a constructive Craig interpolation theorem, adapting existing interpolation techniques to handle definite descriptions and lambda-terms. The work advances the treatment of non-rigid description terms in temporal semantics, and demonstrates how tensal descriptions and downarrow binders interact in a proof-theoretic setting, with potential extensions to stronger frame classes and description-logics-inspired formalisms. The results yield a robust, implementable method for reasoning about temporal descriptions and predicate abstraction in a rigorous logical framework, with implications for automated reasoning and semantic analysis in natural language and formal ontology contexts.

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.

Paper Structure

This paper contains 11 sections, 10 theorems, 9 equations, 4 figures.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Tableau Calculus
  4. Basic rules
  5. Soundness and Completeness
  6. Soundness
  7. Completeness
  8. Interpolation
  9. Conclusion
  10. Acknowledgements
  11. Conflict of interest

Key Result

Lemma 1

Let $\varphi \in \mathsf{FOR}$, let $\mathcal{M} = (\mathcal{T}, \prec,\mathcal{D},\mathcal{I})$ be a tense model, let $\bm{t} \in \mathcal{T}$, and let $\mathcal{v}_1,\mathcal{v}_2$ be assignments. If $\mathcal{v}_1(\mathcal{x})=\mathcal{v}_2(\mathcal{x})$ for each $\mathcal{x} \in \mathsf{FVAR} \c

Figures (4)

  • Figure 1: Tense model from Example \ref{['ex::BaldKing']}
  • Figure 2: Rules of the tableau calculus $\mathscr{TC}(\mathsf{FOHL}^\mathsf{F,P}_{\lambda,\iota})$
  • Figure 3: Example proofs conducted in $\mathscr{TC}(\mathsf{FOHL}^\mathsf{F,P}_{\lambda,\iota})$; \ref{['fig::Examples']}(a) shows a proof tree for the derivation $@_{\iota \bm{x}W(t,j)}M(t,j,l),\ @_{\iota \bm{x}W(t,j)}\iota \bm{y}B\ \vdash\ @_{\iota \bm{y}B}M(t,j,l)$ from \ref{['ex::Wedding']}; \ref{['fig::Examples']}(b) presents a proof of the derivability of the rule $(\mathsf{DD})$$@_{\bm{j}} @_{\iota \bm{x}\varphi}\iota \bm{y}\psi\ ,\ @_{\bm{j}}@_{\iota \bm{x}\varphi}\chi\ / \ @_{\bm{j}} @_{\iota \bm{y}\psi}\chi$ in $\mathscr{TC}(\mathsf{FOHL}^\mathsf{F,P}_{\lambda,\iota})$; \ref{['fig::Examples']}(c) displays a proof of the validity of the Barcan formula in $\mathsf{HFL_K}$.
  • Figure 4: The interderivability of the rules $(\iota_2^o)$ and $({\iota_2^o}')$; \ref{['fig::Derivability']}(a) displays a proof of the derivability of $({\iota_2^o}')$ in $\mathscr{TC}(\mathsf{FOHL}^\mathsf{F,P}_{\lambda,\iota})$ with $(\mathsf{cut})$; \ref{['fig::Derivability']}(b) shows a proof of the derivability of $({\iota_2^o})$ in $\mathscr{TC}(\mathsf{FOHL}^\mathsf{F,P}_{\lambda,\iota})'$

Theorems & Definitions (14)

  • Example 1
  • Example 2
  • Example 3
  • Example 4
  • Lemma 1: Coincidence Lemma
  • Lemma 2: Substitution Lemma
  • Lemma 3
  • Theorem 4: Soundness
  • Proposition 5
  • Lemma 6
  • ...and 4 more