Une Preuve Formelle et Intuitionniste du Théorème de Complétude de la Logique Classique (Q3128482)

As is well known, by means of the Curry-Howard correspondence, we can associate a program, precisely a \(\lambda\)-term, to each intuitionistic proof, formalized in natural deduction in the second-order predicate calculus [cf., for example, the author, Lambda calculus, types and models (1993; Zbl 0779.03005); see the review of the French original: Lambda-calcul, types et modèles (1990; Zbl 0697.03004)]. This can also be done for each classical proof, using a suitable extension of \(\lambda\)-calculus [cf. \textit{V. Danos, J. B. Joinet} and \textit{H. Schellinx}, in: J.-Y. Girard et al. (eds.), Advances in linear logic, based on the Linear Logic Workshop, Cornell, 1993, Lond. Math. Soc. Lect. Note Ser. 222, 211-224 (1995; Zbl 0829.03031); the author, Ann. Pure Appl. Logic 68, 53-78 (1994; Zbl 0814.03009); \textit{M. Parigot}, Lect. Notes Comput. Sci. 713, 263-276 (1993; Zbl 0805.03012)]. Therefore, to every theorem formalized in second-order classical logic, there corresponds a program specification. Now, the problem of finding the specification associated with a given theorem is, in general, absolutely not trivial. This amounts to find the common operational behaviour of the various \(\lambda\)-terms associated with every proof of the theorem. In the present paper, this problem is solved for the completeness theorem of classical logic. The first step (sections I and II) is the complete formalization of this theorem in second-order logic. As a by-product, we get that this theorem is provable in intuitionistic second-order logic, which is perhaps unexpected. We must, however, change slightly the notion of model, by introducing an additional ``trivial' model in which every formula is satisfied. In this respect, one should notice that \textit{G. Kreisel} has shown [J. Symb. Log. 27, 139-158 (1963; Zbl 0117.01005)] that the usual completeness theorem of intuitionistic logic has no intuitionistic proof. \smallskip The second step is done in section III, in which the results are only stated; complete proofs will be developed in a subsequent paper. It consists in an analysis of all the possible classical proofs of the completeness theorem, and of the corresponding \(\lambda\)-terms. In this way, we obtain the specification associated with the completeness theorem of classical logic, which appears somewhat surprising: it is, indeed, an interactive disassembler, provided with the protection device for system calls which is usually implemented in this sort of programs. This result naturally calls for epistemological comments, which are postponed to the subsequent paper mentioned earlier.