Proof-functional connectives and realizability (Q1330311)

The paper analyses and investigates to the so called ``proof-functional'' logical connectives, building on and developing previous observations and results by \textit{E. G. K. Lopez-Escobar} [Lect. Notes Math. 1130, 208-221 (1985; Zbl 0615.03047)] and \textit{G. Mints} [Notre Dame J. Formal Logic 30, No. 3, 420-441 (1989; Zbl 0704.03004)]. Proof-functionality is an intensional concept related to connectives whose meaning depends on the actual shape of the proofs (realizers) for the components of a compound formula. Such an undoubtedly debatable concept (some hints and suggestions for discussion are given in the introduction) is embodied in the paper in two particular connectives: strong conjunction and strong equivalence. In the former, the two components of the conjunction have the same realizer, whereas in the latter the equivalence is established by means of realizer-maps which are one the inverse of the other. The main focus of the paper is the realizability analysis of such connectives. For each connective a formal system is provided which is sound and complete with respect to provable realizability in intuitionistic logic. Such systems are shown to have an interpretation in terms of computer science concepts, the system for strong conjunction being equivalent to a particular type assignment system for lambda-terms with intersection types, and that for strong equivalence being related to systems for provable isomorphisms in typed lambda-calculi. A connection is also established with the connective of relevant implication. The provable realizability completeness results are also shown to imply the semantical completeness for the type assignment systems mentioned above.