Intuitionistic implication without disjunction (Q2893316)

The authors consider a unified approach to investigate fragments of intuitionistic propositional logic \(\mathsf{IpL}\) without disjunction but with implication. In particular, they give a new proof of the well-known fact that, for any \(n\), each of these fragments has only finitely many nonequivalent formulas with the variables \(p_1,\ldots,p_n\). A fragment \(F=[P,\circ_1,\ldots,\circ_n]\) is given by a set of atoms \(P\) and connectives \(\circ_1,\ldots,\circ_n\) (\(\neg\neg\) being considered as a connective). The diagram \(F_\equiv\) of a fragment \(F\) is the set of the equivalence classes of formulas partially ordered by the derivability relation. A model \(M=\langle W,\leq,\models\rangle\) is universal for \(F\) if \(\forall w\,(w\models\varphi\Leftrightarrow w\models\psi)\) means the same as \(\varphi\equiv\psi\). A construction of the universal model \(\mathsf{UM}\) for \(\mathsf{IpL}\) is proposed. The worlds in this model are so-called semantical types, which are defined inductively as objects of the form \(\langle P,X\rangle\), where \(P\) is a collection of propositional variables and \(X\) is a finite collection of types. The model \(\mathsf{UM}\) is locally finite in the sense that the set of worlds above \(w\) is finite for any \(w\). A model \(M\) is an exact (a quasi-exact) model for \(F\) if \(F_\equiv\) is isomorphic to (a subset of) the collection of upward closed subsets of \(W\). For any finite \(P\), an exact model \(\mathsf{EM}_\neg(P)\) for \([P,\neg,\land,\to]\), an exact model \(\mathsf{EM}(P)\) for \([P,\land,\to]\) and a quasi-exact model \(\mathsf{QEM}(P)\) for \([P,\neg\neg,\land,\to]\) are constructed. All three are finite submodels of \(\mathsf{UM}\). These models are used to characterize the fragments under consideration. For a model \(M\), let \({\mathcal P}^a(M)\) denote the collection of antichains in \(W\) ordered by the relation \(A\preceq B\leftrightharpoons B\subseteq A\downarrow\), where \(A\downarrow\) is the downward closure of \(A\). It is proved that \([P,\neg,\land,\to]_\equiv\) is isomorphic to \({\mathcal P}^a(\mathsf{EM}_\neg(P))\), \([P,\land,\to]_\equiv\) is isomorphic to \({\mathcal P}^a(\mathsf{EM}(P))\), and \([P,\neg\neg,\land,\to]_\equiv\) is isomorphic to \({\mathcal P}^a(\mathsf{QEM}(P)\setminus\{\langle P,\emptyset\rangle\})\). A similar characterization of the fragments without \(\land\) and \(\lor\) is obtained too. Formulas for the size of the (quasi-)exact models and the diagrams of the fragments are proposed and their asymptotic behaviour is studied. Namely, the size of diagrams grows superexponentially with the number of variables.