EWD463 Algunas Preguntas: (Some Questions (Dijkstra - Gödel Theorem))

Original: "Some questions": http://www.cs.utexas.edu/users/EWD/transcriptions/EWD04xx/EWD463.html
Original: (pdf of typewrited text): http://www.cs.utexas.edu/users/EWD/ewd04xx/EWD463.PDF

Año: 1974

Algunas preguntas:

Hay algunas preguntas que, por el solo hecho de ser presentadas, revelan una visión profunda. Otras preguntas, por el mismo hecho de ser presentadas, solo muestran ignorancia. Con toda probabilidad, mis preguntas caerán en la última categoría.

Comienza con el Teorema de Gödel, y aquí empiezo ya con una muestra de ignorancia. Alguien, (¿quién fue?) - se llevó 'prestada' mi copia de la "Introducción a la metamatemática" de Kleene [1]. y, como resultado, sólo puedo confiar en mi memoria. Eso no sería tan malo si hubiera estudiado el libro a fondo, pero no lo había hecho. Y no solo no lo estudié, sino que solo lo leí en parte, a causa del hecho que su lectura no me dió la sensación de que su contenido realmente me interesara. Pero si recuerdo correctamente, dice: (¡Perdón por mi vaga terminología!) que ningún conjunto consistente de axiomas puede servir como base para la demostración de su propia integridad. La vaga formulación anterior podría hacer que un lógico profesional se estremeciera. Lo siento: mi memoria es así de mala. Lo que sí recuerdo de forma más clara es que el resultado tal vez me sorprendió, pero ciertamente no me molestó. ¿Es porque el Teorema de Gödel negó la posibilidad de una forma de comprensión perfecta que, por cierto, nunca había sido mi ideal? 


Menciono lo anterior porque en los últimos años he descubierto que muchas personas tienen sospechas respecto la legitimidad o la adecuación de los métodos axiomáticos [2]. Y recientemente llegué a la conclusión de que no podía entender por qué.

En una carta reciente, Tony Hoare me preguntó si conocía el veredicto de Bertrand Russell: "Las ventajas del método de postulación [3] son excelentes; son las mismas que las ventajas del robo sobre el trabajo honesto". (De alguna manera lo sabía; ¡tal vez fue el mismo Tony quien me lanzó la cita en una ocasión anterior!) Una deshonestidad (¿intelectual?) característica del método de postulación es más que levemente sugerida. Admito una diferencia en el criterio de "honestidad" entre Russell y yo, - y con el debido respeto: ¡tal diferencia no necesariamente me molestaría! Sin embargo, el veredicto me intriga lo suficiente como para plantear la pregunta "¿Por qué?".

El veredicto de Russell no me interesaría, si no fuera por el hecho de que ahí escuché un eco con respecto a las propuestas para definir la semántica de los lenguajes de programación. Lo que ahora se conoce como "el método axiomático" - ¿el "método postulacional" hubiera dado lugar a menos malentendidos? - define la semántica de un lenguaje de programación en estrecho paralelismo con su sintaxis: Para cada nueva forma de definir la semántica de un objeto compuesto en cuanto a la semántica de sus componentes, se elige una nueva construcción sintáctica. Ese enfoque me atrajo mucho: para el tipo de programas que me gustaría poder diseñar mejor de manera controlada, tales postulados parecían ser más fácilmente forjados en una herramienta para la composición práctica del programa. Lo encontré, por ejemplo, mucho más atractivo que mecanizar -o al menos desarrollar un cálculo para- la traducción de programas recursivos a programas repetitivos.

La defensa habitual para ese enfoque de dos pasos era que era una forma de conciliar la eficacia potencialmente mayor de las soluciones repetitivas con el hecho de que "las soluciones recursivas son más naturales". Pero lo son? ¿Es esta una ley de la naturaleza humana? ¿O las personas se sienten así, confunden "conveniente" con "convencional" y no es más que el síntoma de una incapacidad matemática para hacer frente a la repetición, --y a las "variables", tal como ocurre en los lenguajes de programación-- por derecho propio? ?

Encontré una confirmación en la tentación (¡me rendí una vez, en un momento de debilidad!) Para definir la semántica de 

" Mientras B 'hacer:' S 'recah' "  
[NT: Original: "while B do S od"]

