E. J. Lowe; Impredicative identity criteria and Davidson's criterion of event identity, Analysis, Volume 49, Issue 4, 1 October 1989, Pages 178–181, https://doi.

In this paper, a general perspective on criteria of identity of kinds of objects is developed. The question of the admissibility of impredicative or circular identity criteria is investigated in the light of the view that is articulated. It is argued that in and of itself impredicativity does not constitute sufficient grounds for rejecting a putative identity criterion. The view that is presented is applied to Davidson’s criterion of identity for events and to the structuralist criterion of identity of (...) places in a structure. (shrink)

Thought: A Journal of Philosophy, EarlyView.

A definition of a property P is impredicative if it quantifies over a domain to which P belongs. Due to influential arguments by Ramsey and Gödel, impredicative mathematics is often thought to possess special metaphysical commitments. It seems that an impredicative definition of a property P does not have the intended meaning unless P already exists, suggesting that the existence of P cannot depend on its explicit definition. Carnap (1937 [1934], p. 164) argues, however, that accepting impredicative definitions amounts to (...) choosing a "form of language" and is free from metaphysical implications. This paper explains this view in its historical context. I discuss the development of Carnap’s thought on the foundations of mathematics from the mid-1920s to the mid-1930s, concluding with an account of Carnap’s (1937 [1934]) non-Platonistic defense of impredicativity. This discussion is also important for understanding Carnap’s influential views on ontology more generally, since Carnap’s (1937 [1934]) view, according to which accepting impredicative definitions amounts to choosing a "form of language", is an early precursor of the view Carnap presents in "Empiricism, Semantics and Ontology" (1956 [1950]), according to which referring to abstract entities amounts to accepting a "linguistic framework". (shrink)

Gödel and others held that impredicative specification is illegitimate in a constructivist framework but legitimate elsewhere. Michael Dummett argues to the contrary that impredicativity, though not necessarily illicit, needs justification regardless of whether one assumes the context is realist or constructivist. In this paper I defend the Gödelian position arguing that Dummett seeks a reduction of impredicativity to predicativity which is neither possible nor necessary. The argument is illustrated by considering first highly predicative versions of the equinumerosity axiom (...) for cardinal number and Axiom V for sets, on the one hand, then classically consistent disjunctivised versions of Axiom V which are impredicative but can prove the well-foundedness of the semantics of weaker such systems, on the other. (shrink)

Bob Hale has defended a new conception of properties that is broadly Fregean in two key respects. First, like Frege, Hale insists that every property can be defined by an open formula. Second, like Frege, but unlike later definabilists, Hale seeks to justify full impredicative property comprehension. The most innovative part of his defense, we think, is a “definability constraint” that can serve as an implicit definition of the domain of properties. We make this constraint formally precise and prove that (...) it fails to characterize the domain uniquely. Thus, we conclude, there is no easy road to impredicative definabilism. (shrink)

Gödel and others held that impredicative specification is illegitimate in a constructivist framework but legitimate elsewhere. Michael Dummett argues to the contrary that impredicativity, though not necessarily illicit, needs justification regardless of whether one assumes the context is realist or constructivist. In this paper I defend the Gödelian position arguing that Dummett seeks a reduction of impredicativity to predicativity which is neither possible nor necessary. The argument is illustrated by considering first highly predicative versions of the equinumerosity axiom (...) for cardinal number and Axiom V for sets, on the one hand, then classically consistent disjunctivised versions of Axiom V which are impredicative but can prove the well-foundedness of the semantics of weaker such systems, on the other. (shrink)

In reverse mathematics, it is possible to have a curious situation where we know that an implication does not reverse, but appear to have no information on how to weaken the assumption while preserving the conclusion (other than reducing all the way to the tautology of assuming the conclusion). A main cause of this phenomenon is the proof of a $\Pi^1_2$ sentence from the theory $\mathbf{\Pi^{\textbf{1}}_{\textbf{1}}-CA_{\textbf{0}}}$. Using methods based on the functional interpretation, we introduce a family of weakenings of $\mathbf{\Pi^{\textbf{1}}_{\textbf{1}}-CA_{\textbf{0}}}$ (...) and use them to give new upper bounds for the Nash-Williams Theorem of wqo theory and Menger's Theorem for countable graphs. (shrink)

An instance of Stratified Comprehension ∀x₁ … ∀x n ∃y∀x (x ∈ y ↔ φ(x, x₁, …, x n )) is called strictly impredicative iff, under minimal stratification, the type of x is 0. Using the technology of forcing, we prove that the fragment of NF based on strictly impredicative Stratified Comprehension is consistent. A crucial part in this proof, namely showing genericity of a certain symmetric filter, is due to Robert Solovay. As a bonus, our interpretation also satisfies some (...) instances of Stratified Comprehension which are not strictly impredicative. For example, it verifies existence of Frege natural numbers. Apparently, this is a new subsystem of NF shown to be consistent. The consistency question for the whole theory NF remains open (since 1937). (shrink)

We study constructive set theories, which deal with operations applying both to sets and operations themselves. Our starting point is a fully explicit, finitely axiomatized system ESTE of constructive sets and operations, which was shown in 10 to be as strong as PA. In this paper we consider extensions with operations, which internally represent description operators, unbounded set quantifiers and local fixed point operators. We investigate the proof theoretic strength of the resulting systems, which turn out to be impredicative . (...) © 2011 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim. (shrink)

This paper extends the results of an earlier paper by the author . New subsystems of the combinatory logic TRC shown in that paper to be equivalent to NF are introduced; these systems are analogous to subsystems of NF with predicativity restrictions on set comprehension introduced and shown to be consistent by Crabbé. For one of these systems, an exact equivalence in consistency strength and expressive power with the analogous subsystem of NF is established.

We define a realizability interpretation of Aczel's Constructive Set Theory CZF into Explicit Mathematics. The final results are that CZF extended by Mahlo principles is realizable in corresponding extensions of T 0 , thus providing relative lower bounds for the proof-theoretic strength of the latter.

The proofs of universally quantified statements, in mathematics, are given as “schemata” or as “prototypes” which may be applied to each specific instance of the quantified variable. Type Theory allows to turn into a rigorous notion this informal intuition described by many, including Herbrand. In this constructive approach where propositions are types, proofs are viewed as terms of λ-calculus and act as “proof-schemata”, as for universally quantified types. We examine here the critical case of Impredicative Type Theory, i. e. Girard's (...) system F, where type-quantification ranges over all types. Coherence and decidability properties are proved for prototype proofs in this impredicative context. (shrink)