Impredicativity - MathOverflow most recent 30 from http://mathoverflow.net 2013-05-25T10:32:13Z http://mathoverflow.net/feeds/question/26220 http://www.creativecommons.org/licenses/by-nc/2.5/rdf http://mathoverflow.net/questions/26220/impredicativity Impredicativity dumb student 2010-05-28T02:43:23Z 2010-05-28T19:54:38Z <p>I hope this question is not so elementary that it'll get me banned...</p> <p>In mathematics we see a lot of impredicativity. Example of definitions involving impredicativity include: subgroup/ideal generated by a set, closure/interior of a set (in topology), topology generated by a family of sets, connected/path connected component of a point, sigma algebra generated by a family... And of course, the least upper bound property of real numbers. Impredicativity flood mathematics but there are people who don't like it. I think type theory was developed due the paradoxical and impredicative nature of "set of all sets that don't contain themselves".</p> <p>I'm very ignorant on this and from what I read type theory is hopeless complicated to work this, so I ask the people who favor predicativism: all those people have fiddled with mathematics for all those years and no one ever found a contradiction (I mean in ZFC), so is it worth all that effort?</p> http://mathoverflow.net/questions/26220/impredicativity/26233#26233 Answer by Andrej Bauer for Impredicativity Andrej Bauer 2010-05-28T06:22:36Z 2010-05-28T09:20:29Z <p>Yes, it is worth the effort. A predicative version of an impredicative construction is typically more explicit and informative than the impredicative one. For example, consider the construction of a subgroup $\langle S \rangle$ of a group $G$ generated by the set $S$:</p> <ul> <li><strong>impredicative</strong>: $\langle S \rangle$ is the intersection of all subgroups of $G$ which contain $S$.</li> <li><strong>predicative</strong>: $\langle S \rangle$ consists of all finite combinations of elements of $S$ and their inverses, i.e., a typical elements is $x_1 x_2 \cdots x_n$ where $x_i \in S \cup S^{-1}$.</li> </ul> <p>This can be quite useful if you want to compute with groups (i.e., with a computer), as you will definitely prefer the second description, which tells you how exactly the elements of the subgroup can be represented.</p> <p>Many examples of impredicative constructions are special cases of the following theorem.</p> <blockquote> <p><strong>Theorem</strong> (Knaster and Tarski): <em>A monotone map on a complete lattice has a least fixed-point above every point.</em></p> </blockquote> <p>To take two of your examples:</p> <ul> <li><p><em>Subgroup generated by a set</em>: the complete lattice is the powerset $P(G)$ of the group $G$ in question, and the map $f : P(G) \to P(G)$ takes $S \subseteq G$ to $f(S) = S \cup S^{-1} \cup S \cdot S$.</p></li> <li><p><em>$\sigma$-algebra generated by a family of subsets</em>: exercise.</p></li> </ul> <p>There are two standard ways of proving the Knaster-Tarski theorem, one impredicative and one predicative. These exemplify the two general approaches of getting to desired objects "impredicatively from above" and "predicatively from below".</p> <p>The impredicative proof goes as follows: call a point $x$ a <em>prefixed</em> point if $f(x) \leq x$. Consider the set $S$ of all prefixed points above a given point $y$ (which is not empty as it contains the top of the lattice). The least fixed-point above $y$ is the infimum $x = \inf S$ (exercise).</p> <p>The predicative proof goes as follows: iterate $f$ starting with a given point $y$ to construct an increasing sequence $$y, f(y), f^2(y), \ldots, f^\omega(y), \ldots, f^\alpha(y), \ldots$$ where we have to iterate through ordinals until we're blue in the face. The iteration stops eventually, and that's the least fixed-point above $y$.</p> <p>Of course, in such generality the predicative proof is hardly better than the impredicative one because we replaced one non-description with another. But in particular cases we might know something about $f$. For example, we might know that it preserves suprema of countable chains, as we do in the example of a subgroup generated by a set, in which case the iteration stops at $\omega$.</p> <p>Your third example, namely the connected component of a point, can be dealt with also, but I am not sure it's any better than the impredicative construction:</p> <ul> <li><em>Connected components</em>: the connected component of a point is a maximal connected subset containing it. You are probably thinking of the construction that says "just take the union of all connected subsets that contain the point". We could instead try the following: define $x \sim y$ to mean that for all continuous $f : X \to 2$, $f(x) = f(y)$. The connected components of $X$ are the equivalence classes of $\sim$. Therefore the connected component of a point is just its equivalence class. This is not entirely satisfactory as it replaces one bad description with another. Can we be more explicit? What if we have a nice basis for the space?</li> </ul> <p>Sometime you have to reformulate the whole subject to get away from builtin impredicativity (and it is still worth doing because it gives computational meaning to theorems which are quite non-computational in the impredicative setting):</p> <ul> <li><em>Closure/interior of a set</em>: under classical formulation of topology you can sometimes get away with predicative construction, for example if you can reduce your construction to manipulation of a countable topological basis, e.g. the interior of $S \subseteq \mathbb{R}$ is the union of all open intervals with rational endpoints that are contained in $S$. There are general formulations of topology, such as <a href="http://www.cs.chalmers.se/~coquand/formal.html" rel="nofollow">formal topology</a> and <a href="http://www.paultaylor.eu/ASD/" rel="nofollow">Abstract Stone Duality</a>, which avoid impredicative constructions altogether.</li> </ul> <p>Lastly, you mention Dedekind completeness of reals. I am not sure this is impredicative. The supremum of a non-empty bounded family of left-sided Dedekind cuts is simply their union. What is impredicative about taking the union of a family of cuts?</p> <p><strong>Adendum</strong>: Note that in the typical case it is the <strong>construction</strong>, i.e., an existence proof, which is predicative or impredicative, not the definition. For example, the group generated by a set is <em>defined</em> as the least subgroup containing the generators, which has nothing to to with predicativity/impredicativity.</p> <p>P.S. You need a better MO username.</p> http://mathoverflow.net/questions/26220/impredicativity/26254#26254 Answer by Neel Krishnaswami for Impredicativity Neel Krishnaswami 2010-05-28T12:46:19Z 2010-05-28T12:46:19Z <p>Andrej's answer is great, but I want to elaborate on one point: often, there are multiple, incompatible, ways to strengthen a formalism. Developing a piece of mathematics using relatively weak techniques is a form of "insurance": it will be portable regardless of how you go about strengthening the formalism in the future. </p> <p>In particular, there are actually <em>multiple</em> ways of formalizing the idea we call "impredicativity". </p> <p>Concretely, there are type theories (such as System F) which support what we can call "impredicative indexing" -- that is, we can define types by indexing over all types, such as the type $\forall \alpha:\mathrm{Type}. \alpha \to \alpha$, which is the type of endofunctions which work at arbitrary types. For obvious size reasons, such a construction in Set is not possible. However, such types (and their formation and elimination rules) formalize an idea of Carnap's, which is that even apparently circular impredicative definitions can't possibly get you into logical trouble if you use the totality you quantify over in a purely schematic way.[1] </p> <p>On the other hand, set theory has the powerset axiom, which gives you a different form of impredicativity (which Andrej used in his sketch of the proof of the Knaster-Tarski theorem). These two forms of impredicativity are incompatible with each other[2], but they both embody natural formalizations of the idea of impredicativity.[3] </p> <p>Predicative arguments are ported easily to both type theory (say, for verification in a proof assistant) and to set theory (say, for verification by a grad student) -- but the excessive use of powerset or parametricity axioms will make the porting job a lot harder!</p> <ol> <li>See Fruchhart and Longo's "Carnap's Remarks on Impredicative Definitions and the Genericity Theorem"</li> <li>See Andrew Pitts' "Non-trivial Power Types Can't be Subtypes of Polymorphic Types"</li> <li>As an aside, I find this one of the major annoyances of programming language research; we frequently need F-style impredicativity, but models of F in ordinary mathematics require building structures sufficiently exotic that F's functions in that model "differ enough" from Set's functions. This calls for techniques that feel rather more high-powered than ought to be necessary...</li> </ol> http://mathoverflow.net/questions/26220/impredicativity/26263#26263 Answer by Carl Mummert for Impredicativity Carl Mummert 2010-05-28T13:36:24Z 2010-05-28T13:45:27Z <p>Andrej Bauer points out that predicative constructions are more explicit, and give more useful computational information, than impredicative ones. This has two further consequences that are of interest. I want to point these out as an answer to the implicit question asked by "alephomega".</p> <ol> <li><p>If a theorem about reasonable objects can be proven predicatively, this gives important information on the consistency strength (i.e. the proof-theoretic ordinal) associated with the theorem. Conversely, we know that some theorems such as Kruskal's theorem cannot be proven predicatively because these theorems lead to proof-theoretic ordinals that are too large. Thus the mathematical analysis of predicativity <i>reveals</i> the full complexity of results such as Kruskal's theorem, rather than obscuring it. This is separate from the philosophical analysis of predicativity. </p></li> <li><p>The "computability" consequences of a predicative proof can be extremely important. In the context of a countable group $G$, a "top-down" construction such as "intersect all subgroups of $G$ that contain the set $X$" will only naively give that the constructed object is $\Pi^1_1$ over $G\oplus X$. A bottom-up construction will usually show that the constructed object is actually arithmetical in $G\oplus X$. Examination of the bottom-up proof can then give explicit bounds in the arithmetical hierarchy on the complexity of the constructed object. For example, in the case of a subgroup of a group $G$ generated by a subset $X$, the degree of the subgroup is no more than the Turing jump of $G \oplus X$; this is an enormously better bound than the naive $\Pi^1_1$ result. </p></li> </ol> http://mathoverflow.net/questions/26220/impredicativity/26303#26303 Answer by Christoph-Simon Senjak for Impredicativity Christoph-Simon Senjak 2010-05-28T19:54:38Z 2010-05-28T19:54:38Z <p>Type Theory is worthwile alone for its practical applications. So if you dont like it as a foundation of mathematics, accept it as applied mathematics.</p> <p>On the other hand, predicative definitions are a mostly clearer and easier to understand, and if you look at most algebra-books, whenever there is a short impredicative definition given, you will have at least three lemmata or theorems proving the equivalence with some predicative property. Its questionable why to have this impredicative definitions at first sight then.</p>