Teoría de tipos y metáfora

En mi experiencia, los libros de texto y el material introductorio sobre teoría de tipos (o sistemas lógicos constructivos) están notablemente desprovistos de metáforas. Nunca encontré ningún texto introductorio en esos campos que procediera de manera similar a otras áreas de la lógica, basadas en la teoría de conjuntos, donde puedes optar por introducir el tema "intuitivamente" (metafóricamente), y avanzar gradualmente hacia enfoques más abstractos y secos. .

Mi pregunta es si esta es una característica lingüística esencial del tratamiento de la teoría de tipos en los textos (en otras palabras, la impermeabilidad a la metáfora es una cuestión epistemológica), o si es simplemente una estrategia teórica preferible y recomendable.

Russell da algunas analogías "concretas" interesantes en su tratamiento, ¿no es así? (El barbero del regimiento, por ejemplo, afeita a todos los que no se afeitan a sí mismos, entonces, ¿quién afeita al barbero?)
Esa historia está relacionada con la paradoja que encontró mientras trabajaba en su "Principia Mathematica". Impactó el tratado de Frege sobre los fundamentos de la aritmética, mostrando que sus axiomas producían inconsistencias. Russell propuso la teoría de tipos para evitar tales trampas, pero mi pregunta se centra en la literatura más reciente.

Respuestas (1)

Dudo que esto sea algo esencial para escribir la teoría per se; pero más debido al modo omnipresente de escritura matemática y científica; el arte de la exposición, creo que se ha ido perdiendo poco a poco.

Lagrange, por ejemplo, se enorgullecía de que sus obras matemáticas no tuvieran diagramas. Vladimir Arnold se había quejado de un enfoque excesivamente bourbakista de las matemáticas que, en lugar de aclarar las ideas principales y señalar el significado, lo escondía todo bajo una gruesa incrustación de formalismo; la mayoría de los cuales ocultaban que se decía poco de cualquier significado adicional .

Ciertas teorías de tipos están relacionadas con ciertas categorías, por ejemplo, el cálculo lambda simplemente tipificado con categorías cartesianas cerradas y algunas de estas pueden presentarse de manera más natural como diagramas de cuerdas; y estos pueden entenderse topológicamente de forma natural.

Yo diría que esto es una especie de analogía esquemática.

En Teoría de Conjuntos, los elementos y conjuntos son básicos; y se deriva la noción de función; Topos Theory toma conjuntos y funciones (ie objetos y morfismos) como básicos; y elementos como derivados: Lawvere dijo que quería hacer una teoría de conjuntos sin elementos.

Esto no es exactamente una metáfora, ni siquiera una analogía, pero funciona bastante bien en la forma en que pone la Teoría de Conjuntos 'sobre su cabeza'; más bien como cómo el marxismo como filosofía económica puso a Hegel "de cabeza". Uno podría llamarlo un eslogan; tal vez incluso una 'declaración de misión'.

Sí, la conexión entre la teoría de tipos y la teoría de categorías nos permite expresarnos usando diagramas de objetos y flechas, pero no son metáforas conceptuales, al menos no en este contexto.
Sí creo que el pensamiento matemático se relaciona en general con las metáforas conceptuales (sigo a George Lakoff y Rafael Núñez en esa suposición: en.wikipedia.org/wiki/Where_Mathematics_Comes_From ), pero me gustaría saber si la lógica constructiva podría ser una excepción. Aunque así sea, creo firmemente que el tema siempre ha sido presentado en un estilo excesivamente dogmático, incluso por autores que supuestamente escriben para principiantes.
Seguro que los diagramas no son metáforas; pero a veces son una mejor disposición de la información que permite una mejor comprensión.
Los diagramas de cuerdas que mencioné anteriormente no son los mismos que los diagramas teóricos de categorías habituales; echa un vistazo a esto ; de hecho, recuerdo haber visto una descripción muy breve de la lógica lineal mediante la metáfora de un menú en un restaurante francés; eso es probablemente más apropiado para su pregunta.
Tal vez porque la lógica constructiva va en contra de la lógica clásica convencional; que el estilo de escritura se vuelve dogmático; además, hay menos gente trabajando con él, por lo que las ideas generales, que no se entienden ampliamente ni se confía en ellas, tienen que explicarse una y otra vez; por ejemplo, todo matemático 'conoce' la teoría de conjuntos sin conocer ZFC; puedes llegar muy lejos simplemente usando la metáfora de los diagramas de Venn.
Teoría de tipos y metáfora
RespuestasAquíPolítica de privacidad1y, 0v