Nonstandard connectives of intuitionistic propositional logic (Q1111536): Difference between revisions

This article is organized as follows: In Section 1 the author proposes the question: ``What is an intuitionistic propositional connective?'', and defines a new n-ary connective ``{\#}'' which is said to be extensional (or weakly extensional). In Section 2 he introduces a new unary connective ``\(\circ ''\) and its related axioms. He extends also the ordinary intuitionistic propositional calculus I to the logical system \(I^{\circ}\) with connective \(\circ\). The extended system has a Gentzen system with the subformula property and cut-free deductions. In Section 3 he explains a possibility of introducing new connectives by their interpretation in Kripke models. He proves that for any n-ary connective {\#} there exists a formula \(\psi (A_ 1,...,A_ n)\) with ordinary connectives only, such that \(I\vdash \psi (A_ 1,...,A_ n)\) implies \(I^{\#}\vdash \#(A_ 1,...,A_ n)\), and \(I^{\#}\vdash \#(A_ 1,...,A_ n)\) implies \(I\vdash \neg \neg \psi (A_ 1,...,A_ n).\) In Section 4 he considers some extension \(I^{\#}\) of I such that {\#} can be described by rules of inference in a Gentzen system. Under natural and not strong restrictions on rules of inference he proves that \(I^{\#}\) can be interpreted either in \(I^{\circ}\) or in propositional intuitionistic modal logic S4.