Índice de resultados

Fecha de última modificación

11 de octubre de 2026

Índice del tratado

667 unidades con ID estables. Las dependencias deductivas no se confunden con cobertura formal.

Capítulo 0 — Niveles, lenguajes y sistemas formales

ID Unidad Selección Lean
TLOG-CNV-00001 Estratificación de trabajo no seleccionado
TLOG-DEF-00001 Alfabeto formal no seleccionado
TLOG-DEF-00002 Expresión sobre un alfabeto no seleccionado
TLOG-DEF-00003 Especificación de formación no seleccionado
TLOG-DEF-00004 Lenguaje formal no seleccionado
TLOG-CNV-00002 Datos mínimos de un sistema objeto no seleccionado

Capítulo 1 — Sintaxis proposicional

ID Unidad Selección Lean
TLOG-CNV-00003 Sistema proposicional de referencia CPL no seleccionado
TLOG-DEF-00005 Alfabeto de CPL no seleccionado
TLOG-DEF-00006 Constructores proposicionales no seleccionado
TLOG-DEF-00007 Fórmulas proposicionales de CPL candidato
TLOG-MTH-00001 Principio de inducción estructural proposicional candidato
TLOG-LEM-00001 Balance y segmentos iniciales de una fórmula no seleccionado
TLOG-MTH-00002 Legibilidad única de las fórmulas proposicionales candidato
TLOG-MTH-00003 Teorema de recursión estructural proposicional candidato
TLOG-DEF-00008 Conjunto de subfórmulas no seleccionado
TLOG-DEF-00009 Rango de una fórmula no seleccionado
TLOG-CNV-00004 Omisión controlada de paréntesis no seleccionado

Capítulo 2 — Semántica proposicional

ID Unidad Selección Lean
TLOG-CNV-00005 Semántica bivalente de los conectivos de CPL no seleccionado
TLOG-DEF-00010 Valuación de CPL no seleccionado
TLOG-MTH-00004 Extensión única de una valuación a todas las fórmulas candidato
TLOG-DEF-00011 Satisfacción proposicional local no seleccionado
TLOG-LEM-00002 Localidad de la evaluación proposicional no seleccionado
TLOG-DEF-00012 Satisfacción de un conjunto y conjunto de modelos no seleccionado
TLOG-DEF-00013 Satisfacibilidad e insatisfacibilidad no seleccionado
TLOG-DEF-00014 Validez proposicional no seleccionado
TLOG-DEF-00015 Consecuencia semántica proposicional no seleccionado
TLOG-DEF-00016 Equivalencia semántica proposicional no seleccionado
TLOG-PRO-00001 Caracterizaciones básicas de las nociones semánticas no seleccionado
TLOG-PRO-00002 Reflexividad, monotonía y corte semántico no seleccionado
TLOG-DEF-00017 Soporte proposicional no seleccionado
TLOG-LEM-00003 Finitud del soporte proposicional no seleccionado
TLOG-DEF-00018 Tabla de verdad de una familia finita no seleccionado
TLOG-MTH-00005 Reducción finita de la evaluación candidato
TLOG-MTH-00006 Procedimientos finitos de decisión en CPL no seleccionado

Capítulo 3 — Cálculo proposicional

ID Unidad Selección Lean
TLOG-CNV-00006 Cálculo proposicional de referencia HCPL no seleccionado
TLOG-AXM-00001 Base axiomática de HCPL no seleccionado
TLOG-RUL-00001 Modus ponens no seleccionado
TLOG-DEF-00019 Derivación en HCPL no seleccionado
TLOG-DEF-00020 Derivabilidad y teorema en HCPL no seleccionado
TLOG-MTH-00007 Principio de inducción sobre derivaciones candidato
TLOG-PRO-00003 Propiedades estructurales básicas de la derivabilidad no seleccionado
TLOG-LEM-00004 Autoimplicación no seleccionado
TLOG-MTH-00008 Teorema de deducción de HCPL candidato
TLOG-PRO-00004 Reglas derivadas básicas de HCPL no seleccionado
TLOG-COR-00001 Internalización finita de premisas no seleccionado

Capítulo 4 — Corrección y completitud proposicional

ID Unidad Selección Lean
TLOG-LEM-00005 Validez semántica de los esquemas axiomáticos de HCPL no seleccionado
TLOG-LEM-00006 Preservación semántica de modus ponens no seleccionado
TLOG-MTH-00009 Corrección de HCPL respecto de CPL candidato
TLOG-COR-00002 Todo teorema de HCPL es válido no seleccionado
TLOG-DEF-00021 Consistencia y consistencia maximal en HCPL no seleccionado
TLOG-LEM-00007 Núcleo clásico derivado de HCPL no seleccionado
TLOG-LEM-00008 Tests de consistencia y trivialidad no seleccionado
TLOG-MTH-00010 Lema de Lindenbaum enumerable para CPL no seleccionado
TLOG-MTH-00011 Lema de verdad para la valuación canónica candidato
TLOG-MTH-00012 Existencia de modelo para conjuntos consistentes no seleccionado
TLOG-MTH-00013 Completitud fuerte de HCPL respecto de CPL no seleccionado
TLOG-COR-00003 Adecuación, finitariedad semántica y compacidad proposicional no seleccionado

Capítulo 5 — Signaturas, términos y fórmulas

ID Unidad Selección Lean
TLOG-CNV-00007 Familia de lenguajes de primer orden con igualdad no seleccionado
TLOG-DEF-00022 Signatura unisortada y aridades no seleccionado
TLOG-DEF-00023 Variables individuales y alfabeto de una signatura no seleccionado
TLOG-DEF-00024 Términos de primer orden candidato
TLOG-LEM-00009 Legibilidad única de términos no seleccionado
TLOG-MTH-00014 Principio de inducción estructural sobre términos candidato
TLOG-DEF-00025 Fórmulas atómicas con igualdad lógica no seleccionado
TLOG-DEF-00026 Fórmulas de primer orden con igualdad candidato
TLOG-LEM-00010 Legibilidad única de fórmulas de primer orden candidato
TLOG-MTH-00015 Inducción estructural de fórmulas de primer orden candidato
TLOG-DEF-00027 Subfórmulas y rango sintáctico de primer orden no seleccionado
TLOG-CNV-00008 Impresión compacta y alcance explícito de cuantificadores no seleccionado

Capítulo 6 — Variables, sustitución y recursión sintáctica

ID Unidad Selección Lean
TLOG-DEF-00028 Direcciones de ocurrencias individuales no seleccionado
TLOG-DEF-00029 Alcance sintáctico y relación de vinculación candidato
TLOG-LEM-00011 Unicidad del cuantificador vinculante no seleccionado
TLOG-DEF-00030 Ocurrencias libres y variables libres no seleccionado
TLOG-MTH-00016 Ecuaciones estructurales de variables libres candidato
TLOG-DEF-00031 Sentencias y fórmulas cerradas no seleccionado
TLOG-PRO-00005 Finitud y coexistencia de ocurrencias libres y ligadas no seleccionado
TLOG-MTH-00017 Existencia y unicidad de recursión estructural sobre términos candidato
TLOG-MTH-00018 Existencia y unicidad de recursión estructural sobre fórmulas candidato
TLOG-COR-00004 Caracterización funcional única de variables libres no seleccionado
TLOG-DEF-00032 Sustitución simultánea sobre términos candidato
TLOG-LEM-00012 Soporte de variables bajo sustitución de términos no seleccionado
TLOG-PRO-00006 Identidad y composición de sustituciones de términos no seleccionado
TLOG-DEF-00033 Soporte total de nombres y selección canónica de frescos no seleccionado
TLOG-DEF-00034 Libertad para sustituir y control de captura candidato
TLOG-LEM-00013 Criterio de captura por ocurrencias candidato
TLOG-DEF-00035 Sustitución literal segura sobre fórmulas candidato
TLOG-LEM-00014 Soporte libre de la sustitución segura no seleccionado
TLOG-DEF-00036 Paso alfa elemental y equivalencia alfa candidato
TLOG-PRO-00007 Invariancia de variables libres y rango bajo alfa no seleccionado
TLOG-MTH-00019 Sustitución total determinista sin captura candidato
TLOG-DEF-00037 Código por profundidad del vinculante candidato
TLOG-MTH-00020 Equivalencia alfa caracterizada por códigos candidato
TLOG-DEF-00038 Sustitución global simultánea sobre fórmulas candidato
TLOG-LEM-00015 Transporte de ocurrencias, soporte y localidad candidato
TLOG-MTH-00021 Compatibilidad alfa e identidad de sustitución no seleccionado
TLOG-MTH-00022 Composición de sustituciones de fórmulas módulo alfa candidato
TLOG-COR-00005 Acción derecha de sustituciones sobre clases alfa no seleccionado

