Notación del cálculo épsilon de Bourbaki

Question

Bourbaki utilizó una notación muy muy extraña para el épsilon-cálculo consistente en $\tau$ s y $\blacksquare$ . De hecho, esa casilla no debería rellenarse, pero por alguna razón, no puedo producir un \Box.

En fin, me preguntaba si alguien podría explicarme qué significan los enlaces de vuelta a la tau, qué significan las casillas. Siempre que leo ese libro, sustituyo el $\tau$ s con la de Hilbert $\varepsilon$ s. Es decir, se tomaron muchas molestias para usar esta notación, así que debe significar algo no trivial, ¿no?

Puede véase en la primera página del enlace de google books que he puesto. No estoy seguro de si se supone que es intencionalmente vaga, pero nunca introducen ninguna regla metamatemática para hacer frente a los vínculos a excepción de los criterios de sustitución, que más o menos no puede interactuar con $\tau$ condiciones.

Además, por supuesto, como es un libro escrito para ser completamente un coñazo de leer, utilizan un cálculo hilbert, y lo que es peor, sin igualdad primitiva para determinar si dos conjuntos son equivalentes o no.

Answer 1

Permítanme abordar la parte de la pregunta sobre "qué significan los vínculos con la tau, qué significan las casillas". La notación habitual para utilizar el símbolo épsilon de Hilbert es que se escribe $(\varepsilon x)\phi(x)$ para significar "algunos (no especificados) $x$ satisfaciendo $\phi$ (si existe, y un objeto arbitrario en caso contrario)". Si, como Bourbaki, uno quiere evitar los cuantificadores en la notación oficial y utilizar $\varepsilon$ en su lugar (concretamente, expresando $(\exists x)\phi(x)$ como $\phi((\varepsilon x)\phi(x))$ ), entonces cualquier fórmula no trivial contendrá montones de $\varepsilon$ aplicadas a muchas variables, todas anidadas en un lío complicado. Para reducir ligeramente la complicación, supongamos que las variables vinculadas se han renombrado de modo que cada aparición de $\varepsilon$ utiliza una variable diferente. La notación de Bourbaki (aún más complicada, en mi opinión) es lo que se obtendría si se hace lo siguiente para cada ocurrencia de $\varepsilon$ en la fórmula. (1) Sustituya este $\varepsilon$ avec $\tau$ . (2) Borre la variable que viene justo después del $\varepsilon$ . (3) Sustituye todas las apariciones posteriores de esa variable por una casilla. (4) Vincule cada una de esas casillas a la variable $\tau$ que escribiste en (1). Así que $(\varepsilon x)\phi(x)$ se convierte en $\tau\phi(\square)$ con un enlace desde el $\tau$ a las cajas (tantas cajas como había $x$ 's en $\phi(x)$ ).

Cabe preguntarse por qué Bourbaki hace todo esto. Hasta donde yo sé, el objetivo de las cajas y los enlaces es que no hay variables ligadas en la notación oficial; todas han sido reemplazadas por cajas. Así que Bourbaki no necesita definir cosas como ocurrencias libres y ligadas de una variable. Donde yo (y casi todo el mundo) diría que una variable aparece libre en una fórmula, Bourbaki puede decir simplemente que la variable aparece en la fórmula.

Sospecho que Bourbaki eligió utilizar la expresión de Hilbert $\varepsilon$ como una forma inteligente de obtener el axioma de elección y los cuantificadores lógicos a la vez. Y no tengo ni idea de por qué cambiaron $\varepsilon$ à $\tau$ (aunque, mientras escribía esta respuesta, me he dado cuenta de que prefiero escribir tau a varepsilon).

Answer 2

Debe leer el encantador ensayo en el que se ridiculiza esta notación, a la vez que se hace un análisis lógico exhaustivo de la misma, de Adrian Mathias .

• Adrian Mathias, Un plazo de duración 4.523.659.424.929 Synthese 133 (2002) 75-86

Lo describe así:

Cálculo del número de símbolos necesarios para dar la definición de Bourbaki del número 1; a lo que hay que añadir 1.179.618.517.981 enlaces desambiguadores. Se discuten las implicaciones para las afirmaciones filosóficas de Bourbaki y la salud mental de sus lectores.

Answer 3

Las polémicas de Matthias son divertidas en algunos momentos, pero también engañosas en varios aspectos:

1. ZFC también tiene una enorme longitud y profundidad de deducciones para material trivial. Según la página de metamatemáticas de Norman Megill, "la demostración completa de 2 + 2 = 4 implica 2.452 subteoremas, incluidos los 150 [profundidad del árbol de demostración] anteriores. ... Éstos tienen un total de 25.933 pasos -éste es el número de pasos que tendrías que examinar si quisieras verificar la demostración a mano con todo detalle hasta llegar a los axiomas." El sistema de Megill se basa en un formalismo para sustituciones, así que puede haber un enorme ahorro aquí comparado con la forma en que Matthias realiza los recuentos (es decir, el tamaño expandido completo en símbolos) para el sistema de Bourbaki. Si recuerdo correctamente otra información de Megill sobre la longitud de prueba que estimó para varios resultados en ZFC, el número de símbolos requeridos puede ser órdenes de magnitud mayor y esto es lo que debería compararse con los números de Matthias.

2. El tamaño de las pruebas depende enormemente de la implementación. La longitud de las pruebas Bourbaki podría ser una cuestión de decisiones de diseño no esenciales. Matthias afirma al final del artículo que hay un problema al usar la anotación épsilon de Hilbert para sistemas incompletos o indecidibles, pero no da ninguna indicación de que este o cualquier otro problema sea insuperable en el enfoque Bourbaki.

3. De hecho, el propio Matthias parece haber superado el problema en sus otros trabajos, expresando la teoría de conjuntos de Bourbaki como un subsistema de ZFC. Así que, o bien ha demostrado que algunos subsistemas razonablemente potentes de ZFC tienen pruebas y definiciones que se acortan radicalmente al añadir la Sustitución, o bien que el enorme "término" que atribuye a la Teoría de los conjuntos se reduce a un tamaño más similar a ZFC cuando se implementa en un marco diferente.

EDITAR. Buscando los cálculos de Norman Megill sobre la longitud de las pruebas en ZFC he encontrado lo siguiente:

"incluso las pruebas triviales requieren un asombroso número de pasos directamente de los axiomas . Existencia del conjunto vacío puede demostrarse con 11.225.997 pasos y la recursividad transfinita puede demostrarse con 11.777.866.897.976 pasos".

y

"Las pruebas existen sólo en principio, por supuesto, pero su longitudes se calcularon a partir de las que resultarían de pruebas más tradicionales si estuvieran completamente expandidas. ..... En la versión actual de mi prueba que se ha reorganizado un poco, los números son:

conjunto vacío = 6.175.677 pasos

transf. rec. = 24.326.750.185.446 pasos"

Es sólo el número de pasos. El número de símbolos sería mucho, mucho mayor.

Answer 4

Me gustaría mencionar sobre "lo que significan los vínculos de vuelta a la tau, lo que significan las cajas", que esta notación ha sido revisada por Nicolaas Govert de Bruijn en el marco del lambda-cálculo y se utiliza en gran medida en la informática teórica como una herramienta muy conveniente y se conoce ahora como "de Bruijn" índices. Se puede encontrar bibliografía al respecto.

Answer 5

La notación mediante enlaces fue inventada por Charles Saunders Peirce con sus diagramas existenciales en 1883. Fue reinventada por Willard van Orman Quine en su libro Mathematical Logic en 1940. (Quine no utilizó la notación.) Bourbaki la reinventó en 1970.

Sostengo que la notación con enlaces es más fundamental que los índices de Bruijn, porque eso sigue añadiendo ciertos detalles de aplicación. La notación con enlaces puede parecer incómoda pero, por ejemplo, en la teoría de las interpretaciones hay muchos problemas artificiales para seguir la pista de los nombres de las variables. Los enlaces permiten evitarlos.

Creo que el uso de enlaces dicta un enfoque co-inductivo y descendente, ` visión "descomposicional" de la sintaxis.