como el de la llamada:

"Mientras(B,S)"
[NT: Original:  "while(B, S)"]

O el procedimiento recursivo: 

"procedimiento Mientras(B, S): si B entonces S; Mientras (B, S) is otneimidecorp"
[NT: "proc while(B, S): if B then S; while(B, S) fi corp" ] 

¿Pero no es eso romper un huevo con un mazo? (Sé que para el propósito de una analogía, puede ser esclarecedor considerar todas las constantes escalares como funciones, definidas en el mismo dominio de un punto, cuyo argumento, por lo tanto, puede permanecer anónimo, pero siempre debemos considerar las constantes como tales funciones. Eso, me temo, sería un martillo similar. Y, si puedo plantear la pregunta, ¿es honesto el uso de martillos para romper los huevos, por el hecho de que se hubiera sugerido la necesidad del martillo?

Se han desarrollado otras propuestas para definir la semántica del lenguaje de programación, y se ha afirmado la superioridad sobre el método axiomático debido a un argumento que no entiendo. El argumento es que en tales alternativas, los axiomas del método axiomático no necesitan ser "postulados" sino que pueden demostrarse como teoremas. Fino e interesante. ¿Pero cuál es la ganancia? ¿Es injusto invertir ese argumento y señalar la superioridad del método axiomático debido al hecho de que no es necesario probarlos como teoremas, ya que con postularlos es ya suficiente? Si esos pocos axiomas en un esquema y teoremas en el otro son la única interfaz a través de la cual la teoría tiene su impacto en la actividad de programación, y supongamos que este sea el argumento, ¿es así? entonces, ¿no es más eficiente simplemente postular esa interfaz, ignorando el elaborado tejido que podría ser tejido debajo de ellas? Aquí estamos claramente de vuelta al veredicto de Russell. ¿Es el método de postulación injusto, o quizás mortalmente peligroso? 

Un posible ataque al método de postulación es "¿Pero cómo sabes que tus postulados son verdaderos, si no los has probado?", Pero esa pregunta solo tiene sentido si consideramos los postulados como propiedades de algo ya definido de otra manera, y la cuestión de la "verdad" se vuelve irrelevante cuando se consideran los postulados como "especificaciones de interfaz". Una duda posiblemente más válida puede surgir con la pregunta "¿Cómo sabes que tus axiomas son consistentes?". 

Mi inclinación, ¿pero tal vez soy terriblemente ingenuo? Es decir: "Bueno, estoy bastante seguro de que son consistentes. Y si no lo son: ¡ese es mi riesgo! ¡Lo peor que podría haber hecho es hablar de un universo vacío y, aunque infructuoso, tampoco pueden haber hecho mucho daño ". Mi impresión es que, cuando los lógicos hablan de "interpretar" o "proporcionar un modelo", tan pronto como empiezan a hacerlo, siempre me siento confundido: Están tratando de demostrar (?) la consistencia de un conjunto de axiomas  mostrando la existencia (?) del universo al que se aplican. ¿Hacen esto  en términos de otro sistema formal, sobre la consistencia del cual tienen mayor confianza? ¿Es esta una descripción justa de lo que están haciendo los lógicos? Si es así, me parece una forma completamente respetable de tratar de elevar un nivel de confianza, cuya relevancia, sin embargo, parece estar estrechamente relacionada con el hecho de que tengamos razones para no confiar demasiado en el primer sistema, y ​​cuya efectividad parece estar estrechamente relacionada relacionado con nuestra simpatía con el segundo sistema. 

Si el objetivo de "hacer modelos" es dar una "prueba de existencia", creo que puedo entender el propósito del ejercicio. Dudo, para decirlo con suavidad, cuando la semántica del primer sistema se identifica con -o se define como- las propiedades del modelo, porque además --¡afortunadamente! - muestra las propiedades previstas, el modelo tendrá, en general, muchas otras propiedades también, algunas de ellas ya conocidas, algunas de ellas, quizás, aún no descubiertas. ¡Y esa parece una forma menos atractiva de definir una interfaz! 

Y ahora estamos de vuelta en nuestro viejo dilema. O tomamos por definición todas las propiedades del modelo como relevantes, o especificamos de una forma u otra cuáles de sus propiedades son las relevantes. En el primer caso, no hemos podido introducir en nombre de "divide y vencerás" una interfaz que nos permita dividir y gobernar, y el estudio de cómo podríamos construir sobre la interfaz (solo implícitamente definida) parece deteriorarse en un estudio del modelo mismo; en el segundo caso estamos nuevamente cerca del método axiomático ...

En resumen: estoy convencido de "las grandes ventajas" mencionadas por Russell, pero ¿por qué el "robo"? ¿A quién se está robando de qué? ¿O es "deshonesto" crear un sistema en el que las preguntas sean nulas y que de otro modo podrían resolverse con un "trabajo honesto"? 

Incluso si ignoro el juicio moral implícito en el veredicto de Russell, me resulta difícil de tragar. Juzgo una teoría no solo por su belleza intrínseca, sino también por qué problemas evoca, qué esfuerzos atrae, cuánto se necesita para ello, qué problemas resuelve y qué tan eficientemente lo hace, etc. Y hasta donde puedo Ver, el método de postulación, cuando se aplica a la semántica del lenguaje de programación, tiene puntuaciones bastante altas en la mayoría de estos diversos aspectos. ¿Estoy ciego a algunas preguntas filosóficas, de la misma manera que otras personas son sordas o daltónicas, o viene el veredicto de Russell y sus ecos de un clima intelectual en el que la ciencia pura estaba bastante divorciada de la ciencia aplicada , y mucho menos de la ingeniería? 

O, para decirlo de otra manera: si la teoría tradicional de los autómatas tiende a hacernos insensibles al papel que las interfaces podrían y deberían desempeñar para hacer frente a diseños complejos, ¿deberían entonces (continuar) ocupando una posición central en los planes de estudios de ciencias de la computación? 

17th November 1974 Burroughs Plataanstraat 5 NUENEN - 4565 The Netherlands

prof.dr.Edsger W.Dijkstra Burroughs Research Fellow

 

[1] NT: Kleene: Introduction to Metamathematics: Book note:  
https://www.logicmatters.net/tyl/booknotes/kleene-metamath/   
"Introducción a la metamatemática de Stephen Cole Kleene (Holanda del Norte, 1962; reimpreso Ishi Press 2009: pp. 550) durante un tiempo mantuvo el campo como un tratado de supervisión de la lógica de primer orden (sin pasar mucho por el teorema de integridad) y como un  tratado mas en profundidad de la teoría de las funciones computables y los teoremas de incompletitud de Gödel"

[2] NT: Método Axiomático: (Axiomatic Method): 
https://en.wikipedia.org/wiki/Axiomatic_system#Axiomatic_method  
"Establecer definiciones y proposiciones de tal manera que cada nuevo término pueda ser eliminado formalmente por los términos introducidos previamente requiere nociones primitivas (axiomas) para evitar un retroceso infinito. Esta forma de hacer matemáticas se llama método axiomático".
"Los axiomas de Zermelo-Fraenkel, el resultado del método axiomático aplicado a la teoría de conjuntos, permitió la formulación "adecuada" de los problemas de la teoría de conjuntos y ayudó a evitar las paradojas de la teoría de conjuntos ingenua. Uno de esos problemas fue la hipótesis del continuo. La teoría de conjuntos de Zermelo-Fraenkel con el axioma de elección históricamente controvertido incluido se abrevia comúnmente como ZFC, donde C significa elección. Muchos autores usan ZF para referirse a los axiomas de la teoría de conjuntos de Zermelo-Fraenkel con el axioma de elección excluido. Hoy ZFC es la forma estándar de la teoría de conjuntos axiomáticos y, como tal, es la base más común de las matemáticas".

[3] NT: Postulational Method:  Mathematical Logic Object Theory:  
https://en.wikipedia.org/wiki/Object_theory 
"The genetic versus axiomatic method" 

"El siguiente es un ejemplo del método genético o constructivo de hacer objetos en un sistema, el otro es el método axiomático o postulacional. Kleene afirma que un método genético tiene la intención de" generar "todos los objetos del sistema y por lo tanto" determinar la estructura abstracta del sistema completamente "y de manera única (y, por lo tanto, define el sistema categóricamente). Si se utilizan axiomas en lugar de un método genético, se dice que tales conjuntos de axiomas son categóricos"