Capítulo 7 — Estructuras, asignaciones e interpretación

ID Unidad Selección Lean
TLOG-CNV-00009 Separación de estructura, asignación e interpretación no seleccionado
TLOG-DEF-00039 Estructura unisortada para una signatura no seleccionado
TLOG-PRO-00008 Existencia de estructuras sobre universos no vacíos en ZF no seleccionado
TLOG-DEF-00040 Asignación y actualización puntual no seleccionado
TLOG-LEM-00016 Leyes de actualizaciones de asignación no seleccionado
TLOG-MTH-00023 Existencia y unicidad de evaluación de términos candidato
TLOG-LEM-00017 Localidad de la evaluación de términos no seleccionado
TLOG-MTH-00024 Lema de sustitución semántica para términos candidato
TLOG-DEF-00041 Inclusión de signaturas, reducto y expansión no seleccionado
TLOG-PRO-00009 Reducción iterada y expansión uniforme sin elección no seleccionado
TLOG-LEM-00018 Persistencia de términos, fórmulas y ligadura no seleccionado
TLOG-MTH-00025 Invariancia de evaluación bajo reductos candidato
TLOG-DEF-00042 Homomorfismo, embedding e isomorfismo no seleccionado
TLOG-MTH-00026 Naturalidad de evaluación respecto de homomorfismos candidato
TLOG-PRO-00010 Identidades, composición e inversas de aplicaciones estructurales no seleccionado
TLOG-DEF-00043 Subestructura e inclusión inducida no seleccionado
TLOG-PRO-00011 Existencia y unicidad de subestructuras inducidas y generadas no seleccionado

Capítulo 8 — Satisfacción, verdad y consecuencia

ID Unidad Selección Lean
TLOG-CNV-00010 Espacios de asignaciones y funciones booleanas no seleccionado
TLOG-DEF-00044 Dato semántico inicial sobre átomos no seleccionado
TLOG-DEF-00045 Operadores booleanos y cuantificación semántica no seleccionado
TLOG-MTH-00027 Existencia y unicidad de satisfacción de fórmulas candidato
TLOG-LEM-00019 Localidad de satisfacción por variables libres candidato
TLOG-COR-00006 Independencia de asignación para sentencias no seleccionado
TLOG-PRO-00012 Dualidad de cuantificadores y cuantificación vacua no seleccionado
TLOG-LEM-00020 Compatibilidad de asignaciones inducidas con cambios puntuales no seleccionado
TLOG-MTH-00028 Sustitución semántica literal libre de captura candidato
TLOG-LEM-00021 Renombrado alfa elemental conserva satisfacción no seleccionado
TLOG-MTH-00029 Invariancia de satisfacción bajo equivalencia alfa no seleccionado
TLOG-MTH-00030 Sustitución semántica simultánea global candidato
TLOG-COR-00007 Sustitución simple total sin captura y satisfacción no seleccionado
TLOG-MTH-00031 Invariancia de satisfacción bajo reductos no seleccionado
TLOG-MTH-00032 Invariancia de satisfacción bajo isomorfismos candidato
TLOG-DEF-00046 Fragmento de fórmulas sin cuantificadores no seleccionado
TLOG-PRO-00013 Invariancia sin cuantificadores bajo embeddings no seleccionado
TLOG-DEF-00047 Satisfacción simultánea y asignaciones realizadoras no seleccionado
TLOG-LEM-00022 Álgebra y localidad de los conjuntos de asignaciones no seleccionado
TLOG-DEF-00048 Modelo de un conjunto de sentencias y satisfacibilidad no seleccionado
TLOG-PRO-00014 Independencia de asignación y naturaleza de la clase de modelos no seleccionado
TLOG-DEF-00049 Consecuencia local, validez y equivalencia semántica no seleccionado
TLOG-PRO-00015 Consecuencia, negación, validez y sentencias no seleccionado
TLOG-PRO-00016 Reflexividad, monotonía y corte semántico no seleccionado
TLOG-PRO-00017 Implicación interna y generalización con condición lateral candidato
TLOG-DEF-00050 Generalización canónica y consecuencia global no seleccionado
TLOG-PRO-00018 Clausura universal y contraejemplo de consecuencia no seleccionado
TLOG-DEF-00051 Teoría de una estructura y clausura semántica de sentencias no seleccionado
TLOG-PRO-00019 Extensividad, monotonía, idempotencia y modelos invariantes no seleccionado
TLOG-MTH-00033 La consecuencia no depende de símbolos nuevos candidato

Capítulo 9 — Sistemas deductivos y teorías

ID Unidad Selección Lean
TLOG-CNV-00011 Cálculo (H_^{=}) no seleccionado
TLOG-AXM-00002 Levantamiento de H1–H12 no seleccionado
TLOG-AXM-00003 Cuantificadores primitivos y sustitución segura no seleccionado
TLOG-AXM-00004 Reflexividad y sustitución de iguales no seleccionado
TLOG-DEF-00052 Axiomas básicos y generalizaciones finitas no seleccionado
TLOG-RUL-00002 Modus ponens de primer orden no seleccionado
TLOG-DEF-00053 Derivación desde un conjunto de fórmulas candidato
TLOG-DEF-00054 Derivabilidad en (H_^{=}) no seleccionado
TLOG-MTH-00034 Principio de inducción deductiva candidato
TLOG-PRO-00020 Premisa, axioma, MP, monotonía, finitariedad y corte no seleccionado
TLOG-MTH-00035 Generalización bajo premisas independientes candidato
TLOG-LEM-00023 Levantamiento de demostraciones proposicionales candidato
TLOG-MTH-00036 Descarga de una premisa para un cálculo con MP candidato
TLOG-PRO-00021 Conjunción, disyunción, bicondicional y reducción clásica no seleccionado
TLOG-PRO-00022 Simetría, transitividad y congruencia no seleccionado
TLOG-PRO-00023 Particularización, introducción existencial y dualidad no seleccionado
TLOG-MTH-00037 Equivalencia alfa implica equivalencia demostrable candidato
TLOG-DEF-00055 Clausura deductiva y teoría sintáctica no seleccionado
TLOG-PRO-00024 Extensividad, monotonía, idempotencia y cierre de teorías no seleccionado
TLOG-DEF-00056 Contradicción fija y consistencia sintáctica no seleccionado
TLOG-PRO-00025 Explosión, pares contradictorios y adjunción no seleccionado
TLOG-MTH-00038 Las sentencias como premisas autorizan generalización candidato

