A note about Grothendieck's constant
A remark on the proof that the Grothendieck constant satisfies $K_G < π/(2\ln(1+\sqrt{2}))$.
math.FA↗
arXiv subjects
Jean-Louis Krivine
Publications and source records attributed to Jean-Louis Krivine.
A program for the full axiom of choice
The theory of classical realizability is a framework for the Curry-Howard correspondence which enables to associate a program with each proof in Zermelo-Fraenkel set theory. But, almost all the applications of mathematics in physics, probability, statistics, etc. use Analysis i.e. the axiom of dependent choice (DC) or even the (full) axiom of choice (AC). It is therefore important to find explicit programs for these axioms. Various solutions have been found for DC, for instance the lambda-term called "bar recursion" or the instruction "quote" of LISP. We present here the first program for AC.
cs.LO↗
Bar recursion in classical realisability : dependent choice and continuum hypothesis
This paper is about the bar recursion operator in the context of classical realizability. After the pioneering work of Berardi, Bezem & Coquand [1], T. Streicher has shown [10], by means of their bar recursion operator, that the realizability models of ZF, obtained from usual models of $λ$-calculus (Scott domains, coherent spaces, . . .), satisfy the axiom of dependent choice. We give a proof of this result, using the tools of classical realizability. Moreover, we show that these realizability models satisfy the well ordering of $\mathbb{R}$ and the continuum hypothesis These formulas are therefore realized by closed $λ_c$-terms. This allows to obtain programs from proofs of arithmetical formulas using all these axioms.
cs.LO↗
On the structure of classical realizability models of ZF
The technique of "classical realizability" is an extension of the method of "forcing"; it permits to extend the Curry-Howard correspondence between proofs and programs, to Zermelo-Fraenkel set theory and to build new models of ZF, called "realizability models". The structure of these models is, in general, much more complicated than that of the particular case of "forcing models". We show here that the class of constructible sets of any realizability model is an elementary extension of the constructibles of the ground model (a trivial fact in the case of forcing, since these classes are identical). It follows that Shoenfield absoluteness theorem applies to realizability models.
cs.LO↗
Realizability algebras III: some examples
We use the technique of "classical realizability" to build new models of ZF + DC in which R is not well ordered. This gives new relative consistency results, probably not obtainable by forcing. This gives also a new method to get programs from proofs of arithmetical formulas with dependent choice.
cs.LO↗
Realizability algebras II : new models of ZF + DC
Using the proof-program (Curry-Howard) correspondence, we give a new method to obtain models of ZF and relative consistency results in set theory. We show the relative consistency of ZF + DC + there exists a sequence of subsets of R the cardinals of which are strictly decreasing + other similar properties of R. These results seem not to have been previously obtained by forcing.
math.LO↗
Realizability algebras: a program to well order R
The theory of classical realizability is a framework in which we can develop the proof-program correspondence. Using this framework, we show how to transform into programs the proofs in classical analysis with dependent choice and the existence of a well ordering of the real line. The principal tools are: The notion of realizability algebra, which is a three-sorted variant of the well known combinatory algebra of Curry. An adaptation of the method of forcing used in set theory to prove consistency results. Here, it is used in another way, to obtain programs associated with a well ordering of R and the existence of a non trivial ultrafilter on N.
cs.LO↗
Algèbres de réalisabilité: un programme pour bien ordonner R
We give a method to transform into programs, classical proofs using a well ordering of the reals. The technics uses a generalization of Cohen's forcing and the theory of classical realizability introduced by the author.
cs.LO↗
Structures de réalisabilité, RAM et ultrafiltre sur N
We show how to transform into programs the proofs in classical Analysis which use the existence of an ultrafilter on the integers. The method mixes the classical realizability introduced by the author, with the "forcing" of P. Cohen. The programs we obtain, use read and write instructions in random access memory.
cs.LO↗
Valid formulas, games and network protocols
We describe a remarkable relation between the notion of valid formula of predicate logic and the specification of network protocols. We give several examples such as the acknowledgement of one packet or of a sequence of packets. We show how to specify the composition of protocols.
cs.LO↗