A survey of logical problems for the concept of omniscience.

This paper presents a systematic study of the prehistory of the traditional subsystems of second-order arithmetic that feature prominently in the reverse mathematics program of Friedman and Simpson. We look in particular at: (i) the long arc from Poincar\'e to Feferman as concerns arithmetic definability and provability, (ii) the interplay between finitism and the formalization of analysis in the lecture notes and publications of Hilbert and Bernays, (iii) the uncertainty as to the constructive status of principles equivalent to Weak K\"onig's (...) Lemma, and (iv) the large-scale intellectual backdrop to arithmetical transfinite recursion in descriptive set theory and its effectivization by Borel, Lusin, Addison, and others. (shrink)

Partial functions can be easily represented in set theory as certain sets of ordered pairs. However, classical set theory provides no special machinery for reasoning about partial functions. For instance, there is no direct way of handling the application of a function to an argument outside its domain as in partial logic. There is also no utilization of lambda-notation and sorts or types as in type theory. This paper introduces a version of von-Neumann-Bernays-Gödel set theory for reasoning about sets, proper (...) classes, and partial functions represented as classes of ordered pairs. The underlying logic of the system is a partial first-order logic, so class-valued terms may be nondenoting. Functions can be specified using lambda-notation, and reasoning about the application of functions to arguments is facilitated using sorts similar to those employed in the logic of the IMPS Interactive Mathematical Proof System. The set theory is intended to serve as a foundation for mechanized mathematics systems. (shrink)

Partial functions are ubiquitous in both mathematics and computer science. Therefore, it is imperative that the underlying logical formalism for a general-purpose mechanized mathematics system provide strong support for reasoning about partial functions. Unfortunately, the common logical formalisms — first-order logic, type theory, and set theory — are usually only adequate for reasoning about partial functionsin theory. However, the approach to partial functions traditionally employed by mathematicians is quite adequatein practice. This paper shows how the traditional approach to partial functions (...) can be formalized in a range of formalisms that includes first-order logic, simple type theory, and Von-Neumann—Bernays—Gödel set theory. It argues that these new formalisms allow one to directly reason about partial functions; are based on natural, well-understood, familiar principles; and can be effectively implemented in mechanized mathematics systems. (shrink)

In his recent book, Quine, New Foundations, and the Philosophy of Set Theory, Sean Morris attempts to rehabilitate Quine’s NF as a possible foundation for mathematics. I explain why he does not succeed.

Michael Friedman has recently argued that Carnap'sLogical Syntax of Language is fundamentally flawed in a way that reveals the ultimate failure of logical positivism. Friedman's argument depends crucially on two claims: (1) that Carnap was committed to the view that there is a universal metalanguage and (2) that given what Carnap wanted from a metalanguage, in particular given that he wanted a definition of analytic for an object language, he was in fact committed to a hierarchy of stronger and stronger (...) metalanguages. We argue that neither of these claims need be accepted. We show that there is no textual evidence for (1) and that if metalanguages are to be used for merely descriptive and not also justificatory purposes, Carnap does not need to define analyticity sufficiently for proving consistency, and so could have given a definition that does not entail a hierarchy of metalanguages. (shrink)