Krivine's classical realisability from a categorical perspective

2013 ◽  
Vol 23 (6) ◽  
pp. 1234-1256 ◽  
Author(s):  
THOMAS STREICHER

In a sequence of papers (Krivine 2001; Krivine 2003; Krivine 2009), J.-L. Krivine introduced his notion of classical realisability for classical second-order logic and Zermelo–Fraenkel set theory. Moreover, in more recent work (Krivine 2008), he has considered forcing constructions on top of it with the ultimate aim of providing a realisability interpretation for the axiom of choice.The aim of the current paper is to show how Krivine's classical realisability can be understood as an instance of the categorical approach to realisability as started by Martin Hyland in Hyland (1982) and described in detail in van Oosten (2008). Moreover, we will give an intuitive explanation of the iteration of realisability as described in Krivine (2008).

Author(s):  
Tim Button ◽  
Sean Walsh

In this chapter, the focus shifts from numbers to sets. Again, no first-order set theory can hope to get anywhere near categoricity, but Zermelo famously proved the quasi-categoricity of second-order set theory. As in the previous chapter, we must ask who is entitled to invoke full second-order logic. That question is as subtle as before, and raises the same problem for moderate modelists. However, the quasi-categorical nature of Zermelo's Theorem gives rise to some specific questions concerning the aims of axiomatic set theories. Given the status of Zermelo's Theorem in the philosophy of set theory, we include a stand-alone proof of this theorem. We also prove a similar quasi-categoricity for Scott-Potter set theory, a theory which axiomatises the idea of an arbitrary stage of the iterative hierarchy.


2010 ◽  
Vol 16 (1) ◽  
pp. 1-36 ◽  
Author(s):  
Peter Koellner

AbstractIn this paper we investigate strong logics of first and second order that have certain absoluteness properties. We begin with an investigation of first order logic and the strong logics ω-logic and β-logic, isolating two facets of absoluteness, namely, generic invariance and faithfulness. It turns out that absoluteness is relative in the sense that stronger background assumptions secure greater degrees of absoluteness. Our aim is to investigate the hierarchies of strong logics of first and second order that are generically invariant and faithful against the backdrop of the strongest large cardinal hypotheses. We show that there is a close correspondence between the two hierarchies and we characterize the strongest logic in each hierarchy. On the first-order side, this leads to a new presentation of Woodin's Ω-logic. On the second-order side, we compare the strongest logic with full second-order logic and argue that the comparison lends support to Quine's claim that second-order logic is really set theory in sheep's clothing.


2020 ◽  
pp. 187-212
Author(s):  
Bob Hale

Quine’s charge against second-order logic is that it carries massive existential commitments. This chapter argues that if we interpret second-order variables as ranging over properties construed in accordance with an abundant or deflationary conception, Quine’s charge can be resisted. This need not preclude the use of model-theoretic semantics for second-order languages; but it precludes the standard semantics, along with the more general Henkin semantics, of which it is a special case. To that extent, the approach of this chapter has revisionary implications; it is, however, compatible with the different special case in which second-order variables are taken to range over definable subsets of the first-order domain, and with respect to such a semantics, important metalogical results obtainable under the standard semantics may still be obtained. Finally, the chapter discusses the relations between second-order logic, interpreted as recommended, and a strong version of schematic ancestral logic promoted in recent work by Richard Kimberly Heck.


Author(s):  
Ignacio Jané

This article discusses canonical (i.e., full, or standard) second-order consequence and argues against it being a case of logical consequence. The discussion is divided into three parts. The first part comprises the first three sections. After stating the problem in Section 1, Sections 2 and 3 examine the role that the consequence relation is expected to play in axiomatic theories. This leads to put forward two requirements on logical consequence, which are called “formality” and “noninterference.” It is this last requirement that canonical second-order consequence violates, as the article sets out to substantiate. The fourth section argues that canonical second-order logic is inadequate for axiomatizing set theory, on the grounds that it codes a significant amount of set-theoretical content.


1995 ◽  
Vol 1 (3) ◽  
pp. 317-326 ◽  
Author(s):  
George Boolos

Two thoughts about the concept of number are incompatible: that any zero or more things have a (cardinal) number, and that any zero or more things have a number (if and) only if they are the members of some one set. It is Russell's paradox that shows the thoughts incompatible: the sets that are not members of themselves cannot be the members of any one set. The thought that any (zero or more) things have a number is Frege's; the thought that things have a number only if they are the members of a set may be Cantor's and is in any case a commonplace of the usual contemporary presentations of the set theory that originated with Cantor and has become ZFC.In recent years a number of authors have examined Frege's accounts of arithmetic with a view to extracting an interesting subtheory from Frege's formal system, whose inconsistency, as is well known, was demonstrated by Russell. These accounts are contained in Frege's formal treatise Grundgesetze der Arithmetik and his earlier exoteric book Die Grundlagen der Arithmetik. We may describe the two central results of the recent re-evaluation of his work in the following way: Let Frege arithmetic be the result of adjoining to full axiomatic second-order logic a suitable formalization of the statement that the Fs and the Gs have the same number if and only if the F sand the Gs are equinumerous.


2001 ◽  
Vol 7 (4) ◽  
pp. 504-520 ◽  
Author(s):  
Jouko Väänänen

AbstractWe discuss the differences between first-order set theory and second-order logic as a foundation for mathematics. We analyse these languages in terms of two levels of formalization. The analysis shows that if second-order logic is understood in its full semantics capable of characterizing categorically central mathematical concepts, it relies entirely on informal reasoning. On the other hand, if it is given a weak semantics, it loses its power in expressing concepts categorically. First-order set theory and second-order logic are not radically different: the latter is a major fragment of the former.


2015 ◽  
Vol 10 (7) ◽  
pp. 463-478
Author(s):  
Jouko Väänänen

Author(s):  
Tim Button ◽  
Sean Walsh

This chapter introduces the concepts of signature and structure, and describes the semantics for first- and second-order logic. We outline three different but extensionally equivalent treatments of quantifiers and variables (the Tarskian approach, the Robinsonian approach, and a hybrid approach) and discuss their philosophical merits concerning compositionality, and Fine’s antinomy of the variable. We also outline two extensionally distinct semantics for second-order logic (Henkin, full). The appendix to the chapter presents the formal definitions of some theories of arithmetic and set theory that we employ frequently throughout the remainder of the book.


Sign in / Sign up

Export Citation Format

Share Document