Semantic characterization of intuitionistic logical connectives (Q1111537)

In classical propositional logic any \(2^ n\)-distribution of 0 and 1 can be interpreted as a suitable combination of propositional variables connected only by \& and \(\neg\). So, any clssical connective given semantically can be expressed by \& and \(\neg\); or, the pair (\&,\(\neg)\) is functionally complete. The author investigates the analogous question for intuitionistic propositional logic: do the four ``standard'' intuitionistic connectives (\&,\(\vee,\Rightarrow,\neg)\) suffice to express any semantically given connective? And, in general, what is an intuitionistic connective when speaking of functional completeness? It is natural to agree that the analogue of classical 0-1-tableau will be a one-free-variable predicate formula (evaluating the connective in Kripke-models) which links the validity of the operation in an arbitrary possible world with validity of the operands in some other worlds. E.g. the evaluation of the intuitionistic implication, \(x\Vdash A\Rightarrow B\), can be regarded as the predicate \((A\Rightarrow B)(x)\) defined by the formula (\(\forall y\geq x)\) (if \(A(y)\) then \(B(y)\)). Furthermore, the author postulates the following three principles for this predicate (they also seem to be natural from the intuitionistic point of view): 1) monotonicity (if C(x) and \(x\leq y\) then C(y)), i.e. what has been proved remains true forever; 2) relativization of quantifiers (\(\forall z\geq w\), \(\exists z\geq w\), etc.), i.e. the truth value at given vertex is determined only by the situation at this vertex and in the future, but not in the past; 3) similarity (intuitively: a proposition constructed by means of logical connectives should not separate models which are equivalent in a precise sense). Then the fundamental theorem affirms that the set of all semantically expressed intuitionistic connectives is exactly covered by the set of all propositional formulas. In such a way the sufficiency of the four standard connectives obtains some semantic ground. Reviewer's note: Some intuitionistic connectives have been proposed which are out of domain of the fundamental theorem. The more important examples of such connectives are the so-called ``dual implication and negation'', introduced by \textit{C. Rauszer} [Fundamenta Math. 83, 219-249 (1974; Zbl 0298.02064)]. Their semantical definitions are the following: \(x\Vdash B\dot- A\) iff (\(\exists y\leq x)\) \((y\Vdash B\) and not \(y\Vdash A)\); \(x\Vdash \ulcorner A\) iff (\(\exists y\leq x)\) (not \(y\Vdash A)\) [see \textit{D. Vakarelov}, Bull. Acad. Pol. Sci., Sér. Sci. Math. Astron. Phys. 22, 1087-1095 (1974; Zbl 0301.02066)]. As we see, the principle of relativization is not true here, and \(\dot-\) and \(\ulcorner\) are not expressible by \&, \(\vee\), \(\Rightarrow\), \(\neg\), indeed. In fact, the corresponding logic is a conservative extension of intuitionistic logic but the intuitionistic character of these connectives is doubtful because, e.g., the law of excluded middle is valid for \(\ulcorner\). So, exceptio probat regulam.