Off-campus access
Using PhilPapers from home?
Click here to configure this browser for off-campus access.
- Gian Aldo Antonelli (1998). Extensional Quotients for Type Theory and the Consistency Problem for NF. Journal of Symbolic Logic 63 (1):247-261.Quine’s “New Foundations” (NF) was first presented in Quine [1937] and later on in Quine [1963]. Ernst Specker [1958, 1962], building upon a previous result of Ehrenfeucht and Mostowski [1956], showed that NF is consistent if and only if there is a model of the Theory of Negative (and positive) Types (TNT) with full extensionality that admits of a “shifting automorphism,” but the existence of a such a model remains an open problem.
Similar books and articles
Image factorizations in regular categories are stable under pullbacks, so they model a natural modal operator in dependent type theory. This unary type constructor [A] has turned up previously in a syntactic form as a way of erasing computational content, and formalizing a notion of proof irrelevance. Indeed, semantically, the notion of a support is sometimes used as surrogate proposition asserting inhabitation of an indexed family. We give rules for bracket types in dependent type theory and provide complete semantics using regular categories. We show that dependent type theory with the unit type, strong extensional equality types, strong dependent sums, and bracket types is the internal type theory of regular categories, in the same way that the usual dependent type theory with dependent sums and products is the internal type theory of locally Cartesian closed categories. We also show how to interpret first-order logic in type theory with brackets, and we make use of the translation to compare type theory with logic. Specifically, we show that the propositions-as-types interpretation is complete with respect to a certain fragment of intuitionistic first-order logic, in the sense that a formula from the fragment is derivable in intuitionistic first-order logic if, and only if, its interpretation in dependent type theory is inhabited. As a consequence, a modified double-negation translation into type theory (without bracket types) is complete, in the same sense, for all of classical first-order logic.
Most scholars who presently deal with the Mind-Body problem consider themselves monist materialists. Nevertheless, many of them also assume that there exist (in some sense of existence) mental entities. But since these two positions do not harmonize quite well, the literature is full of discussions about how to reconcile the positions. In this paper, I will defend a materialist theory that avoids all these problems by completely rejecting the existence of mental entities. This is Quine's repudiation theory. According to the theory, there are no mental entities, and the behavioral or physiological phenomena that have been attributed to mental entities, or that point to the existence of these entities, are exclusively caused by physiological factors. To be sure, several objections have been raised to materialist theories that do not assign some role to mental entities. But we will see that Quine is able to give convincing replies to these objections.
In this article, I analyze Quine?s conception of science, which is a radical defence of extensionalism on the grounds that first?order logic is the most adequate logic for science. I examine some criticisms addressed to it, which show the role of modalities and probabilities in science and argue that Quine?s treatment of probability minimizes the intensional character of scientific language and methods by considering that probability is extensionalizable. But this extensionalizing leads to untenable results in some cases and is not consistent with the fact that Quine himself admits confirmation which includes probability. Quine?s extensionalism does not account for this fact and then seems unrealistic, even if science ought to be extensional in so far as it is descriptive and mathematically expressible.
Section 1 is devoted to the study of countable recursively saturated models with an automorphism moving every non-algebraic point. We show that every countable theory has such a model and exhibit necessary and sufficient conditions for the existence of automorphisms moving all non-algebraic points. Furthermore we show that there are many complete theories with the property that every countable recursively saturated model has such an automorphism. In Section 2 we apply our main theorem from Section 1 to models of Quine's set theory New Foundations (NF) to answer an old consistency question. If NF is consistent, then it has a model in which the standard natural numbers are a definable subclass N of the model's set of internal natural numbers Nn. In addition, in this model the class of wellfounded sets is exactly $\bigcup_{n\in \mathbb{N}}\mathscr{P}^n(\varnothing)$.
IN Hilbert's theory of the foundations of any given branch of mathematics the main problem is to establish the consistency (of a suitable formalisation) of this branch. Since the (intuitionist) criticisms of classical logic, which Hilbert's theory was intended to meet, never even alluded to inconsistencies (in classical arithmetic), and since the investigations of Hilbert's school have always established much more than mere consistency, it is natural to formulate another general problem in the foundations of mathematics: to translate statements of theorems and proofs in the branch considered into those of some preferred system, where the translation must satisfy certain appropriate conditions (interpretation). The problem is relative to the choice of preferred system, as is Hilbert's consistency problem since he required the consistency to be established by particular methods (finitist ones). A finitist interpretation of classical number theory, which has been published in full detail elsewhere, is here described by means of typical examples. Partial results on analysis (theory of arbitrary functions whose arguments and values are the non-negative integers) are here presented for the first time. One of these results is restricted to functions whose values are bounded; its interest derives from the fact that real numbers may be represented by such functions. It is hoped that diverse general observations and comments, which would bore the specialist, may be of help to the general reader. The specialist may find some points of interest in the last two sections of the main text and in the notes following it.
Simple-type theory is widely regarded as inadequate to capture the metaphysics of mathematics. The problem, however, is not that some kinds of structure cannot be studied within simple-type theory. Even structures that violate simple-types are isomorphic to structures that can be studied in simple-type theory. In disputes over the logicist foundations of mathematics, the central issue concerns the problem that simple-type theory fails to assure an infinity of natural numbers as objects . This paper argues that the problem of infinity is based on a metaphysical prejudice in favor of numbers as objects — a prejudice that mathematics can get along without.
This paper re-addresses Quine's indeterminacy of translation/inscrutability of reference thesis, as a problem for cognitive theories of content. In contradistinction with Quine's behavioristic semantics, theories of meaning, or content, in the cognitivist tradition endorse intentional realism, and are prone to be unsympathetic to Quine's thesis. Yet, despite this fundamental difference, I argue that they are just as vulnerable to the indeterminacy. I then argue that the vulnerability is rooted in a theoretical commitment tacitly shared with Quine, namely, the commitment to the view that the perceptual input to the cognitive system is extensional - differentiating objects, but not the aspects (or, properties) they manifest. Thus, input extensionalism, and not behaviorism, is what forces the indeterminacy. I conclude by suggesting that the solution to Quine's indeterminacy problem hinges on the elaboration of an intensional theory of perceptual input, and of content in general.
We show that, if non-uniform impredicative stratified comprehension is assumed, Feferman's theories of explicit mathematics are consistent with a strong power type axiom. This result answers a problem, raised by Jäger. The proof relies upon an interpretation into Quine's set theory NF with urelements.
One of the key interpretative problems generated by the development of quantum theory was the conceptual consistency underlying scientific change, a problem not adequately treated by any of the leading theories of scientific development. In different but related ways Quine, Sellars, and Davidson have treated the problem of conceptual consistency by showing how one can begin with ordinary language and proceed to specialized extensions. Their techniques have not been applied to modern physics. However, one basis for applying them arises from the deep similarities between some of the work of these analysts and the Copenhagen interpretation rightly interpreted. To make this more concrete three concepts whose meanings have changed as a result of scientific progress are considered: 'atom', 'state of a system', and 'particle'. Each functions in a different way and requires a different type of analysis.
No categories
An ω-model (a model in which all natural numbers are standard) of the predicative fragment of Quine's set theory "New Foundations" (NF) is constructed. Marcel Crabbe has shown that a theory NFI extending predicative NF is consistent, and the model constructed is actually a model of NFI as well. The construction follows the construction of ω-models of NFU (NF with urelements) by R. B. Jensen, and, like the construction of Jensen for NFU, it can be used to construct α-models for any ordinal α. The construction proceeds via a model of a type theory of a peculiar kind; we first discuss such "tangled type theories" in general, exhibiting a "tangled type theory" (and also an extension of Zermelo set theory with Δ 0 comprehension) which is equiconsistent with NF (for which the consistency problem seems no easier than the corresponding problem for NF (still open)), and pointing out that "tangled type theory with urelements" has a quite natural interpretation, which seems to provide an explanation for the more natural behaviour of NFU relative to the other set theories of this kind, and can be seen anachronistically as underlying Jensen's consistency proof for NFU.
Discussion of Gian Aldo Antonelli, Extensional quotients for type theory and the consistency problem for NF
|
|
There are no threads in this forum |
Nothing in this forum yet.

