INTERACCION E IGUALDAD. LA INTERPRETACION DIALOGICA DE LA TEORIA CONSTRUCTIVA DE TIPOS.
| Autor | Rahman, Shahid |
| Cargo | Ensayo |
-
Introduccion
1.1. Objetivos
El objetivo principal de este articulo es proveer elementos de analisis que vinculen la nocion de interaccion argumentativa, concebida dentro de un cuadro dialogico para la logica constructiva, con la nocion de igualdad definicional de la teoria constructiva de tipos (en adelante, TCT) de Per Martin-Lof. Dicho con mayor precision, intentaremos mostrar que tal igualdad, que en la TCT provee el criterio de identidad asociado a un tipo, puede comprenderse, desde el punto de vista ludico, como resultado de una forma especifica de interaccion dialogica regida por la regla conocida como regla formal, mas recientemente llamada regla socratica, la cual prescribe el uso de jugadas de espejo (copy-cat moves). Ilustraremos nuestra tesis con el desarrollo dialogico de las partes esenciales de la demostracion del axioma de eleccion de Per Martin-Lof, quien baso su prueba en la igualdad definicional entre la funcion que prueba el antecedente y la funcion que ocurre en el consecuente.
1.2. Antecedentes y marco conceptual
A partir de una sugerencia de Goran Sundholm, se realizo una lectura dialogica de las reglas de introduccion y de eliminacion de la deduccion natural propuesta por Rahman, Clerbout y Keiff (2009). La idea subyacente es, por una parte, concebir las reglas de introduccion como prescripciones que establecen las condiciones que debe satisfacer el proponente (P) para la construccion de una estrategia ganadora y, por la otra, concebir las reglas de eliminacion como prescripciones que determinan como construir una estrategia ganadora para P a partir de las afirmaciones que el oponente (O) esta forzado a conceder. Esa interaccion normativa y armonica de derechos y obligaciones motivo a Clerbout y Rahman (2015) a explorar la contribucion de la interpretacion dialogica a los fundamentos pragmaticos de la significacion en un cuadro constructivista extendido como el de la TCT. (1)
Un nuevo impulso a estas investigaciones provino de una reciente serie de conferencias de Per Martin-Lof en Paris (2015), quien utilizo la perspectiva dialogica sobre la normatividad de la logica para salir de una circularidad que parecia amenazar la explicacion de las nociones de inferencia y demostracion.
En efecto, desde el punto de vista constructivista, una demostracion se puede explicar como una cadena de inferencias (inmediatas) a partir de ninguna premisa. Que una inferencia como
[[J.sub.1]...[J.sub.n]/J]
sea valida significa que la conclusion, el juicio J, puede hacerse evidente bajo la suposicion de que "conozcamos" [[J.sub.1]...[J.sub.n]]. Esta nocion de suposicion, que Sundholm llama "suposicion epistemica", permite asi la explicacion de la nocion de inferencia valida. No podemos, sin embargo, entender "conocido" en el sentido de demostrado, ya que entonces estamos explicando la nocion de inferencia en terminos de demostracion, mientras que la demostracion se ha explicado en terminos de inferencia. Martin-Lof sugiere que aqui debemos entender "conocido" como "afirmado en el sentido dialogico". De este modo, los supuestos epistemicos expresan juicios que otro ha llevado a cabo: el oponente. Este se hace asi responsable de las obligaciones contraidas por su propia afirmacion. Que la inferencia sea valida significa, entonces, que dado que otro ha asumido la responsabilidad de las premisas, puedo ahora asumir la responsabilidad de la conclusion basandome en la autoridad otorgada al antagonista:
cuando se esta dando cuenta de la nocion de inferencia inmediata, la nocion de demostracion no esta aun a nuestra disposicion. Por ello, la expresion [cuando queremos explicar que es una inferencia inmediata] "supongamos que [[J.sub.1]... [J.sub.n]]" nos hace blanco de la acusacion de que nuestra explicacion es circular [...]. Es ahora de mi parecer que la solucion a este problema de circularidad resulta naturalmente de un analisis dialogico [...]. La solucion aqui no es suponer que las premisas se conocen en un sentido cualitativo [del termino conocer], esto es, que se han demostrado, sino que simplemente debemos suponer que se han afirmado, lo que equivale a decir que otros han tomado la responsabilidad por ellas, y ahora la pregunta que se plantea es si estoy dispuesto a hacerme responsable de la conclusion. [...] Esta parece ser la definicion apropiada de la nocion de supuesto epistemico en el sentido de Sundholm. (2) Esta nueva perspectiva llevo a los autores del presente estudio a iniciar una indagacion mas profunda de los lazos entre el concepto de explicacion de significado de la TCT y la concepcion pragmatica del significado del marco dialogico. (3) La idea es enfocar el estudio de la conexion entre estas dos teorias del significado en el proceso de constitucion de un tipo. En efecto, dado que una de las etapas fundamentales en el proceso de constitucion de un tipo es el criterio de identidad definicional, parece natural preguntarse como se relaciona un criterio tal de identidad con la interpretacion dialogica. La propuesta principal de nuestro articulo es que si vinculamos la regla socratica con la igualdad definicional y con la nocion de supuesto epistemico, obtendremos una nueva via, simple y directa, para utilizar el enfoque de la TCT dentro del marco dialogico. En general, la idea rectora es que la regla socratica es la que subyace tras la interpretacion normativa de la nocion de supuesto epistemico sugerida por Martin-Lof. Nuestra propuesta puede resumirse de la siguiente manera:
-
O puede atacar un objeto ludico b que P ha propuesto como defensa de una proposicion elemental A.
-
La defensa de un ataque a b consiste en afirmar una igualdad definicional reflexiva o no reflexiva. En ambos casos esta igualdad expresa que el objeto ludico en cuestion b es igual al que O uso para defender A. La igualdad codifica el resultado de una interaccion mediante la cual P copia jugadas del adversario a fin de proveer las unidades semanticas basicas de la tesis en cuestion.
El caso no reflexivo expresa el caso en el que O elige b como resolucion de una instruccion ludica (un operador que no tiene la forma argumentativa canonica requerida por A), que forma parte de una de las concesiones asociadas a la afirmacion de la tesis.
De estas consideraciones se sigue la organizacion del presente trabajo: empezaremos con una discusion del tratamiento de la igualdad en la TCT y luego presentamos su desarrollo en el marco dialogico.
-
Igualdad definicional en la teoria constructiva de tipos
2.1. Algunos postulados relevantes de la teoria constructiva de tipos En la TCT, las constantes logicas se interpretan a traves de la correspondencia Curry-Howard entre proposiciones y conjuntos. Una proposicion se interpreta como un conjunto cuyos elementos representan las pruebas de la proposicion. Tambien es posible visualizar un conjunto como la descripcion de un problema y sus elementos como las soluciones al problema de una manera similar a la explicacion de Kolmogorov del calculo proposicional intuicionista. Ademas, en TCT los conjuntos se entienden tambien como tipos, de modo tal que las proposiciones pueden verse como datos o tipos de prueba. (4)
El objetivo filosofico fundamental de la TCT es desarrollar un enfoque de interpretacion total ( fully interpreted approach), (5) donde se presta especial atencion a:
evitar mantener separados el contenido y la forma. En su lugar mostraremos ciertas formas de juicio e inferencia que se utilizan en las pruebas matematicas y al mismo tiempo daremos una explicacion semantica de tales formas de juicio. De esta manera, hacemos explicito lo que se suele dar por sentado implicitamente. (6) En relacion con la tarea de explicitacion, se trata de poner en el nivel del lenguaje objeto caracteristicas que determinan el significado y que se formulan usualmente en el nivel meta. De acuerdo con el punto de vista logico de la TCT, las premisas y la conclusion de una inferencia logica no son proposiciones, sino juicios:
Una regla de inferencia se justifica explicando la conclusion bajo el supuesto de que las premisas se conocen. Por lo tanto, antes de que una regla de inferencia pueda ser justificada, debe explicarse que es lo que hay que saber para tener el derecho de hacer un juicio sobre cualquiera de las diversas formas que las premisas y la conclusion pueden tener. (7) Otros dos principios basicos de la TCT son los siguientes:
- Ninguna entidad sin tipo
- Ningun tipo sin identidad
En consecuencia, podemos tomar la afirmacion de que un individuo es un elemento del conjunto A como la afirmacion de que dicho individuo ejemplifica el tipo A. Un conjunto se define en la TCT especificando sus elementos canonicos (que no se definen por medio de otros elementos) y sus elementos no canonicos, de los que se puede mostrar, usando algun metodo prescrito de transformacion, que son iguales (en este conjunto) a uno canonico. Esto ultimo es lo que prescribe el segundo principio basico y que, en otras palabras, consiste en la introduccion de una relacion de equivalencia en un conjunto. Asi, si A es un tipo y tenemos un objeto b que satisface las condiciones correspondientes, entonces b es un objeto de tipo A. Esto se escribe formalmente b : A. (8)
En consecuencia,
b:A A true Y se pueden leer como: b es una prueba de la proposicion A A es verdadera b es un elemento del conjunto A A tiene un elemento b satisface las expectativas de A A es satisfecha b es una solucion al problema A A tiene una solucion Es esencial distinguir entre el elemento de prueba b ( proof-object), el tipo A y el juicio b : A, que establece, en este ejemplo, que b es un elemento de prueba para la proposicion A (si A es del tipo proposicion). En logica estandar, la existencia de una prueba para una proposicion dada se expresa en el nivel del metalenguaje. El hecho de que exista algo (un elemento) b que fundamenta la proposicion de que Primus le debe 100 monedas a Secundus (lo que supondria la afirmacion correspondiente) se da en el...
Para continuar leyendo
Solicita tu pruebaCOPYRIGHT GALE, Cengage Learning. All rights reserved.
