La consideración de Hintikka del axioma de elección y del desafío constructivista

In the present paper we confront Martin- Löf’s analysis of the axiom of choice with J. Hintikka’s standing on this axiom. Hintikka claims that his game theoretical semantics (GTS) for Independence Friendly Logic (IF logic) justifies Zermelo’s axiom of choice in a first-order way perfectly acceptable for the constructivists. In fact, Martin- Löf’s results lead to the following considerations:Hintikka preferred version of the axiom of choice is indeed acceptable for the constructivists and its meaning does not involve higher order logic.However, the version acceptable for constructivists is based on an intensional take on functions. Extensionality is the heart of the classical understanding of Zermelo’s axiom and this is the real reason behind the constructivist rejection of it.More generally, dependence and independence features that motivate IF-Logic, can be formulated within the frame of constructive type theory (CTT) without paying the price of a system that is neither axiomatizable nor has an underlying theory of inference – logic is about inference after all.We conclude pointing out that recent developments in dialogical logic show that the CTT approach to meaning in general and to the axiom of choice in particular is very natural to game theoretical approaches where (standard) metalogical features are explicitly displayed at the object language-level. Thus, in some way, this vindicates, albeit in quite of a different manner, Hintikka’s plea for the fruitfulness of game-theoretical semantics in the context of the foundations of mathematics.En el presente trabajo confrontamos el análisis del axioma de elección de Martin - Löf con la posición de J. Hintikka respecto de este axioma. Hintikka afirma que su Semántica Teorética de Juegos (STJ) para una Lógica de la Independencia Amigable (Lógica IA), justifica el axioma de elección de Zermelo en un sentido de primer orden perfectamente aceptable para los constructivistas. De hecho, los resultados de Martin - Löf conducen a las siguientes consideraciones:La versión preferida de Hintikka del axioma de elección, es ciertamente aceptable para los constructivistas y su significado no implica una lógica de orden superior.Sin embargo, la versión aceptable para los constructivistas se basa en una consideración intensional sobre las funciones. La extensionalidad es el corazón de la comprensión clásica del axioma de Zermelo y esta es la razón real tras el rechazo constructivista de éste.En general, las características de dependencia e independencia que motivan la Lógica IA, pueden formularse en el marco de la Teoría de Tipos Constructiva ( TTC ) sin tener que pagar el precio de un sistema que no es ni axiomatizable ni tiene una teoría subyacente de la inferencia – la lógica trata sobre la inferencia después de todo.Concluimos señalando que los recientes desarrollos en lógica dialógica muestran que el enfoque TTC hacia el significado, en general, y hacia el axioma de elección, en particular, es connatural al enfoque de la teorética de juegos, donde las características metalógicas (standard) se despliegan explícitamente a nivel del lenguaje - objeto. Por tanto, de algún modo, esto justifica, aunque de una manera bastante diferente, la exhortación de Hintikka por la fecundidad de la Semántica Teorética de Juegos en el contexto de los fundamentos de las matemáticas