Índice de hipótesis y fundamentos

Índice del tratado

Los axiomas no se interpretan como conclusiones ni como hipótesis satisfechas de los contraejemplos. La matriz argumentada del capítulo 17 distingue rutas y fuerza lógica.

Axioma	Localizador
Asociatividad	1.1.1
Identidades	1.1.2
Existencia de un objeto terminal	1.2.1
Productos binarios	1.3.1
Exponenciales	1.4.1
Existencia de productos fibrados	3.2.1
Clasificador de subobjetos	3.3.1
Paquete de regularidad	4.2.1
Elección regular categórica (hipótesis opcional)	5.2.5

Contratos por capítulo

Capítulo	Marco	Elección de la prueba
1	teoría elemental de categorías; lógica subyacente con igualdad; objetos y flechas dados	none
2	categoría con terminal y productos; exponenciales sólo desde §2.5; metateoría conjuntista explícita para ejemplos y funtor de puntos	none
3	categorías con productos; límites por pullback desde §3.2; clasificador de subobjetos sólo desde §3.3; ejemplos conjuntistas en ZF clásico	none
4	vía mínima: límites finitos + TF-AX-00008; vía acumulada de topos elemental: la regularidad es consecuencia externa conocida, no demostrada aquí; pruebas diagramáticas con precaución de tamaño	none
5	categoría regular según TF-AX-00008; principio de elección regular sólo cuando se invoca TF-AX-00009; reconstrucciones conjuntistas específicamente en ZF clásico	none en teoremas 5.1–5.2 y elección única; TF-AX-00009 asumido sólo en implicaciones explícitas; equivalencias conjuntistas 5.3 en ZF
6	categoría con límites finitos para mapas parciales; categoría regular sólo cuando se comparan relaciones de capítulos 4–5; teoría ZF clásica para extensiones conjuntistas; Top y computabilidad en sus modelos explícitos	none en construcción de Par(C), extensiones no restringidas a codominio habitado en ZF y diagonal computacional; AC se compara sólo para extensiones sometidas a relaciones totales arbitrarias, sin asumirlo
7	límites finitos para spans, restricciones, composición e igualdad; clasificador TF-AX-00007 sólo para predicados característicos; regularidad TF-AX-00008 para imágenes existenciales; estructura de topos elemental bajo límites finitos + exponenciales + clasificador para lógica de Heyting	none
8	categoría con límites finitos para formular clasificación; topos elemental (límites finitos, exponenciales y clasificador de subobjetos) para construir L(B); coproductos extensivos y Booleanidad sólo en identificación con B coproducto 1	none
9	computabilidad de Turing clásica sobre N en secciones 9.1–9.4; teoría de espacios representados y realizadores Tipo 2 en secciones 9.5–9.6; comparación explícita con los clasificadores categóricos, no deducción de efectividad desde axiomas categóricos	none
10	capítulos 1–9; índices de máquinas de Turing sobre N para §§10.1–10.4; nombres de Cauchy rápidos en §10.5; no se infiere efectividad a partir de igualdad categórica	none
11	evaluación y exponenciales de TF-CAT-001–002; subobjetos y objeto potencia de TF-CAT-003; programas parciales de TF-CAT-009; igualdad extensional de TF-CAT-010	none
12	tipos simples como sistema explícito de comparación; productos y exponenciales de TF-CAT-001; extensionalidad de TF-CAT-002 y TF-CAT-010; parcialidad y programas de TF-CAT-006,009; diagonal de TF-CAT-011	none
13	comparación relativa: ZF clásico para conjuntos y Set; cálculo lambda simplemente tipado con productos y unidad; categoría cartesianamente cerrada; teoría de tipos dependientes explícita cuando se indique; modelo efectivo de Turing	none
14	ZF sin elección para la comparación de relaciones y functores con datos explícitos; lógica clásica cuando se indica; máquina de Turing y conjunto de parada sólo en la sección efectiva	no se adopta AC; los representantes de una equivalencia se suministran como datos, sin escogerlos desde existencia meramente individual
15	teoría de categorías localmente pequeñas; categoría índice pequeña para formar conjuntos de transformaciones; Set en ZF sin AC para ejemplos de acciones y familias de productos	none
16	categoría pequeña C; prehaces contravariantes C^op -> Set; conjuntos y cocientes de conjuntos en ZF, sin axioma de elección	none
17	síntesis de contratos locales: categorías, topoi, ZF clásico y representaciones efectivas; no se identifican sus metateorías	ninguno añadido; elección regular sólo como principio opcional comparado
18	síntesis de marcos declarados; ejemplo en naturales de Set y lectura tipada bajo reglas explícitas	ninguna elección arbitraria en el ejemplo; principios de elección sólo como fronteras

Control complementario: matriz preliminar y capítulo 17, §§17.1–17.4.

← Anterior · Índice del tratado · Siguiente →