# A two-dimensional metric temporal logic

## TL;DR

This paper introduces a novel two-dimensional metric temporal logic with dense linear orderings for internal and external time flows, providing semantics, a sequent calculus, and proving completeness and cut-elimination.

## Contribution

It presents the first formalization of a two-dimensional metric temporal logic with dense orderings, including semantics, proof calculus, and key metatheoretical results.

## Key findings

- Established semantics for the logic
- Developed a sequent calculus with axioms
- Proved completeness and cut-elimination

## Abstract

We introduce a two-dimensional metric (interval) temporal logic whose internal and external time flows are dense linear orderings. We provide a suitable semantics and a sequent calculus with axioms for equality and extralogical axioms. Then we prove completeness and a semantic partial cut-elimination theorem down to formulas of a certain type.