Bibliografía y procedencia

Fecha de última modificación

11 de octubre de 2026

Índice del tratado

Texto propio y reconstrucción deductiva. Una cita identifica procedencia; no sustituye una prueba ni acredita lectura integral.

ID Fuente Función Alcance
TLOG-SRC-0001 Kurt Gödel, “Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I” (1931) primary; incompletitud y aritmetización histórica SEED — requiere colación TLOG
TLOG-SRC-0002 Herbert B. Enderton, A Mathematical Introduction to Logic, 2nd ed. (2001) architecture; proof-model; sintaxis BIB-VERIFIED / TEXT-COLLATED / USED-IN-NODE — Introducción xi–xii; §1.0 pp. 11–13; §1.1 pp. 13–19; §1.2 pp. 20–28; §1.3 pp. 29–34; §1.4 pp. 34–44; cap. 2 §2.4 pp. 109–114; §2.5 pp. 131–135; §1.7 pp. 59–61; cap. 2 §§2.1–2.2 pp. 67–85, 94–97
TLOG-SRC-0003 Wolfgang Rautenberg, A Concise Introduction to Mathematical Logic, 3rd ed. (2010) countercheck; objeto/metanivel; sintaxis proposicional BIB-VERIFIED / TEXT-COLLATED / USED-IN-NODE — Introducción pp. xv–xvi; cap. 1 §1.1 pp. 4–9; §1.2 pp. 11–12; §1.3 pp. 17–21; §1.4 pp. 26–30; §1.6 pp. 35–40; cap. 2 §§2.1–2.2 pp. 43–52, 54–61; cap. 2 §2.3 pp. 62–63, 70–72
TLOG-SRC-0004 Yuri I. Manin, A Course in Mathematical Logic for Mathematicians architecture; contrast SEED / LOCATED-IN-DRIVE
TLOG-SRC-0005 Boolos–Burgess–Jeffrey, Computability and Logic computability-control; incompletitud SEED / LOCATED-IN-DRIVE
TLOG-SRC-0006 Peter Smith, An Introduction to Gödel’s Theorems, 2nd ed. proof-model; representabilidad y diagonalización SEED / LOCATED-IN-DRIVE
TLOG-SRC-0007 Dirk W. Hoffmann, Gödel’s Incompleteness Theorems: A Guided Tour Through Kurt Gödel’s Historic Proof historical; countercheck SEED / LOCATED-IN-DRIVE
TLOG-SRC-0008 Nicolas Bourbaki, Theory of Sets set-theory-control; notación/arquitectura fundacional SEED / LOCATED-IN-DRIVE
TLOG-SRC-00013 Jeremy Avigad, Computability and Incompleteness, lecture notes, versión9enero2007, sitio del autor/CMU portada y §4.6, pp. impresas110–112 (páginas digitales113–115); formulación de Rosser y separación de ω-consistencia/consistencia ONLINE-TEXT-CHECKED / LIMITED-EXCERPT; no colación integral
TLOG-SRC-00014 Barkley Rosser, Extensions of Some Theorems of Gödel and Church, JSL1(3), septiembre1936,87–91; DOI10.2307/2269028 extracto público y metadata de Cambridge; no texto completo BIB-VERIFIED / ONLINE-EXTRACT-CHECKED

Controles adicionales

  • TLOG-SRC-0009 — Thomas J. Jech, The Axiom of Choice (1973), cap. 2, §2.3 («The Prime Ideal Theorem»). Rol set-theory-control / contrast; estado BIB-VERIFIED / SECTION-LOCATED / NOT-TEXT-COLLATED. Se consultó metadato editorial y corroboración de fuentes institucionales/Stanford sobre la equivalencia ZF/BPI; no se afirma lectura integral del capítulo. Referencias de acceso: https://plato.stanford.edu/entries/axiom-choice/ y https://www.sciencedirect.com/science/article/pii/S0049237X08717531

  • TLOG-SRC-00010 — Christian Espíndola, «Semantic Completeness of First-Order Theories in Constructive Reverse Mathematics», Notre Dame Journal of Formal Logic 57 (2016), n.º 2, pp. 281–286, DOI 10.1215/00294527-3470433. Rol formalization-control / contrast; estado BIB-VERIFIED / ABSTRACT-CHECKED / NOT-TEXT-COLLATED. Control bibliográfico en https://philpapers.org/rec/ESPSCO y https://su.diva-portal.org/smash/person.jsf?pid=authority-person%3A88088

Nueva identidad: TLOG-SRC-00011 — Stanford Encyclopedia of Philosophy, suplemento «Zermelo–Fraenkel Set Theory (ZF)» de la entrada Set Theory. URL: https://plato.stanford.edu/entries/set-theory/zf.html ; consulta: 2026-10-10. Rol: set-theory-control / countercheck; estado BIB-VERIFIED / ONLINE-CLAUSE-CHECKED / NOT BOOK-TEXT-COLLATED.

Nueva identidad TLOG-SRC-00012: Shogo Saito; adaptación Mathlib por Hunter Monroe, Mathlib.Logic.Godel.GodelBetaFunction, archivo fuente (copyright2023), repositorio oficial leanprover-community/mathlib4, revisión 6be3d352cec3ceabd28bf85266d28646e02f1975. Estado ONLINE-CODE-CHECKED, alcance limitado: documentación del lector de restos, elección factorial de módulos coprimos y enunciado beta_unbeta_coe. Rol: contraste primario de la ruta β, no prueba importada ni compilación Lean de TLOG. Fuente estable. La fórmula de módulo coincide en su forma; nuestra elección b=L!*(1+max valores) y prueba mediante Bézout se dan autónomamente. La fuente no acredita representación dentro de PA.

Se incorpora una identidad nueva TLOG-SRC-00015: YuriMatiyasevich,Hilbert’s Tenth Problem, §1.1enla página del autor/PDMI. Alcance:únicamente el fragmentopúblico§1.1,declaración dedominio, dosladospolinómicos ydirección de reducciones. EstadoAUTHOR-PAGE/ONLINE-EXCERPT-CHECKED; no libro completo cotejado, no demostraciónMRDPconsultada/incorporada. El sitio no fija una versión de ese fragmento; no se atribuye una fecha editorial nueva. Fuente nueva enTLOG, no IDheredado deGAS.

Sólo Enderton y Rautenberg tienen estado TEXT-COLLATED para los alcances expresamente indicados. Los demás controles conservan sus estados limitados.

Reutilización

GFDL-1.3-or-later