Capítulo 10 — Teorema de corrección

ID Unidad Selección Lean
TLOG-LEM-00024 Validez de las instancias proposicionales de primer orden no seleccionado
TLOG-LEM-00025 Validez de los esquemas cuantificacionales Q1–Q5 candidato
TLOG-LEM-00026 Validez de los esquemas de igualdad E1–E2 candidato
TLOG-LEM-00027 Preservación de satisfacción bajo modus ponens no seleccionado
TLOG-PRO-00026 La validez subsiste bajo prefijos universales finitos no seleccionado
TLOG-MTH-00039 Todas las instancias axiomáticas del cálculo son válidas no seleccionado
TLOG-MTH-00040 Teorema de corrección de primer orden con igualdad candidato
TLOG-COR-00008 Los teoremas son válidos y los contramodelos impiden demostraciones no seleccionado
TLOG-COR-00009 La existencia de realización semántica implica consistencia sintáctica no seleccionado

Capítulo 11 — Completitud y compacidad

ID Unidad Selección Lean
TLOG-CNV-00012 Lenguaje numerable y frontera de elección no seleccionado
TLOG-LEM-00028 Eliminación finita de constantes auxiliares no seleccionado
TLOG-LEM-00029 Axioma de Henkin con constante fresca candidato
TLOG-DEF-00057 Ampliaciones de lenguaje y axiomas testigo por niveles no seleccionado
TLOG-LEM-00030 La unión numerable es consistente y testimoniada no seleccionado
TLOG-MTH-00041 Extensión completa, consistente y de Henkin candidato
TLOG-DEF-00058 Universo cociente e interpretaciones por términos cerrados no seleccionado
TLOG-LEM-00031 Equivalencia, congruencia y sección canónica no seleccionado
TLOG-MTH-00042 Lema de verdad del modelo canónico candidato
TLOG-MTH-00043 Existencia de modelo en lenguaje numerable no seleccionado
TLOG-PRO-00027 Consistencia, satisfacibilidad y compacidad sentencial numerable no seleccionado
TLOG-PRO-00028 Reducción a soporte numerable y expansión uniforme no seleccionado
TLOG-DEF-00059 Parámetros constantes y traducción sentencial no seleccionado
TLOG-LEM-00032 Correspondencia semántica entre parámetros y asignaciones candidato
TLOG-LEM-00033 Clausura existencial de una familia finita consistente candidato
TLOG-PRO-00029 Satisfacibilidad finita de las sentencias parametrizadas no seleccionado
TLOG-MTH-00044 Completitud fuerte local para premisas numerables candidato
TLOG-COR-00010 Adecuación, finitariedad semántica y compacidad local numerable no seleccionado
TLOG-CNV-00013 Régimen de buen orden y principio booleano de ideal primo no seleccionado
TLOG-LEM-00034 Torre de Henkin sobre una signatura arbitraria, sin elección candidato
TLOG-MTH-00045 Modelo de Henkin en toda signatura bien ordenable, sin selector global candidato
TLOG-MTH-00046 Completitud fuerte local y compacidad sobre firmas bien ordenables candidato
TLOG-MTH-00047 BPI proporciona modelos a toda teoría consistente de sentencias candidato
TLOG-MTH-00048 BPI implica completitud fuerte y compacidad irrestrictas no seleccionado
TLOG-MTH-00049 La compacidad irrestricta de primer orden implica BPI no seleccionado
TLOG-COR-00011 Fuerza exacta de compacidad y completitud en ZF no seleccionado
TLOG-COR-00012 Vector de adecuación por hipótesis y cierre tipado no seleccionado

Capítulo 12 — El lenguaje de la teoría de conjuntos y los axiomas de ZF

ID Unidad Selección Lean
TLOG-CNV-00014 Separación estricta de ZF metateórica y ZF objeto no seleccionado
TLOG-DEF-00060 Signatura pura de pertenencia candidato
TLOG-DEF-00061 Abreviaciones conservativas y normalización de vinculantes no seleccionado
TLOG-AXM-00005 Axioma de extensionalidad no seleccionado
TLOG-AXM-00006 Axioma de pares no seleccionado
TLOG-AXM-00007 Axioma de unión no seleccionado
TLOG-AXM-00008 Axioma del conjunto potencia no seleccionado
TLOG-AXM-00009 Axioma del infinito en lenguaje primitivo no seleccionado
TLOG-AXM-00010 Esquema de separación con parámetros candidato
TLOG-AXM-00011 Esquema de reemplazo funcional sobre conjuntos candidato
TLOG-AXM-00012 Axioma de fundamentación o regularidad no seleccionado
TLOG-DEF-00062 Conjunto de axiomas objeto de ZF no seleccionado
TLOG-LEM-00035 Conjuntidad y numerabilidad de las instancias de ZF no seleccionado
TLOG-DEF-00063 Teoría objeto ZF, derivabilidad y satisfacción no seleccionado
TLOG-PRO-00030 Existencia y unicidad del conjunto vacío en ZF objeto no seleccionado
TLOG-PRO-00031 Imposibilidad de un conjunto universal: argumento de Russell no seleccionado
TLOG-PRO-00032 La regularidad excluye la autopertenencia no seleccionado
TLOG-MTH-00050 Existencia condicional de modelos de ZF objeto no seleccionado
TLOG-CNV-00015 Equivalencia de presentaciones de una teoría objeto no seleccionado
TLOG-LEM-00036 Invariancia deductiva de instancias bajo conversión alfa candidato
TLOG-PRO-00033 Equivalencia de los dos esquemas paramétricos de separación no seleccionado
TLOG-PRO-00034 Equivalencia de funcionalidad global y sobre el conjunto de partida candidato
TLOG-DEF-00064 Esquema de cobertura de imágenes funcionales no seleccionado
TLOG-MTH-00051 Equivalencia de cobertura funcional y reemplazo en presencia de separación no seleccionado
TLOG-PRO-00035 El conjunto vacío se demuestra con pares y separación no seleccionado
TLOG-DEF-00065 Extensión por una constante definida no seleccionado
TLOG-MTH-00052 Conservatividad sintáctica y semántica de definiciones únicas candidato
TLOG-COR-00013 La introducción de () no crea teoremas antiguos no seleccionado
TLOG-LEM-00037 Particularización correcta de las instancias sentenciales no seleccionado
TLOG-LEM-00038 Unicidad extensional de subconjuntos e imágenes definidos no seleccionado
TLOG-MTH-00053 Invariancia de la teoría objeto bajo las presentaciones alternativas autorizadas no seleccionado

Capítulo 13 — Construcciones elementales de conjuntos

