Propiedades del Cálculo de Construcciones Inductivas (CIC), la lógica
a la que corresponde, la impredicatividad, los axiomas de la lógica y la
correspondencia de Curry-Howard. Al final hay una consulta ajena al
libro (ThrottleStop y alarmas de temperatura en un portátil HP).
Hilo de la conversación
Oriol pregunta por las propiedades de CIC. Claude enumera las
metateóricas (normalización fuerte, confluencia, preservación de tipos,
consistencia, decidibilidad del chequeo de tipos) y las estructurales
(tipos dependientes, Curry-Howard, tipos inductivos, jerarquía de
universos, positividad estricta, lógica constructiva, extracción de
programas). No tiene de serie extensionalidad, irrelevancia de pruebas
ni univalencia.
Con qué lógica se corresponde: lógica intuicionista de orden
superior con definiciones inductivas; ubicación en el cubo lambda de
Barendregt (λC) y fuerza comparable a una ZF intuicionista con universos
inaccesibles.
Qué es “impredicativo”: cuantificar sobre una colección que contiene
la propia proposición (∀ P : Prop, P → P), frente a
Type estratificado. Ventajas, riesgos (Russell, Girard) y
restricción de eliminación; antecedentes en Poincaré y Russell.
Axiomas de la lógica: no hay un conjunto único; se dan los de
Hilbert (proposicional clásica), la variante intuicionista, los de
predicados y la deducción natural.
Varias preguntas dictadas y truncadas (“después de que me cae de
construcciones”, “fondo”, “Curry Howard”) que Claude interpreta:
sucesores de CoC (CIC, pCIC, coinductivos, Lean, HoTT y cúbica), núcleo
del cálculo (todo es término, producto dependiente, impredicatividad) y
Curry-Howard dentro de CoC.
Pregunta final sobre axiomas de esa lógica: casi ninguno, solo
reglas de tipado; los axiomas opcionales son tercero excluido, doble
negación, extensionalidad, irrelevancia de pruebas, univalencia y
elección.
CIC es una lógica intuicionista de orden superior en la que lógica y
computación coinciden (Curry-Howard); sus “axiomas” son reglas de
introducción y eliminación.
La impredicatividad se tolera solo en Prop; en
Type se estratifica para evitar paradojas.
Los axiomas fijan reglas de inferencia, no verdades sobre el
mundo.
Oriol no formula tesis propia; sus preguntas apuntan a la relación
entre lógica, axiomas y fundamentos constructivos.
Autores y referencias
citados
Coquand y Huet (CoC), Barendregt (cubo lambda), Girard (paradoja),
Russell y Poincaré (círculo vicioso, teoría ramificada), Hilbert
(axiomatización), Curry-Howard, Heyting. Sistemas: Coq/Rocq, Lean, HoTT.
Sin obras ni enlaces.
Puntos a verificar
Ninguna afirmación lleva fuente. Las más comprobables: que la
consistencia se siga de la normalización (la consistencia de CIC con
universos no se prueba dentro del propio sistema); la equiparación en
fuerza con “ZF intuicionista con universos inaccesibles” (matizar); y
“decidibilidad del chequeo de tipos”.
La definición False := ∀ P, P y la igualdad de Leibniz
impredicativa son codificaciones de CoC puro, no de CIC (donde son tipos
inductivos); Claude mezcla ambos.
“Sin axiomas el sistema ya es una lógica completa y consistente” es
impreciso: la completitud en el sentido de Gödel no se aplica.
Lean tiene tercero excluido y elección como axiomas disponibles; “de
serie” conviene matizarlo.
Las preguntas dictadas fueron mal transcritas; algunas
interpretaciones de Claude son conjeturas.
Las consultas sobre hardware no tienen relación con el libro.