We develop a second-order extension of intuitionistic modal logic, allowing quantification over propositions, both syntactically and semantically. A key feature of second-order logic is its capacity to define positive connectives from the negative fragment. Duly we are able to recover the diamond (and its associated theory) using only boxes, as long as we include both forward and backward modalities (`tense' modalities). We propose axiomatic, proof theoretic and model theoretic definitions of `second-order intuitionistic tense logic', and ultimately prove that they all coincide. In particular we establish completeness of a labelled sequent calculus via a proof search argument, yielding at the same time a cut-admissibility result. Our methodology also applies to the classical version of second-order tense logic, which we develop in tandem with the intuitionistic case.

翻译：本文发展了一种直觉主义模态逻辑的二阶扩展，允许在句法和语义层面进行命题量化。二阶逻辑的一个关键特征在于其能够从否定片段定义正连接词。相应地，只要同时包含前向与后向模态（"时态"模态），我们便能仅用方框算子（及其相关理论）恢复菱形算子。我们提出了"二阶直觉主义时态逻辑"的公理化、证明论与模型论定义，并最终证明这些定义相互等价。特别地，我们通过证明搜索论证建立了带标签相继式演算的完备性，同时获得了切割可容许性结果。我们的方法同样适用于二阶时态逻辑的经典版本，该版本与直觉主义情形被并行发展。