ID Unidad Selección Lean
TLOG-CNV-00016 Fórmulas caracterizadoras y nombres eliminables no seleccionado
TLOG-LEM-00039 Unicidad de una descripción extensional no seleccionado
TLOG-PRO-00036 Existencia y unicidad del par no ordenado no seleccionado
TLOG-DEF-00066 Par no ordenado y singleton como extensiones definicionales candidato
TLOG-PRO-00037 Membresía y leyes extensionales de pares no seleccionado
TLOG-PRO-00038 Existencia y unicidad de unión de una familia no seleccionado
TLOG-DEF-00067 Macro de unión y su regla de expansión no seleccionado
TLOG-PRO-00039 Unión binaria por par más unión y leyes básicas no seleccionado
TLOG-PRO-00040 Existencia y unicidad del conjunto potencia no seleccionado
TLOG-DEF-00068 Macro del conjunto potencia no seleccionado
TLOG-PRO-00041 Membresía, monotonía y reflexión de inclusión para potencia no seleccionado
TLOG-DEF-00069 Subconjunto separado por fórmula y parámetros candidato
TLOG-PRO-00042 Intersección y diferencia relativas no seleccionado
TLOG-MTH-00054 Eliminación finita de símbolos funcionales definibles candidato
TLOG-COR-00014 Construcción uniforme de familias finitas no seleccionado
TLOG-CNV-00017 Fórmulas funcionales sobre un dominio conjunto no seleccionado
TLOG-PRO-00043 Existencia y unicidad de imagen funcional por reemplazo candidato
TLOG-DEF-00070 Macro parcial de imagen funcional no seleccionado
TLOG-PRO-00044 Identidad, constante y monotonía de imágenes no seleccionado
TLOG-PRO-00045 Composición de imágenes funcionales definibles no seleccionado
TLOG-PRO-00046 Imagen acotada de relación no funcional no seleccionado
TLOG-CNV-00018 Intersección de familias: absoluta y relativa no seleccionado
TLOG-PRO-00047 Existencia y unicidad de intersección de familia no vacía candidato
TLOG-DEF-00071 Macro parcial de intersección no vacía no seleccionado
TLOG-PRO-00048 Leyes de intersección, pares y antitonicidad no seleccionado
TLOG-DEF-00072 Intersección relativa dentro de un ambiente no seleccionado
TLOG-PRO-00049 Reconstrucción de intersección mediante separación sobre la unión no seleccionado
TLOG-PRO-00050 Unión de imágenes funcionalmente indexadas candidato
TLOG-LEM-00040 Imposibilidad de intersección absoluta de familia vacía no seleccionado
TLOG-MTH-00055 Totalización y eliminación de operaciones definibles bajo hipótesis candidato
TLOG-COR-00015 Cierre de construcciones elementales y frontera de relaciones no seleccionado

Capítulo 14 — Relaciones, productos y funciones

ID Unidad Selección Lean
TLOG-CNV-00019 Par ordenado como descripción interna y no como primitivo no seleccionado
TLOG-DEF-00073 Gráfica pura del par ordenado candidato
TLOG-PRO-00051 Totalidad y unicidad del constructor codificado no seleccionado
TLOG-LEM-00041 Intersección y unión internas de un par ordenado no seleccionado
TLOG-MTH-00056 Teorema de identidad de Kuratowski en ZF objeto candidato
TLOG-DEF-00074 Fórmula de producto con cota explícita no seleccionado
TLOG-PRO-00052 Existencia y unicidad de AB, sin elección candidato
TLOG-PRO-00053 Vacío, no vacío, monotonía y recuperación de factores no seleccionado
TLOG-DEF-00075 Relación tipada RAB y relación sin factores declarados no seleccionado
TLOG-PRO-00054 Relación de extensión para una condición sobre un producto no seleccionado
TLOG-DEF-00076 Dominios y recorridos por separación sobre una cota uniforme no seleccionado
TLOG-PRO-00055 Caracterización de coordenadas y cotas de una relación candidato
TLOG-PRO-00056 Restricción acotada y estabilidad de las coordenadas no seleccionado
TLOG-PRO-00057 Dos relaciones son iguales exactamente cuando tienen los mismos pares no seleccionado
TLOG-MTH-00057 Eliminación de pares ordenados y productos cartesianos candidato
TLOG-COR-00016 Infraestructura relacional construida sin axioma de elección no seleccionado
TLOG-CNV-00020 Grafo funcional y flecha tipada no seleccionado
TLOG-DEF-00077 Función parcial y aplicación total entre conjuntos candidato
TLOG-PRO-00058 Caracterización de la funcionalidad por testigos únicos no seleccionado
TLOG-DEF-00078 Valor f(x) y su dominio exacto de impresión no seleccionado
TLOG-PRO-00059 Dominio, recorrido y codominio declarado no seleccionado
TLOG-DEF-00079 Espacio funcional B^A como subconjunto de una potencia no seleccionado
TLOG-PRO-00060 Funciones como elementos de una potencia y casos vacíos no seleccionado
TLOG-PRO-00061 Del reemplazo funcional a un conjunto de pares candidato
TLOG-DEF-00080 Imágenes de subconjuntos, con preimagen guardada no seleccionado
TLOG-PRO-00062 Álgebra de imagen directa e inversa no seleccionado
TLOG-DEF-00081 Gráfico identidad y composición relacional acotada candidato
TLOG-PRO-00063 Dominio exacto de la composición de funciones candidato
TLOG-PRO-00064 Leyes del monoide parcial de composición no seleccionado
TLOG-DEF-00082 Relación conversa de un grafo no seleccionado
TLOG-PRO-00065 Converso funcional si y sólo si inyectividad candidato
TLOG-MTH-00058 Inversa bilateral y biyectividad relativa al codominio candidato
TLOG-MTH-00059 Eliminación de aplicaciones, composición e inversas guardadas candidato
TLOG-COR-00017 Funciones conjuntistas disponibles sin elección no seleccionado

Capítulo 15 — Equivalencias, cocientes y órdenes

ID Unidad Selección Lean
TLOG-CNV-00021 Equivalencias relativas a un conjunto base no seleccionado
TLOG-DEF-00083 Reflexividad, simetría y transitividad con guarda candidato
TLOG-PRO-00066 Diagonal, conversa y composición no seleccionado
TLOG-DEF-00084 Gráfica pura de la clase relativa candidato
TLOG-PRO-00067 Existencia, unicidad y testigo interno no seleccionado
TLOG-LEM-00042 Criterio fundamental de coincidencia candidato
TLOG-PRO-00068 Coincidencia o disjunción, sin elección no seleccionado
TLOG-DEF-00085 Cociente acotado por el conjunto potencia no seleccionado
TLOG-PRO-00069 Construcción efectiva del cociente y casos vacíos candidato
TLOG-DEF-00086 Partición con tratamiento exacto de (A=) no seleccionado
TLOG-PRO-00070 Construcción por separación sobre (AA) no seleccionado
TLOG-MTH-00060 La correspondencia es una biyección de conjuntos candidato
TLOG-DEF-00087 Proyección al cociente por separación no seleccionado
TLOG-PRO-00071 Sobreyección, fibras e igualdad de valores candidato
TLOG-MTH-00061 Propiedad universal del cociente candidato
TLOG-PRO-00072 Aplicaciones compatibles e identidad/composición inducidas no seleccionado
TLOG-DEF-00088 Núcleo relativo al dominio no seleccionado
TLOG-MTH-00062 Cociente por núcleo e imagen exacta candidato
TLOG-COR-00018 Cocientes y descenso sin elección de representantes no seleccionado
TLOG-CNV-00022 Orden no estricto, orden estricto y universo declarado no seleccionado
TLOG-DEF-00089 Reflexividad y transitividad relativas candidato
TLOG-PRO-00073 La parte simétrica es una equivalencia candidato
TLOG-DEF-00090 Antisimetría, totalidad y orden parcial no seleccionado
TLOG-MTH-00063 Orden parcial canónico sobre clases simétricas candidato
TLOG-PRO-00074 Antisimetría y trivialidad de la parte simétrica no seleccionado
TLOG-DEF-00091 Irreflexividad, transitividad y tricotomía no seleccionado
TLOG-MTH-00064 Las dos presentaciones de un orden parcial candidato
TLOG-PRO-00075 Totalidad equivale a tricotomía estricta no seleccionado
TLOG-DEF-00092 Monotonía, reflexión, embedding e isomorfismo candidato
TLOG-PRO-00076 Identidades, composición e inyectividad no seleccionado
TLOG-DEF-00093 Subconjunto cadena, mínimos, máximos, extremos no seleccionado
TLOG-PRO-00077 Extremos únicos; minimalidad en un orden lineal no seleccionado
TLOG-DEF-00094 Orden bien fundado en el sentido de buen orden no seleccionado
TLOG-PRO-00078 Todo buen orden es lineal y se hereda por restricción candidato
TLOG-DEF-00095 Saturación bilateral e independencia del representante candidato
TLOG-MTH-00065 Criterio necesario y suficiente de buena definición relacional candidato
TLOG-PRO-00079 Una relación reflexiva saturada identifica sólo puntos mutuamente relacionados candidato
TLOG-PRO-00080 Descenso de una operación binaria bajo congruencia candidato
TLOG-MTH-00066 Monotonía y factorización hacia órdenes parciales candidato
TLOG-COR-00019 Infraestructura de equivalencias y órdenes sin elección no seleccionado

