Sí, vale la pena el esfuerzo. Un predicativo versión de un impredicative de la construcción es típicamente más explícito y más informativa que la impredicative uno. Por ejemplo, considerar la construcción de un subgrupo de $\langle S \rangle$ de un grupo de $G$ generado por el conjunto de $S$:
- impredicative: $\langle S \rangle$ es la intersección de todos los subgrupos de $G$ que contengan $S$.
- predicativo: $\langle S \rangle$ se compone de todos finito de combinaciones de elementos de $S$ y sus inversos, es decir, un típico elementos es $x_1 x_2 \cdots x_n$ donde $x_i \in S \cup S^{-1}$.
Esto puede ser bastante útil si desea calcular con grupos (es decir, con un ordenador), como definitivamente prefiero la segunda descripción, que le dice exactamente cómo los elementos del subgrupo puede ser representado.
Muchos ejemplos de impredicative construcciones son casos especiales de la siguiente teorema.
Teorema (Knaster y Tarski): Una voz un mapa completo de la celosía tiene al menos un punto fijo por encima de cada punto.
Tomar dos de sus ejemplos:
Subgrupo generado por un conjunto: el enrejado es el powerset $P(G)$ de la $G$ en cuestión, y el mapa de $f : P(G) \to P(G)$ es de $S \subseteq G$ a $f(S) = S \cup S^{-1} \cup S \cdot S$.
$\sigma$-álgebra generada por una familia de subconjuntos: el ejercicio.
Hay dos maneras estándar de la prueba de la Knaster-teorema de Tarski, uno impredicative y un predicativo. Estos ejemplifican los dos enfoques generales de llegar a los objetos deseados "impredicatively desde arriba" y "predicatively desde abajo".
El impredicative prueba es como sigue: llame a un punto de $x$ un prefijo punto si $f(x) \leq x$. Consideremos el conjunto $S$ de todo el prefijo puntos por encima de un punto dado, $y$ (que no es vacío, ya que contiene la parte superior de la rejilla). El menor punto fijo por encima de $y$ es el infimum $x = \inf S$ (ejercicio).
El predicativo prueba es como sigue: iterar $f$ a partir de un determinado punto de $y$ a la construcción de un aumento de la secuencia $$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$.
Por supuesto, en la generalidad de los predicativo prueba es apenas mejor que la impredicative porque hemos sustituido uno no descripción con otro. Pero, en determinados casos, puede que sepamos algo acerca de $f$. Por ejemplo, podemos saber que se conserva suprema de contables de las cadenas, como hacemos en el ejemplo de un subgrupo generado por un conjunto, en cuyo caso la iteración se detiene en $\omega$.
Su tercer ejemplo, a saber, el componente conectado de un punto, puede ser tratada también, pero no estoy seguro de que es mejor que la impredicative construcción:
- Los componentes conectados: el componente conectado de un punto es un máximo conectado subconjunto contiene. Usted probablemente está pensando en la construcción de la que dice "tomar sólo la unión de todos los conectados subconjuntos que contienen el punto". En su lugar, podríamos tratar el siguiente: definir $x \sim y$ significa que para todas continua $f : X \to 2$, $f(x) = f(y)$. Los componentes conectados de $X$ son las clases de equivalencia de $\sim$. Por lo tanto, el componente conectado de un punto es sólo su clase de equivalencia. Esto no es del todo satisfactorio, ya que sustituye a una mala descripción con otro. Se puede ser más explícito? Lo que si tenemos una buena base para el espacio?
En algún momento usted tiene que reformular todo el tema para alejarse de builtin impredicativity (y es todavía vale la pena hacerlo porque le da computacional significado de los teoremas que son bastante no-computacional en la impredicative configuración):
- Cierre/interior de un conjunto: en virtud de la clásica formulación de la topología a veces, usted puede conseguir lejos con predicativo de la construcción, por ejemplo, si usted puede reducir su construcción a la manipulación de una contables topológico, como por ejemplo el interior de $S \subseteq \mathbb{R}$ es la unión de todos los intervalos abiertos con racional de los extremos que figuran en el $S$. Generales de las formulaciones de la topología, como formal topología y Abstracto de Piedra de la Dualidad, que evite impredicative construcciones por completo.
Por último, mencionar Dedekind integridad de reales. No estoy seguro de que este es impredicative. El supremum de un no vacío acotado a la familia de lado izquierdo Dedekind cortes es simplemente su unión. ¿Qué es impredicative acerca de la toma de la unión de una familia de recortes?
Adendum: tenga en cuenta que en el caso típico es el de la construcción, es decir, la existencia de la prueba, que es predicativo o impredicative, no la definición. Por ejemplo, el grupo generado por un conjunto se define como el menor subgrupo que contiene los generadores, que no tiene nada que con predicativity/impredicativity.
P. S. Usted necesita un mejor MO nombre de usuario.
