Intuitionistic implication without disjunction
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.
- Intuitionistic propositional logic with only equivalence has no interpolation
- Interpolation in fragments of intuitionistic propositional logic
- A Finite Hilbert‐Style Axiomatization of the Implication‐Less Fragment of the Intuitionistic Propositional Calculus
- Complexity of intuitionistic propositional logic and its fragments
- Computations in fragments of intuitionistic propositional logic
- The admissible rules of \(\mathsf{BD}_2\) and \(\mathsf{GSc}\)
- Classifying material implications over minimal logic
- On three implication-less fragments of t-norm based fuzzy logics
- Noninterference for Intuitionist Necessity
- Algebraic semantics for the (, )-fragment of IPC
- A generalization of inquisitive semantics
- Duality and universal models for the meet-implication fragment of IPC
- Positive formulas in intuitionistic and minimal logic
- Disjunction and existence under implication in elementary intuitionistic formalisms
- Intuitionistic propositional logic with only equivalence has no interpolation
- scientific article; zbMATH DE number 1045389 (Why is no real title available?)
- Extendible formulas in two variables in intuitionistic logic
- Monadic fragments of intuitionistic control logic
- The Expressive Force of Some Fragments of Intuitionistic Propositional Logic with Regard to Kripke Frames
- An \(\mathsf{AC}^{1}\)-complete model checking problem for intuitionistic logic
- The complexity of disjunction in intuitionistic logic
- Notes on my scientific life
This page was built for publication: Intuitionistic implication without disjunction
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2893316)
