Nivel 7

Completitud en Lean (experto)

La formalización completa del teorema de completitud: cada definición y cada lema, en matemática y en Lean, lado a lado.

Adaptado de: Capítulo: Teorema de la completitud.

Contenido

  1. Panorama y estrategia
  2. Syntax.lean: fórmulas y semántica
  3. NaturalDeduction.lean: el cálculo
  4. Reglas estructurales y derivadas
  5. Corrección y consistencia
  6. El lema de Kalmár constructivo
  7. Descarga y completitud
  8. La auditoría de axiomas