He leído que $ZFC$ y la lógica de primer orden podría formalizar todas las matemáticas, pero no puedo concebir que. En primer lugar, permítanme mostrarles lo que mi comprensión de $ZFC$ es.
He leído que $ZFC$ L a teoría donde L es el lenguaje formado con funciones, constantes y dos relaciones de $=$$\in$.
Uno puede agregar funciones de símbolos para hacer $ZFC$ más rico, por ejemplo, si $ZFC \vdash \forall x \forall y \exists ! z,F(x,y,z) $, uno puede crear el $ZFC+$ L+-teoría, donde L+ L a la que añadimos un símbolo de función f con arity 2, y, en $ZFC+$ $ZFC$ a la que añadimos las fórmulas $\forall x \forall y F(x,y,f(x,y)) $. Es fácil probar que para todo F L-fórmula que se cierran, tenemos $$ZFC\vdash F$$ if and only if we have $$ZFC+ \vdash F$$ And I think that for all L+-formula F, there is a L-formula F' such that $ZFC+ \bigcup \left\{F\right\}$ and $ZFC+ \bigcup \left\{F'\right\}$ are equivalent; or something like that, so we can work in everyday mathematics as if it were in ZFC, although we use symbols such as $\cos$, $\pecado$, $\emptyset$, $\left\{a,b\right\}$ y así sucesivamente.
Así, podemos introducir nuestro idioma $ZFC+$, pero, ¿cómo podemos pensar en una frase tan fácil $$(\star) \forall f \in \mathbb{C}^{\mathbb{N}}, \forall n \in \mathbb{N}, f(n) \in \mathbb{C}$$ Because, although we have introduced our function symbols for each $f$ (for example, taking the formulas $\forall x \existe ! y,(x\in \mathbb{N} \wedge (x,y) \in f) \vee (x\noen \mathbb{N} \wedge y=\emptyset )$ ), no tenemos un primer orden de la frase, o eso creo.
$\textbf{EDIT}$ : Es porque f aquí es un símbolo de una función. Por ejemplo, una de primer orden de la frase, como yo los entiendo, sería : $\forall f \in \mathbb{C}^{\mathbb{N}}, (f=f) \wedge (f \in f)$, porque aquí f es el símbolo de una variable.
Es posible formalizar la sentencia de $(\star)$ con un primer orden de la frase ? Me estoy perdiendo algo ?
Respuestas
¿Demasiados anuncios?
Cuando la construcción de las matemáticas de la teoría de conjuntos ($\mathsf{ZFC}$, si te gusta), tenemos que tomar decisiones acerca de cómo las cosas en el universo matemático están codificados. Este es un muy laboriosa tarea. Consideremos el caso simple de la función de un conjunto a otro.
Por lo general, hacemos la decisión de que la función de $f$ está definido para ser su gráfica; el conjunto de todos los pares ordenados $\langle x , y \rangle$ tal que $f(x) = y$. Por supuesto, también tenemos que determinar lo que un par ordenado es. El común de la actual convenio es definir el par ordenado $\langle x , y \rangle$ a ser el conjunto de $\{ \{ x \} , \{ x , y \} \}$. Podemos mostrar que esta determinación obedece a las propiedades básicas esperamos ser cierto acerca de los pares ordenados (a saber, que $\langle x , y \rangle = \langle u , v \rangle$ fib $x=u$$y=v$).
Así que, dado que dos conjuntos de $X , Y$, ¿cómo podemos determinar que algunos de $f$ es una función de$X$$Y$? Bien, aquí están algunos pasos:
- cada elemento de a $f$ debe ser un par ordenado de la forma $\langle x,y \rangle$ donde$x \in X$$y \in Y$; y
- cada elemento de a $X$ debe ser la primera coordenada de exactamente un elemento de $f$.
Poner esto en primer orden de los términos:
- $( \forall u ) ( u \in f \rightarrow ( \exists x ) ( \exists y ) ( x \in X \wedge y \in Y \wedge u = \langle x , y \rangle ) )$ (donde esta última parte es en realidad una abreviatura para $( \forall a ) ( a \in u \leftrightarrow ( ( \forall v ) ( v \in a \leftrightarrow v = x ) \vee ( \forall v ) ( v \in a \leftrightarrow ( v = x \vee v = y ) ) ) )$); y
- $( \forall x ) ( x \in X \rightarrow ( \exists y ) ( \forall z ) ( ( \exists u ) ( u \in f \wedge u = \langle x , z \rangle ) \leftrightarrow z = y ) )$.
Así que tenemos una descripción en el lenguaje de la teoría de lo que es una función entre dos conjuntos. $\mathsf{ZFC}$ tiene ciertos axiomas que nos permite proclamar que, dada $X , Y$ hay un conjunto $Y^X$ de todas las funciones $X \to Y$, y luego se puede cuantificar a través de este conjunto: el uso de $( \forall f \in Y^X ) \phi$ como una abreviatura para $( \forall f ) ( f \in Y^X \rightarrow \phi )$. (Para ser perfectamente honesto, diciendo: $f \in Y^X$ puede ser visto como una abreviatura para la conjunción de las dos fórmulas dadas arriba.)
Aunque es muy importante, esta fue una bastante simple paso en el largo proceso de formalización "la matemática real" dentro de la teoría de conjuntos. (Por ejemplo, todavía tenemos que construir los conjuntos de $\mathbb{R} , \mathbb{C}$ reales y los números complejos.)
Respuesta a los comentarios de abajo
Usted no será capaz de encontrar una fórmula única que será el de la onu-abreviatura de $u = \{ x_1 , \ldots , x_n \}$ para todos los posibles conjuntos en el lado derecho. En su lugar vamos a crear un esquema que nos permite construir el requisito de fórmulas de forma recursiva.
En su base el nivel de $u = \{ x_1 , \ldots , x_n \}$ es una abreviatura para $$( \forall v ) ( v \in u \leftrightarrow ( v = x_1 \vee \cdots \vee x_n ))$$ (where it is clear what the formula will look like for each $n$). Depending on that set on the right-hand-side (if it is given to us explicitly) we may also un-abbreviate each $v = x_i$. For the abbreviation you have given $u = \{ \varnothing, \{ \varnothing , \{ \varnothing \} \} \}$ trabajamos así:
- en la base de paso, esta es una abreviatura para $$( \forall v ) ( v \in u \leftrightarrow ( v = \varnothing \vee v = \{ \varnothing , \{ \varnothing \} \} ) ); \tag{1}$$
- tomando nota de que $v = \{ \varnothing , \{ \varnothing \} \}$ es una abreviatura para $( \forall w ) ( w \in v \leftrightarrow ( w = \varnothing \vee w = \{ \varnothing \} ) )$, podemos conectarlo en (1), produciendo $$( \forall v ) ( v \in u \leftrightarrow ( v = \varnothing \vee ( \forall w ) ( w \in v \leftrightarrow ( w = \varnothing \vee w = \{ \varnothing \} ) ) ) ); \tag{2}$$
- destacar nuevamente que $w = \{ \varnothing \}$ es una abreviatura para $( \forall y ) ( y \in w \leftrightarrow y = \varnothing )$ sustituimos esto en (2), dando $$( \forall v ) ( v \in u \leftrightarrow ( v = \varnothing \vee ( \forall w ) ( w \in v \leftrightarrow ( w = \varnothing \vee ( \forall y ) ( y \in w \leftrightarrow y = \varnothing ) ) ) ) ); \tag{3}$$
- por último destacar, ya que usted tiene, ese $x = \varnothing$ es una abreviatura para $( \forall z ) ( z \notin x )$, que conecta todos los esenciales instancias de este en (3), resultando en $$\begin{multline}( \forall v ) ( v \in u \leftrightarrow ( ( \forall z ) ( z \notin v ) \vee ( \forall w ) ( w \in v \leftrightarrow \\ \leftrightarrow ( ( \forall z ) ( z \notin w ) \vee ( \forall y ) ( y \in w \leftrightarrow ( \forall z ) ( z \notin y ) ) ) ) ) )\end{multline} \tag{4}$$
Como se puede ver, (4) un poco difícil de manejar para trabajar con directamente o incluso de comprender si se acaba de dar, directamente, que es el único punto de venir para arriba con las abreviaturas.
Usted podría ampliar el lenguaje de la teoría de conjuntos para incluir todas estas abreviaturas, y también extender $\mathsf{ZFC}$ para incluir a todos los de la definición de fórmulas. Este va a ser un conservador de extensión, lo que significa que en las mismas penas en la onu-idioma expandido será teoremas en cada una de las $\mathsf{ZFC}$$\mathsf{ZFC}+\text{(all definitions)}$. Pero el punto de todo esto es que uno no tiene para expandir el lenguaje. Se le preguntó acerca de la formalización de las matemáticas dentro de $\mathsf{ZFC}$, y esto se puede hacer, aunque no de una manera agradable.
Más al punto, si no hubo definiciones de estos nuevos símbolos dentro de$\mathsf{ZFC}$, entonces no habría ninguna garantía de que dicha prórroga fue conservador (o tal vez incluso significante).
Cuando nos formalizar la matemática en $\sf ZFC$ nosotros no añadir nuevos símbolos para el lenguaje de la teoría de conjuntos.
El significado es que podemos utilizar sets de el universo de $\sf ZFC$ a codificar las operaciones y los símbolos de los idiomas con los que queremos trabajar, y podemos formalizar la declaración de "$M$ $\cal L$- estructura".
Ahora en $\sf ZFC$ sí podemos cuantificar sobre las funciones, sobre los conjuntos de $M$, y así sucesivamente. Porque esos son todos los elementos del universo de la teoría de conjuntos. Y a la afirmación "Cada conjunto acotado de números reales tiene un $\sup$" es ahora una de primer orden de declaración en $\sf ZFC$, porque lo que realmente dice algo como esto:
Cada set, lo cual es un subconjunto de un conjunto subyacente de una estructura de codificación del campo de los números reales y a es acotado por arriba, tiene al menos un límite superior.
Reiterar el punto que estoy tratando de hacer todo a lo largo de aquí.
Cuando se utiliza $\sf ZFC$ como fundacional de la teoría de las matemáticas, uno no se extiende el lenguaje de la teoría de conjuntos. Y si uno se decide a hacerlo, entonces se añade la constante de símbolos para $\Bbb{N,R,C}$ y así sucesivamente. Las constantes que se interpretan como se establece en el universo de la teoría de conjuntos.
Por lo tanto, la declaración de $\forall f\in\Bbb{C^N}\ldots$ es de hecho un primer orden de instrucción en el lenguaje de la teoría de conjuntos que son la constante de símbolos $\Bbb{C,N}$ y un operador de exponenciación.
Cabe señalar que cualquier adición al lenguaje de la teoría de conjuntos es un conservador de la extensión de la lengua. Rara vez agregar cosas que son indefinible. Por ejemplo, $\subseteq,\mathcal P,\times,\cup$ son definidos por las relaciones y las operaciones sobre conjuntos. Por lo tanto, la adición de ellos es sólo una cuestión de conveniencia y le permite traducir fácilmente cualquier declaración en una declaración sin el uso de estos símbolos, que va a ser muy largo y no se puede leer.
$$(\star) \forall f \in \mathbb{C}^{\mathbb{N}}, \forall n \in \mathbb{N}, f(n) \in \mathbb{C}$ $ no es una fórmula bien formada en la lógica de primer orden, pero lo que significó fue lo que se entiende por la siguiente fórmula bien formada en la lógica de primer orden en el lenguaje de una teoría$ZFC ++...+$ PS
