Bourbaki ' notación épsilon-cálculo de s

Question

Bourbaki utiliza una muy, muy extraño notación para el epsilon-cálculo consta de $\tau$s y $\blacksquare$. De hecho, esa caja no debe ser rellenado, pero por alguna razón, yo no puedo producir un \Cuadro.

De todos modos, me preguntaba si alguien podría explicarme lo de los vínculos de vuelta a la tau decir, lo que los cuadros de media. Cuando leí el libro, puedo reemplazar el $\tau$s de Hilbert $\varepsilon$s. Quiero decir, que fui a un montón de problemas para el uso de esta notación, por lo que debe significar algo trivial, ¿verdad?

Usted puede ver en la primera página de la búsqueda de libros de google enlace que he publicado. No estoy seguro de si se supone que es intencionalmente vaga, pero nunca introducir cualquier metamathematical normas para tratar con vínculos a excepción de los criterios de sustitución, lo que casi no puede interactuar con $\tau$ términos.

También, por supuesto, ya que es un libro escrito para ser completamente un dolor en el cuello a leer, utilizar un cálculo de hilbert, y peor aún, sin la primitiva igualdad para determinar si dos conjuntos son equivalentes.

Answer 1

Permítanme hablar de la parte de la pregunta acerca de "lo que los vínculos de vuelta a la tau decir, lo que los cuadros de decir." La notación habitual para el uso de Hilbert símbolo de epsilon es que uno escribe $(\varepsilon x)\phi(x)$ a significar "algunos (no especificado) $x$ satisfacción $\phi$ (si existe uno, y un objeto cualquiera otra cosa)." Si, como Bourbaki, uno quiere evitar cuantificadores en el boletín oficial de la notación y uso de $\varepsilon$ lugar (en concreto, expresando $(\exists x)\phi(x)$$\phi((\varepsilon x)\phi(x))$), entonces no trivial fórmula contendrá un montón de $\varepsilon$'s, aplicado a un montón de variables, todos anidar juntos en un complejo desorden. Para reducir un poco la complicación, me permiten suponer que las variables vinculadas se han cambiado de nombre para que cada aparición de $\varepsilon$ utiliza una variable diferente. Bourbaki la notación (incluso más complicado, en mi opinión) es lo que tendría que hacer lo siguiente para cada ocurrencia de $\varepsilon$ en la fórmula. (1) Reemplazar esta $\varepsilon$$\tau$. (2) Borrar la variable que sale a la derecha después de la $\varepsilon$. (3) Reemplazar todas las apariciones posteriores de esa variable con un cuadro. (4) Enlace de cada una de esas cajas a la $\tau$ usted escribió en (1). Por lo $(\varepsilon x)\phi(x)$ hace $\tau\phi(\square)$ con un enlace desde el $\tau$ a las cajas (como tantas cajas como las que existían $x$'s $\phi(x)$).

Uno podría preguntarse por qué Bourbaki hace todo esto. Hasta donde yo sé, el punto de las cajas y de los vínculos, es que no hay variables vinculadas en el boletín oficial de la notación; todos ellos han sido sustituidos por cuadros. Así que Bourbaki no necesita definir cosas como libre y unida apariciones de una variable. Donde yo (y casi todos los demás) diría que una variable se produce libre en una fórmula, Bourbaki puede simplemente decir que la variable se produce en la fórmula.

Sospecho que Bourbaki eligió para el uso de Hilbert $\varepsilon$ operador como una forma inteligente de conseguir el axioma de elección y la lógica de los cuantificadores todos a la vez. Y no tengo idea de por qué se cambió $\varepsilon$ $\tau$(a pesar de que, al escribir esta respuesta, me di cuenta de que me gustaría mucho más el tipo de tau que varepsilon).

Answer 2

Matías polémicas son divertidos en los puntos, pero también engañosa en varios aspectos:

1. ZFC también tiene un enorme longitud y profundidad de las deducciones por trivial material. Según Norman Megill del metamath página, "completar la prueba de que 2 + 2 = 4 implica 2,452 subtheorems incluyendo los 150 [profundidad de la prueba de árbol]. ... Estos tienen un total de 25,933 pasos - esta es la cantidad de pasos que tendría que examinar si quería verificar la prueba con la mano en el detalle completo de todo el camino de regreso a los axiomas." Megill del sistema se basa en un formalismo para sustituciones por lo que puede ser un gran ahorro en comparación con la forma en la que Matías realiza la cuenta (es decir, el pleno ampliado el tamaño de los símbolos) para Bourbaki del sistema. Si yo correctamente recordar otra información de Megill acerca de la prueba de longitud se calcula para varios resultados en ZFC, el número de símbolos necesarios pueden ser órdenes de magnitud más grande y esto es lo que debe ser comparado con Matías números.

2. La prueba tamaños son enormemente dependientes de la implementación. Bourbaki prueba de longitud podría ser una cuestión de no esenciales de las decisiones de diseño. Matías reclamaciones en la final del artículo que hay un problema con el uso de Hilbert epsilon-notación para incompleta o indecidible sistemas, pero él no da ninguna indicación de que este o cualquier otro problema que es insuperable en la Bourbaki enfoque.

3. De hecho, Matías mismo parece haber superado el problema en sus otros papeles, expresando Bourbaki la teoría de conjuntos como un subsistema de ZFC. Así que él ya ha demostrado que algunos razonablemente potente subsistemas de ZFC tiene pruebas y definiciones que conseguir radicalmente más corto después de la adición de Reemplazo, o que el enorme "término" que él atribuye a la Theorie des Conjuntos se reduce a una más ZFC-como el tamaño cuando se implementa en un marco diferente.

EDIT. Una búsqueda de Norman Megill los cálculos de la prueba de los tramos en ZFC encontrado el siguiente:

"incluso trivial pruebas requieren un asombroso número de pasos directamente a partir de los axiomas. La existencia de la conjunto vacío puede ser comprobado con 11,225,997 pasos y recursión transfinita puede ser comprobado con 11,777,866,897,976 pasos."

y

"Las pruebas a las que sólo existen en principio, por supuesto, pero su las longitudes se backcomputed de lo que sería el resultado de más tradicional las pruebas eran completamente expandida. ..... En la versión actual de mi prueba base de datos que ha sido reorganizado un poco, los números son:

conjunto vacío = 6,175,677 pasos

transf. rec. = 24,326,750,185,446 pasos"

Eso es sólo el número de pasos. El número de símbolos sería mucho, mucho más.

Answer 3

Me gustaría simplemente mencionar sobre "lo que los vínculos a la media de tau, lo que significan que las cajas", que esta notación ha sido revisitada por Nicolaas Govert de Bruijn en el marco del cálculo lambda y en gran parte se utiliza en informática teórica como una herramienta muy conveniente y es conocida ahora como "de Bruijn" índices. Una literatura se puede encontrar acerca de esto.

Answer 4

Usted debe leer el encanto de ensayo que se burlaban de este tipo de notación, además de dar un minucioso análisis lógico de la misma, por Adrian Mathias.

• Adrian Mathias, Un Plazo de Duración 4,523,659,424,929, Synthese 133 (2002) 75--86

Él lo describe así:

Un cálculo del número de símbolos necesarios para dar Bourbaki la definición del número 1; a lo cual debe agregarse 1,179,618,517,981 disambiguatory enlaces. Las implicaciones para Bourbaki filosóficos de las reclamaciones y la salud mental de sus lectores se discuten.