Capítulo 16 — Naturales, inducción, recursión y secuencias finitas

ID Unidad Selección Lean
TLOG-CNV-00023 Construcción de von Neumann y tipado de las abreviaciones no seleccionado
TLOG-DEF-00096 Fórmula pura de sucesor no seleccionado
TLOG-PRO-00081 El sucesor existe para todo conjunto no seleccionado
TLOG-DEF-00097 Guarda inductiva sin cuantificación sobre fórmulas no seleccionado
TLOG-PRO-00082 Recuperación exacta del axioma de infinito no seleccionado
TLOG-DEF-00098 Intersección definible de inductivos acotados candidato
TLOG-PRO-00083 Existencia de (W_I) y clausura por sucesor candidato
TLOG-LEM-00043 (W_I) está contenido en todo conjunto inductivo candidato
TLOG-MTH-00067 Existencia y unicidad del menor inductivo candidato
TLOG-DEF-00099 Gráfica única de los naturales de von Neumann no seleccionado
TLOG-PRO-00084 El menor inductivo contiene cero y todos sus sucesores no seleccionado
TLOG-MTH-00068 Inducción para cada fórmula del lenguaje de pertenencia candidato
TLOG-PRO-00085 Separación entre cero y sucesores, y cancelación candidato
TLOG-PRO-00086 Cero o sucesor de un único natural candidato
TLOG-PRO-00087 El primer elemento aparece en cada sucesor no seleccionado
TLOG-PRO-00088 Cada natural es transitivo candidato
TLOG-PRO-00089 Todo miembro de un natural es natural no seleccionado
TLOG-MTH-00069 Estructura interna con cero, sucesor e inducción candidato
TLOG-COR-00020 Núcleo natural construido sin elección no seleccionado
TLOG-CNV-00024 Recursión con valores en un conjunto fijado no seleccionado
TLOG-DEF-00100 Gráfica de aproximación admisible candidato
TLOG-LEM-00044 Segmentos sucesores, cero y antecesores candidato
TLOG-LEM-00045 Prolongación canónica de una aproximación candidato
TLOG-PRO-00090 Existencia mediante inducción sin recursión previa candidato
TLOG-LEM-00046 Unicidad de valores en dominios solapados candidato
TLOG-MTH-00070 Existencia y unicidad de la función recursiva candidato
TLOG-PRO-00091 Gráfico simultáneo de una familia recursiva candidato
TLOG-DEF-00101 Función de suma mediante recursión con parámetro candidato
TLOG-PRO-00092 Suma total y ecuaciones de recursión no seleccionado
TLOG-LEM-00047 Identidad izquierda y sucesor izquierdo candidato
TLOG-MTH-00071 El monoide conmutativo aditivo de \(\omega\) candidato
TLOG-PRO-00093 Cancelación en ambos argumentos no seleccionado
TLOG-DEF-00102 Producto por suma iterada candidato
TLOG-PRO-00094 Ceros y unidades multiplicativas no seleccionado
TLOG-LEM-00048 \((a+b)\cdot c=a\cdot c+b\cdot c\) candidato
TLOG-PRO-00095 \(a\cdot(b+c)=a\cdot b+a\cdot c\) candidato
TLOG-MTH-00072 Leyes fundamentales de la multiplicación de naturales candidato
TLOG-COR-00021 Estructura aritmética interna sin elección no seleccionado
TLOG-LEM-00049 Todo elemento de un natural tiene sucesor interno o terminal no seleccionado
TLOG-MTH-00073 Comparabilidad estricta de naturales candidato
TLOG-PRO-00096 Irreflexividad, transitividad y totalidad no seleccionado
TLOG-MTH-00074 Mínimo de todo subconjunto no vacío no seleccionado
TLOG-COR-00022 Inducción y principio del mínimo contraejemplo no seleccionado
TLOG-DEF-00103 Relación \(\leq\) y su expansión conjuntista no seleccionado
TLOG-PRO-00097 Equivalencia entre \(m\leq n\) y \(m\subseteq n\) no seleccionado
TLOG-LEM-00050 Desplazamiento de un segmento finito candidato
TLOG-DEF-00104 Secuencia finita y longitud candidato
TLOG-PRO-00098 Conjunto de todas las secuencias finitas candidato
TLOG-LEM-00051 Existencia y composición de restricciones no seleccionado
TLOG-DEF-00105 Extensión por un valor final no seleccionado
TLOG-PRO-00099 Toda secuencia no vacía tiene último término único candidato
TLOG-MTH-00075 Principio de inducción por adjunción candidato
TLOG-DEF-00106 Unión del prefijo y la cola desplazada candidato
TLOG-PRO-00100 Concatenación de secuencias finitas candidato
TLOG-LEM-00052 Vacío derecho y compatibilidad con adjunción no seleccionado
TLOG-MTH-00076 El monoide de secuencias finitas candidato
TLOG-PRO-00101 Restricción inicial como orden parcial no seleccionado
TLOG-LEM-00053 Inyectividad de la concatenación derecha con prefijo fijo candidato
TLOG-LEM-00054 Transformación de secuencias mediante una función candidato
TLOG-MTH-00077 Plegado izquierdo único en cualquier alfabeto conjunto candidato
TLOG-PRO-00102 Familia indexada de espacios de palabras no seleccionado
TLOG-COR-00023 Interfaz finitaria cerrada dentro de ZF objeto no seleccionado

Capítulo 17 — Computabilidad mínima para la metamatemática

