Intuitionistic Implication in Elementary Team Logics
Abstract
The logic FOT is a team-based logic whose expressive power coincides with first-order logic at the level of both sentences and open formulas. In contrast to dependence and independence logics, which can define stronger second-order team properties, FOT is designed to capture exactly elementary team properties, modulo the empty team. In this paper we consider two modifications of FOT. First, we investigate essentially the inclusion atom free fragment of FOT. Our main result establishes quantifier elimination for the fragment in the empty signature. Second, we study an extension of FOT by the intuitionistic implication. The main conclusion is that adding this single connective increases the expressive strength so that every second-order sentence can be encoded by an open formula evaluated on the full team. Consequently, validity of formulas is equivalent to validity of full second-order logic.
Related
- Intuitionistic and Constructive Modal Logics for Classical Modal Logicians
- Rule extensions of the implication--negation fragment of intuitionistic logic
- Elementary modal logics and circuit complexity
- Fine Selection for Intuitionistic Modal Logic
- Failure of Higher-Order Truth within Intuitionistic Propositional Logic
BibTeX
@misc{engstrom2026intuitionistic,
title = {{Intuitionistic Implication in Elementary Team Logics}},
author = {Fredrik Engström and Juha Kontinen},
howpublished = {arXiv},
year = {2026},
month = sep,
doi = {10.48550/arxiv.2609.15216},
eprint = {2609.15216},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2609.15216},
note = {CC BY 4.0},
}
RIS
TY - UNPB
TI - Intuitionistic Implication in Elementary Team Logics
AU - Fredrik Engström
AU - Juha Kontinen
PY - 2026
DA - 2026/09/14
PB - arXiv
DO - 10.48550/arxiv.2609.15216
UR - https://arxiv.org/abs/2609.15216
AB - The logic FOT is a team-based logic whose expressive power coincides with first-order logic at the level of both sentences and open formulas. In contrast to dependence and independence logics, which can define stronger second-order team properties, FOT is designed to capture exactly elementary team properties, modulo the empty team. In this paper we consider two modifications of FOT. First, we investigate essentially the inclusion atom free fragment of FOT. Our main result establishes quantifier elimination for the fragment in the empty signature. Second, we study an extension of FOT by the intuitionistic implication. The main conclusion is that adding this single connective increases the expressive strength so that every second-order sentence can be encoded by an open formula evaluated on the full team. Consequently, validity of formulas is equivalent to validity of full second-order logic.
ER -