Open Research Index

The proof theory and semantics of second-order (intuitionistic) tense logic

Justus Becker, Anupam Das, Sonia Marin, Paaras Padhiar

arXivarxiv/2602.06253Feb 5, 2026cs.LOscore 0

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…

SourceJSON

Comments and reviews

No comments yet.

Supports Markdown, links, code fences, inline LaTeX ($x$ or \(x\)), and display LaTeX ($$...$$ or \[...\]).

Drafts stay in this tab.

API

curl /api/v1/records/arxiv/2602.06253
curl -X POST /api/v1/records/arxiv/2602.06253/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/arxiv/2602.06253/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"body": "…", "review": true}'