Interval logics formalize temporal reasoning on interval
structures over linearly (or partially) ordered domains, where
time intervals are the primitive ontological entities and
truth of formulae is defined relative to time intervals,
rather than time points.
In this paper, we introduce and study Metric Propositional
Neighborhood Logic (MPNL) over natural numbers. MPNL features two modalities referring, respectively, to an interval
that is ``met by" the current one and to an interval that
``meets" the current one, plus an infinite set of length
constraints, regarded as atomic propositions, to constrain
the length of intervals. We argue that MPNL can be successfully
used in different areas of computer science to combine
qualitative and quantitative interval temporal reasoning,
thus providing a viable alternative to well-established
logical frameworks such as Duration Calculus.
We show that MPNL is decidable in double exponential time and
expressively complete with respect to a well-defined
sub-fragment of the two-variable fragment FO2[N,=,<,s] of first-order logic for linear orders with successor function, interpreted
over natural numbers.
Moreover, we show that MPNL can be extended in a natural way
to cover full FO2[N,=,<,s], but, unexpectedly, the latter (and hence the former) turns out to be undecidable.
