Generalised definablility of discrete time interval-based temporal connectives

In Linear Temporal Logic with past (PLTL), expressive completeness implies that first-order definable connectives are also definable in terms of Since and Until. This is not so about discrete time interval-based temporal logics with state-based semantics for the propositional variables. We prove the next best thing about the extension ITLNL of Moszkowski's discrete time propositional Interval Temporal Logic ITL by the neighbourhood modalities: given an interval-based first-order definable connective #, a star-free ITLNL defining formula for #(A1,…,Am) can be produced that is built from the past, future and introspective formulas appearing in some separated equivalents of the operands A1,…,Am. Our proof is based on an interval-based analogue of Gabbay's separation theorem about PLTL that we previously established for ITLNL and have now used to prove the expressive completeness of ITLNL. As a side result, we also obtain new proofs of expressive completeness and temporal separation for ITLNL's star-free subset.