ID Unidad Selección Lean
TLOG-CNV-00025 Alcance de la palabra computable no seleccionado
TLOG-DEF-00107 Cuatro coordenadas y tres constructores disjuntos candidato
TLOG-DEF-00108 Programa de \(r\) registros con \(n\) etiquetas candidato
TLOG-PRO-00103 \(\operatorname{Prog}_q\) es un conjunto no vacío no seleccionado
TLOG-DEF-00109 Estado con contador de instrucciones y registros no seleccionado
TLOG-LEM-00055 Cada rama no nula tiene predecesor único no seleccionado
TLOG-DEF-00110 Transición totalizada con parada absorbente candidato
TLOG-PRO-00104 \(E_P\) es función total \(C_P\to C_P\) candidato
TLOG-MTH-00078 Existe una única órbita de estados candidato
TLOG-PRO-00105 Trazas finitas existentes y verificables candidato
TLOG-DEF-00111 Predicado de parada en tiempo \(t\) no seleccionado
TLOG-LEM-00056 Parada absorbente y tiempo mínimo no seleccionado
TLOG-DEF-00112 Gráfica calculada, posiblemente parcial candidato
TLOG-PRO-00106 Conjunto de pares y univocidad del resultado no seleccionado
TLOG-DEF-00113 Función parcial computable-RM no seleccionado
TLOG-DEF-00114 Dos nociones operacionales diferentes candidato
TLOG-PRO-00107 Reunión creciente de secciones decidibles acotadas candidato
TLOG-PRO-00108 Identidad, cero constante y divergencia universal no seleccionado
TLOG-PRO-00109 Complementos de relaciones decidibles son semidecidibles candidato
TLOG-COR-00024 Infraestructura operacional mínima disponible no seleccionado
TLOG-CNV-00026 Compilación finita y separación de niveles no seleccionado
TLOG-DEF-00115 Macrobloques de registros con guardas de frescura candidato
TLOG-LEM-00057 Saltos incondicionales, borrado y transferencia finitos candidato
TLOG-LEM-00058 Copia conservativa con auxiliar restaurado candidato
TLOG-PRO-00110 Relocalización de registros y de etiquetas sin colisiones candidato
TLOG-MTH-00079 Compilación de diagramas de control finito a programas RM candidato
TLOG-DEF-00116 Bloque de un paso de programa fijo con retorno candidato
TLOG-LEM-00059 Exactitud de la simulación de un paso y detección de HALT candidato
TLOG-PRO-00111 Simuladores finitos de un programa individual no seleccionado
TLOG-MTH-00080 Clausura bajo sustitución general de funciones parciales computables candidato
TLOG-PRO-00112 Proyecciones, sucesor y constantes son computables-RM no seleccionado
TLOG-PRO-00113 Suma y multiplicación son computables-RM no seleccionado
TLOG-DEF-00117 Producto de controles finitos y planificación alternada candidato
TLOG-LEM-00060 Justicia de la planificación e identidad de las dos órbitas candidato
TLOG-MTH-00081 Doble semidecisión implica decidibilidad candidato
TLOG-COR-00025 Caracterización de decisión por doble semidecisión no seleccionado
TLOG-PRO-00114 Unión e intersección de relaciones semidecidibles candidato
TLOG-PRO-00115 Clausura booleana de las relaciones decidibles no seleccionado
TLOG-MTH-00082 Preimágenes semidecidibles y decidibles por mapas computables candidato
TLOG-COR-00026 Cierre operativo del capítulo y frontera de aritmetización no seleccionado

Capítulo 18 — Codificación efectiva de expresiones y derivaciones

ID Unidad Selección Lean
TLOG-CNV-00027 Tres niveles y alcance de la efectividad no seleccionado
TLOG-DEF-00118 Presentación efectiva de un alfabeto no seleccionado
TLOG-DEF-00119 Presentación efectiva de una signatura no seleccionado
TLOG-LEM-00061 Comparaciones y bucles numéricos compilables en RM candidato
TLOG-PRO-00116 Numerabilidad y presentación efectiva no se identifican no seleccionado
TLOG-DEF-00120 Emparejamiento numérico con imagen explícita no seleccionado
TLOG-LEM-00062 Inyectividad y decodificación efectiva del par candidato
TLOG-DEF-00121 Codificación de secuencias finitas y tuplas no seleccionado
TLOG-MTH-00083 Decodificación terminante y reconocimiento de secuencias candidato
TLOG-PRO-00117 Operaciones efectivas sobre secuencias codificadas candidato
TLOG-DEF-00122 Tokens numéricos y códigos de expresiones no seleccionado
TLOG-PRO-00118 Reconocimiento e inyectividad de expresiones no seleccionado
TLOG-DEF-00123 Códigos de árboles sintácticos de primer orden candidato
TLOG-LEM-00063 Descenso estricto de los códigos de hijos candidato
TLOG-MTH-00084 Inyectividad y decodificación fiel de términos y fórmulas candidato
TLOG-MTH-00085 Decidibilidad RM de códigos de términos y fórmulas candidato
TLOG-PRO-00119 Conversión efectiva entre cadenas canónicas y árboles no seleccionado
TLOG-COR-00027 Frontera entre sintaxis efectiva, semántica y prueba no seleccionado
TLOG-CNV-00028 Datos fijados y alcance de la verificación no seleccionado
TLOG-LEM-00064 Recorridos y reconstrucción de árboles con pilas codificadas candidato
TLOG-PRO-00120 Cálculo efectivo de variables y nombres candidato
TLOG-PRO-00121 Selección efectiva de la variable fresca canónica no seleccionado
TLOG-MTH-00086 Sustitución numérica efectiva de términos candidato
TLOG-MTH-00087 Decisión numérica de libertad para sustituir candidato
TLOG-MTH-00088 Sustitución literal segura como función efectiva candidato
TLOG-MTH-00089 Renombrado fresco y sustitución canónica sin captura candidato
TLOG-DEF-00124 Certificados explícitos de instancias axiomáticas básicas no seleccionado
TLOG-LEM-00065 Construcción y comprobación de H1–H12 candidato
TLOG-LEM-00066 Comprobación efectiva de Q1–Q5 y sus condiciones laterales candidato
TLOG-LEM-00067 Comprobación de E1–E2 con sustituciones literales candidato
TLOG-DEF-00125 Certificado de axioma con prefijo universal finito no seleccionado
TLOG-PRO-00122 Decisión de axiomas provistos de certificado candidato
TLOG-DEF-00126 Tres clases de líneas certificadas candidato
TLOG-DEF-00127 Código de derivación certificada y conclusión candidato
TLOG-MTH-00090 Decisión total de derivaciones certificadas finitas candidato
TLOG-MTH-00091 Borrado y certificación de derivaciones originales candidato
TLOG-MTH-00092 Semidecidibilidad uniforme de demostrabilidad desde premisas finitas candidato
TLOG-COR-00028 Salida del microtramo y obligaciones restantes no seleccionado
TLOG-CNV-00029 Alcance del cierre y datos efectivos fijados no seleccionado
TLOG-DEF-00128 Códigos de instrucciones con cuatro coordenadas no seleccionado
TLOG-DEF-00129 Códigos de programas y su dominio tipado no seleccionado
TLOG-DEF-00130 Códigos de configuraciones relativas a un programa no seleccionado
TLOG-LEM-00068 Decodificación, inyectividad y guardas de los códigos RM candidato
TLOG-PRO-00123 Inicialización uniforme de registros codificados no seleccionado
TLOG-MTH-00093 Evaluación uniforme y total de un paso codificado candidato
TLOG-MTH-00094 Ejecución acotada uniforme y detección finita de parada candidato
TLOG-DEF-00131 Códigos de trazas y certificados finitos de parada no seleccionado
TLOG-MTH-00095 Reconocimiento total y exactitud de trazas codificadas candidato
TLOG-PRO-00124 La gráfica calculada como proyección de certificados de parada no seleccionado
TLOG-MTH-00096 Ejecutor universal parcial para las descripciones RM aprobadas candidato
TLOG-LEM-00069 Enumeraciones finitas de subárboles y productos de opciones candidato
TLOG-LEM-00070 Recuperación finita de testigos de Q1 y Q2 candidato
TLOG-LEM-00071 Recuperación finita de los parámetros latentes de E2 candidato
TLOG-MTH-00097 Reconocimiento de axiomas lógicos sin certificados candidato
TLOG-DEF-00132 Secuencias originales de derivación codificadas no seleccionado
TLOG-MTH-00098 Decisión y certificación total de derivaciones originales candidato
TLOG-DEF-00133 Presentaciones efectivas de teorías adicionales no seleccionado
TLOG-MTH-00099 Verificación de derivaciones para axiomas adicionales decidibles no seleccionado
TLOG-MTH-00100 Certificados para teorías de axiomas semidecidibles candidato
TLOG-MTH-00101 Decisión efectiva de equivalencia alfa candidato
TLOG-COR-00029 Cierre del capítulo e interfaces hacia aritmetización no seleccionado

