En una filosofía sitio, ella dijo que usted podría tener una categoría con teoremas como los objetos y de las pruebas como flechas. Esto suena genial, pero no pude encontrar nada en la web que tiene tanto de "categoría" y "pruebas" en el título. Donde es la literatura, como un PDF de esta categoría.
Respuestas
¿Demasiados anuncios?Este documento, llamado la Física, la Topología, la Lógica y la Computación: Una Piedra de Rosetta es lo que hace en la sección 3.2. Si tienes tiempo e interés, me permito sugerir la lectura de todo el documento (ya que todo está bastante bien).
La manera correcta de construir una categoría es una cuestión filosófica. Existen diferentes enfoques en la literatura matemática. Una cosa está clara, sin embargo: los objetos deben ser propuestas, no sólo de teoremas.
El problema es definir la igualdad de las pruebas de una manera sensible. Por ejemplo, supongamos $\Pi$ ser de Pitágoras teorema. Cada uno de los más de 100 pruebas de $\Pi$ encuentra aquí ser diferentes de morfismos $\top\to\Pi$? En ese caso, es difícil ver cómo la composición de las pruebas pueden ser definidos de tal manera que no hay una única identidad "de prueba" para cada proposición.
Un enfoque es considerar algunas pruebas esencialmente igual si algunos superficial transformaciones vez una prueba en el otro. Esto, sin embargo, traslada el problema de la definición de la igualdad de pruebas para el problema de la definición de la igualdad de las transformaciones de las pruebas. Así que las pruebas y las proposiciones son en realidad parte de algunos $\infty$-categoría. Si te gusta esta línea de razonamiento, echa un vistazo a homotopy tipo de la teoría y su aplicación en diversos prueba assistents.
Otro método es simplemente considerar que cada prueba igual a cualquier otra prueba de la misma proposición, de modo que la categoría de las proposiciones y de las pruebas es un poset. Para el clásico de primer orden de la lógica de este poset es conocido como el Lindenbaum-Taski álgebra.
El $\lambda$-cálculo es un camino intermedio entre la infinidad de categorías y el posets. Las pruebas pueden ser codificados como $\lambda$-términos. Un montón de irrelevantes las diferencias entre las pruebas se han perdido en esta codificación. Existen las relaciones de equivalencia en $\lambda$-plazo basado en transformaciones como $\beta$-reducción. La contrapartida de $\lambda$-cálculos son Cartesiano categorías cerradas.
Véase, por ejemplo, Lambek y Scott: Introducción a las de orden superior categórica lógica, ch 0.1 (lamentablemente no está en la red, pero seguro que en ur de la biblioteca de la universidad). Primero se define un gráfico, a continuación, un sistema deductivo como un gráfico con
- Para cada objeto $A$ una identidad flecha $1_A:A\rightarrow A$
- Para cada par de flechas $f:A\rightarrow B$ $g:B\rightarrow C$ el composición $gf:A\rightarrow C$
La idea de un lógico podría ser que de los objetos como de las fórmulas y las flechas como las deducciones, la composición en este contexto convertirse en una regla de inferencia $$\frac{f:A\rightarrow B\space\space\space g:B\rightarrow C}{gf:A\rightarrow C}$$
Sin embargo esto es sólo una interpretación y dejando esto a un lado uno puede tomar que la definición abstracta de un sistema deductivo para salir con la costumbre de la categoría:
Una categoría es un sistema deductivo con los dolores de ecuaciones para la identidad y la asociatividad - es decir, para $f:A\rightarrow B$, $g:B\rightarrow C$ y $h:C\rightarrow D$ $$f1_a=f=1_Bf,\space\space (hg)f=h(gf)$$