Abstract In the style of Lindström’s theorem for classical first-order logic, this article characterizes propositional bi-intuitionistic logic as the maximal (with respect to expressive power) abstract logic satisfying a certain form of compactness, the Tarski union property and preservation under bi-asimulations. Since bi-intuitionistic logic introduces new complexities in the intuitionistic setting by adding the analogue of a backwards looking modality, the present paper constitutes a non-trivial modification of the previous work done by the authors for intuitionistic logic (Badia and Olkhovikov, 2020, Notre Dame Journal of Formal Logic, 61, 11–30).

We present a completeness result for a logical system which combines stit logic and epistemic justification logic in order to represent proving activity of the agents. This logic is interpreted over the semantics introduced in Olkhovikov and Wansing (2018, Studia Logica). We define a Hilbert-style axiomatic system for this logic and show that this system is strongly complete relative to the intended semantics.

The article introduces notions of first-order asimulation and first-order k-asimulation, which extend notions of asimulation and k-asimulation introduced in Olkhovikov (2012, Review of Symbolic Logic, 6, 348–365) onto the level of intuitionistic predicate logic. We then prove that a first-order formula is equivalent to a standard translation of an intuitionistic predicate formula iff it is invariant with respect to first-order k-asimulations for some k, and then that a first-order formula is equivalent to a standard translation of an intuitionistic predicate formula iff it is invariant with respect to first-order asimulations. Finally, it is proved that a first-order formula is equivalent to a standard translation of an intuitionistic predicate formula over a class of intuitionistic models (intuitionistic models with constant domain) iff it is invariant with respect to first-order asimulations between intuitionistic models (intuitionistic models with constant domain).

Abstract This paper shows that the interpolation theorem fails in the intuitionistic logic of constant domains. This result refutes two previously published claims that the interpolation property holds.