Capítulo 19 — Representabilidad en aritmética

ID Unidad Selección Lean
TLOG-CNV-00030 Tres niveles y la nueva teoría aritmética objeto no seleccionado
TLOG-DEF-00134 Signatura aritmética, numerales y abreviaturas no seleccionado
TLOG-AXM-00013 Axiomas de PA e inducción con parámetros no seleccionado
TLOG-LEM-00072 Efectividad de los axiomas y reglas admisibles de PA candidato
TLOG-DEF-00135 La estructura estándar externa de aritmética no seleccionado
TLOG-MTH-00102 Modelo estándar y corrección externa de PA candidato
TLOG-DEF-00136 Definibilidad y representaciones débil y bilateral no seleccionado
TLOG-PRO-00125 Consecuencias lógicas y límites de las representaciones no seleccionado
TLOG-LEM-00073 Aritmética elemental demostrable y segmentos numerales candidato
TLOG-LEM-00074 División con resto demostrable en PA candidato
TLOG-DEF-00137 Fórmulas acotadas y clase existencial Σ1 no seleccionado
TLOG-MTH-00103 Decisión externa y completitud numeral de Δ0 candidato
TLOG-DEF-00138 La relación aritmética auxiliar β no seleccionado
TLOG-LEM-00075 Existencia y unicidad interna de la lectura β candidato
TLOG-LEM-00076 Bézout e inversos residuales en la metateoría externa candidato
TLOG-LEM-00077 Módulos coprimos y construcción explícita del CRT finito candidato
TLOG-MTH-00104 Codificación β de toda secuencia finita externa candidato
TLOG-DEF-00139 Fórmula aritmética de transición de un programa fijo no seleccionado
TLOG-LEM-00078 Exactitud y determinismo demostrable del paso aritmético candidato
TLOG-DEF-00140 Tablas β de ejecución y fórmula de gráfica Σ1 no seleccionado
TLOG-LEM-00079 Exactitud estándar de las tablas de ejecución candidato
TLOG-LEM-00080 Funcionalidad de las gráficas de ejecución dentro de PA candidato
TLOG-MTH-00105 Representación Σ1 de funciones parcialmente computables RM candidato
TLOG-MTH-00106 Representación bilateral de relaciones decidibles RM candidato
TLOG-MTH-00107 Representación débil de relaciones semidecidibles RM candidato
TLOG-MTH-00108 Caracterizaciones de la semidecidibilidad por Σ1 y pruebas candidato
TLOG-MTH-00109 Caracterización bilateral y computabilidad recuperada candidato
TLOG-DEF-00141 Funciones de numeral, sustitución numeral y autoinstanciación no seleccionado
TLOG-MTH-00110 Representación de la infraestructura sintáctica aprobada candidato
TLOG-DEF-00142 Predicados externos de prueba y sus fórmulas aritméticas no seleccionado
TLOG-MTH-00111 Exactitud y representación del predicado de demostrabilidad candidato
TLOG-PRO-00126 Extensiones aritméticas y teorías con axiomas efectivos no seleccionado
TLOG-COR-00030 Cierre de representabilidad y contrato para el lema diagonal no seleccionado

Capítulo 20 — Diagonalización y lema diagonal

ID Unidad Selección Lean
TLOG-CNV-00031 Fundamento y alcance de la autorreferencia no seleccionado
TLOG-DEF-00143 Comillas de Gödel, instanciación y tres igualdades no seleccionado
TLOG-LEM-00081 Higiene efectiva de variables en representantes candidato
TLOG-DEF-00144 Autoinstanciación en una coordenada designada no seleccionado
TLOG-LEM-00082 Representación numeral de la autoinstanciación candidato
TLOG-LEM-00083 Eliminación de un testigo fijado por un numeral candidato
TLOG-DEF-00145 Punto fijo demostrable y parámetro de código no seleccionado
TLOG-MTH-00112 Lema diagonal para sentencias aritméticas candidato
TLOG-PRO-00127 Hipótesis exactas y lectura de la prueba diagonal no seleccionado
TLOG-MTH-00113 Lema diagonal con parámetros preservados candidato
TLOG-COR-00031 Instancias de un punto fijo con parámetros candidato
TLOG-MTH-00114 Compilador externo total de fórmulas fijas candidato
TLOG-MTH-00115 Obtención efectiva de una derivación del bicondicional candidato
TLOG-PRO-00128 Transferencia a extensiones de PA no seleccionado
TLOG-PRO-00129 Satisfacción de los puntos fijos en modelos de PA candidato
TLOG-LEM-00084 La presentación universal del lema diagonal candidato
TLOG-PRO-00130 Cambio demostrablemente equivalente del predicado objetivo candidato
TLOG-DEF-00146 Autoinstanciación de una familia finita codificada no seleccionado
TLOG-LEM-00085 Representación efectiva de los lectores diagonales finitos candidato
TLOG-MTH-00116 Lema diagonal simultáneo con parámetros candidato
TLOG-COR-00032 Referencias mutuas y ausencia de una elección infinita candidato
TLOG-PRO-00131 Objetivos constantes y falta de unicidad literal candidato
TLOG-DEF-00147 Sentencias diagonales para el predicado de demostrabilidad no seleccionado
TLOG-PRO-00132 Qué entregan las instancias de demostrabilidad no seleccionado
TLOG-PRO-00133 Dependencia de la numeración y del representante no seleccionado
TLOG-DEF-00148 Hipótesis de teorías y obligaciones de la Parte V no seleccionado
TLOG-COR-00033 Cierre de diagonalización y de la Parte IV no seleccionado

Capítulo 21 — Primer teorema de incompletitud

ID Unidad Selección Lean
TLOG-CNV-00032 Apertura de la Parte V y alcance del teorema no seleccionado
TLOG-DEF-00149 Presentación efectiva de una extensión aritmética no seleccionado
TLOG-LEM-00086 Verificador total de pruebas certificadas de T candidato
TLOG-DEF-00150 Predicados de prueba positiva, negativa y demostrabilidad no seleccionado
TLOG-MTH-00117 Exactitud numeral y estándar de los predicados de prueba candidato
TLOG-LEM-00087 De un número finito de instancias a una cota numeral candidato
TLOG-DEF-00151 Completitud de una teoría e independencia de una sentencia no seleccionado
TLOG-PRO-00134 Implicaciones entre las hipótesis de corrección candidato
TLOG-DEF-00152 Una sentencia de Gödel para cada presentación no seleccionado
TLOG-MTH-00118 No demostrabilidad y verdad de la sentencia de Gödel candidato
TLOG-MTH-00119 Forma de Gödel bajo ω-consistencia candidato
TLOG-MTH-00120 Forma de Gödel bajo corrección Σ1 candidato
TLOG-COR-00034 Independencia de la sentencia PA ya construida candidato
TLOG-LEM-00088 Clase Π1 y normalización del auxiliar universal candidato
TLOG-MTH-00121 Elección de una sentencia de Gödel literalmente Π1 candidato
TLOG-PRO-00135 Una extensión consistente que demuestra una falsedad Σ1 candidato
TLOG-DEF-00153 La sentencia de Rosser y el orden de certificados no seleccionado
TLOG-LEM-00089 Primera mitad de Rosser: no hay prueba positiva candidato
TLOG-LEM-00090 Segunda mitad de Rosser: una prueba negativa fuerza una positiva candidato
TLOG-MTH-00122 Primer teorema de incompletitud en forma de Gödel–Rosser candidato
TLOG-COR-00035 Aplicación a PA y a sus extensiones efectivas consistentes candidato
TLOG-MTH-00123 Construcción uniforme externa de una sentencia independiente candidato
TLOG-LEM-00091 Añadir uno de los lados de una sentencia independiente candidato
TLOG-PRO-00136 Una reparación finita no elimina la incompletitud candidato
TLOG-MTH-00124 Árbol binario de extensiones y uniones de ramas candidato
TLOG-DEF-00154 La teoría externa de todas las verdades aritméticas no seleccionado
TLOG-COR-00036 La verdad completa no tiene una axiomatización semidecidible no seleccionado
TLOG-PRO-00137 Cuadro de hipótesis y alcance de las conclusiones no seleccionado
TLOG-DEF-00155 Tres obligaciones de derivabilidad para el capítulo siguiente no seleccionado
TLOG-PRO-00138 Lo que el primer teorema no demuestra sobre consistencia interna no seleccionado
TLOG-COR-00037 Cierre del primer teorema y contrato de salida no seleccionado

