Fan Yang

In this paper, we introduce a logic based on team semantics, called FOT, whose expressive power is elementary, i.e., coincides with first-order logic both on the level of sentences and (possibly open) formulas, and we also show that a sublogic of FOT, called FOT${}^\downarrow$, captures exactly downward closed elementary (or first-order) team properties. We axiomatize completely the logic FOT, and also extend the known partial axiomatization of dependence logic to dependence logic enriched with the logical constants in FOT${}^\downarrow$.

In this paper, we study several propositional team logics that are closed under unions, including propositional inclusion logic. We prove that all these logics are expressively complete, and we introduce sound and complete systems of natural deduction for these logics. We also discuss the locality property and its connection with interpolation in these logics.

We study descriptive complexity of counting complexity classes in the range from #P to #$\cdot$NP. A corollary of Fagin's characterization of NP by existential second-order logic is that #P can be logically described as the class of functions counting satisfying assignments to free relation variables in first-order formulae. In this paper we extend this study to classes beyond #P and extensions of first-order logic with team semantics. These team-based logics are closely related to existential second-order logic and its fragments, hence our results also shed light on the complexity of counting for extensions of FO in Tarski's semantics. Our results show that the class #$\cdot$NP can be logically characterized by independence logic and existential second-order logic, whereas dependence logic and inclusion logic give rise to subclasses of #$\cdot$NP and #P , respectively. Our main technical result shows that the problem of counting satisfying assignments for monotone Boolean $\Sigma_1$-formulae is #$\cdot$NP-complete as well as complete for the function class generated by dependence logic.

NNIL-formulas, introduced by Visser in 1983–1984 in a study of $\varSigma _1$-subsitutions in Heyting arithmetic, are intuitionistic propositional formulas that do not allow nesting of implication to the left. The first results about these formulas were obtained in a paper of 1995 by Visser et al. In particular, it was shown that NNIL-formulas are exactly the formulas preserved under taking submodels of Kripke models. Recently, Bezhanishvili and de Jongh observed that NNIL-formulas are also reflected by the colour-preserving monotonic maps of Kripke models. In the present paper, we first show how this observation leads to the conclusion that NNIL-formulas are preserved by arbitrary substructures not necessarily satisfying the topo-subframe condition. Then, we apply it to construct universal models for NNIL. It follows from the properties of these universal models that NNIL-formulas are also exactly the formulas that are reflected by colour-preserving monotonic maps. By using the method developed in constructing the universal models, we give a new direct proof that the logics axiomatized by NNIL-axioms have the finite model property.

NNIL-formulas, introduced by Visser in 1983-1984 in a study of $\Sigma_1$-subsitutions in Heyting Arithmetic, are intuitionistic propositional formulas that does not allow nesting of implication to the left. The first results about these formulas were obtained in a paper of 1995 by Visser et al. In particular, it was shown that NNIL-formulas are exactly the formulas preserved under taking submodels of Kripke models. Recently Bezhanishvili and de Jongh observed that NNIL-formulas are also reflected by color-preserving monotonic maps of Kripke models. In the present paper, we first show how this observation leads to the conclusion that NNIL-formulas are preserved by arbitrary substructures not necessarily satisfying the topo-subframe condition. Then we apply it to construct universal models for NNIL. It follows from the properties of these universal models that NNIL-formulas are also exactly the formulas that are reflected by color-preserving monotonic maps. By using the method developed in constructing the universal models, we give a new direct proof that the logics axiomatized by NNIL-axioms have the finite model property.