Paulo Oliva
Paulo Oliva (Queen Mary University of London)
Ever since Kleene came up with the notion of realizability in the 1940s [1], several variants of the method have been proposed, with a wide range of applications. This course aims to provide the participants with an introduction to “realizability”, covering the main developments in the subject from Kleene’s number realizability until the more recent bounded modified realizability [2] and the Herbrand realizability [3].
The first lecture will introduce the notion of realizability, and place it in the historical logic context of the 1940s. In the second lecture we will look at the first variants of realizability, such as q-realizability, realizability with truth, Kreisel’s modified realizability, and Goodman’s combination of realizability and forcing. The third lecture covers more recent variants of realizability [2,3], and the interpretation of classical theories, including the interpretation of Peano arithmetic. In the final lecture we study the modified realizability interpretation of analytical principles, such as countable choice and comprehension, making use of modified bar recursion [4].
[1] S. C. Kleene, On the interpretation of intuitionistic number theory. JSL. 10 (4): 109–124, 1945
[2] A. Nunes and F. Ferreira, JSL 71:329-346, 2006
[3] B. van den Berg et al. A functional interpretation for nonstandard arithmetic. APAL, 163:1962–1994, 2012
[4] U. Berger and P. Oliva, Modified bar recursion and classical dependent choice, LNL (20):89-107, 2005