Capítulo 22 — Segundo teorema de incompletitud

ID Unidad Selección Lean
TLOG-CNV-00033 Base y elección de representante no seleccionado
TLOG-DEF-00156 Funciones primitivas recursivas y sus descripciones no seleccionado
TLOG-LEM-00092 Bézout y coprimalidad dentro de PA candidato
TLOG-LEM-00093 Múltiplos comunes finitos con parámetros variables candidato
TLOG-LEM-00094 Colección finita interna sin elección candidato
TLOG-LEM-00095 Resto chino finito demostrado en PA candidato
TLOG-MTH-00125 Codificación β uniforme de familias finitas definibles candidato
TLOG-LEM-00096 Extensión y recodificación de una tabla β candidato
TLOG-MTH-00126 Representación PR con ecuaciones y totalización PA candidato
TLOG-PRO-00139 Uso conservador de símbolos PR auxiliares no seleccionado
TLOG-LEM-00097 Operaciones sintácticas PR para S y G candidato
TLOG-LEM-00098 Verificador certificado PR y rama PA candidato
TLOG-DEF-00157 Representante seleccionado de pruebas no seleccionado
TLOG-MTH-00127 Exactitud estándar y condición D1 candidato
TLOG-LEM-00099 Ensamblaje de certificados y conservación interna candidato
TLOG-MTH-00128 Condición interna D2 candidato
TLOG-LEM-00100 Pruebas aritméticas numerales generadas uniformemente candidato
TLOG-LEM-00101 Certificación uniforme de verdad y falsedad Δ0 candidato
TLOG-MTH-00129 Completitud Σ1 interna para el representante elegido candidato
TLOG-MTH-00130 Condición interna D3 e identificación de la instancia candidato
TLOG-DEF-00158 Abreviatura de caja y consistencia interna no seleccionado
TLOG-LEM-00102 Cálculo de caja derivado de D1–D3 candidato
TLOG-DEF-00159 Sentencia de Gödel para la nueva caja no seleccionado
TLOG-LEM-00103 Internalización de la contradicción de Gödel candidato
TLOG-MTH-00131 Equivalencia interna entre consistencia y Gödel elegido candidato
TLOG-MTH-00132 Segundo teorema de incompletitud candidato
TLOG-COR-00038 Aplicación a PA y verdad estándar de su consistencia candidato
TLOG-MTH-00133 Teorema de Löb y su forma internalizada candidato
TLOG-COR-00039 Reflexión local y segunda prueba del segundo teorema candidato
TLOG-PRO-00140 Puntos fijos afirmativos para la caja seleccionada no seleccionado
TLOG-PRO-00141 Variantes de la fórmula de consistencia no seleccionado
TLOG-PRO-00142 Dependencia del representante y contraste Rosser no seleccionado
TLOG-MTH-00134 Extensiones por consistencia y por su negación candidato
TLOG-PRO-00143 Lectura condicional en modelos no estándar no seleccionado
TLOG-PRO-00144 Presentaciones y transferencia legítima no seleccionado
TLOG-PRO-00145 Alcance del límite y frontera intertratados no seleccionado
TLOG-COR-00040 Cierre del segundo teorema y contrato final no seleccionado

Capítulo 23 — Indecidibilidad, límites y frontera con GAS

ID Unidad Selección Lean
TLOG-CNV-00034 El cierre lógico y sus tres niveles no seleccionado
TLOG-DEF-00160 Reducción computable entre problemas codificados no seleccionado
TLOG-LEM-00104 Transferencia por reducciones y clausuras candidato
TLOG-DEF-00161 Parada universal y diagonal RM no seleccionado
TLOG-LEM-00105 Semidecisión uniforme de H y K candidato
TLOG-MTH-00135 Indecidibilidad diagonal de la parada candidato
TLOG-COR-00041 Parada universal y no semidecidibilidad de sus complementos candidato
TLOG-MTH-00136 K es completo para semidecidibilidad RM candidato
TLOG-PRO-00146 Parada acotada y ausencia de una cota total uniforme candidato
TLOG-DEF-00162 Teoremas, refutaciones y extensiones aritméticas no seleccionado
TLOG-MTH-00137 Indecidibilidad esencial de PA por diagonalización candidato
TLOG-COR-00042 Teoremas efectivos y complementos no semidecidibles candidato
TLOG-PRO-00147 Completitud deductiva y decisión mediante dos búsquedas no seleccionado
TLOG-LEM-00106 Consistencia de extensiones finitas y deducción candidato
TLOG-MTH-00138 Indecidibilidad de consistencia en extensiones finitas candidato
TLOG-COR-00043 Existencia de modelos para extensiones finitas candidato
TLOG-DEF-00163 Verdad aritmética y fragmento Σ1 no seleccionado
TLOG-MTH-00139 Verdad Σ1 semidecidible y completa candidato
TLOG-MTH-00140 Completitud computacional de los teoremas PA candidato
TLOG-DEF-00164 Fragmento finito de bases aritméticas no seleccionado
TLOG-LEM-00107 Pruebas numerales Δ0 desde las ocho bases candidato
TLOG-MTH-00141 Indecidibilidad de validez y demostrabilidad lógica candidato
TLOG-COR-00044 Satisfacibilidad y no satisfacibilidad de primer orden candidato
TLOG-MTH-00142 No definibilidad aritmética de la verdad completa candidato
TLOG-COR-00045 Verdad completa sin semidecisión de ninguna polaridad candidato
TLOG-PRO-00148 Límite uniforme y afirmaciones sobre una sola instancia no seleccionado
TLOG-DEF-00165 Presentación efectiva de polinomios sobre naturales no seleccionado
TLOG-LEM-00108 Validación y evaluación polinómica total candidato
TLOG-MTH-00143 Semidecidibilidad uniforme de soluciones diofánticas candidato
TLOG-PRO-00149 Traducción polinómica a sentencias existenciales candidato
TLOG-MTH-00144 Cotas computables de testigos y decisión diofántica candidato
TLOG-PRO-00150 Contrato condicional para transferir indecidibilidad a Dio no seleccionado
TLOG-PRO-00151 Dominios diofánticos y cambios de problema no seleccionado
TLOG-DEF-00166 Contrato de salida hacia GAS no seleccionado
TLOG-PRO-00152 Lo que no se exporta por cerrar el tratado no seleccionado
TLOG-PRO-00153 Mapa final de hipótesis y tipos de límite no seleccionado
TLOG-COR-00046 Cierre de la Parte V no seleccionado
TLOG-COR-00047 Cierre matemático del alcance aprobado de TLOG no seleccionado

Reutilización

GFDL-1.3-or-later