Nivel 7 · Completitud en Lean (experto)

Syntax.lean: fórmulas y semántica

La primera capa del desarrollo fija el lenguaje objeto y su semántica clásica. Todo lo que sigue en el módulo (el cálculo, la corrección, el lema de Kalmár, la completitud) habla de los objetos que se definen en esta página. Se fija un conjunto numerable $\mathsf{Var}$ de variables proposicionales; en la implementación, cadenas de caracteres.

Matemática

Definición 11.2 (Fórmulas)

El conjunto de fórmulas se genera mediante la gramática

\varphi ::= p \;\mid\; \neg\varphi \;\mid\; (\varphi \to \psi), \qquad p \in \mathsf{Var}.

Se usan solo $\neg$ y $\to$ como primitivos; este es el mismo fragmento minimal de Stansifer (2001) y el fragmento $\{\neg,\to\}$ cuya contraparte sintáctica se estableció en el módulo 3. Basta para la lógica proposicional clásica, puesto que los demás conectivos son definibles.

Definición 11.3 (Valuación y evaluación)

Una valuación es una función $v : \mathsf{Var} \to \{\mathsf{V},\mathsf{F}\}$ (en Lean, una función hacia Prop). La evaluación $\llbracket\cdot\rrbracket_v$ se define por recursión sobre la sintaxis:

\llbracket p \rrbracket_v = v(p), \qquad \llbracket \neg\varphi \rrbracket_v = \neg\,\llbracket \varphi \rrbracket_v, \qquad \llbracket \varphi \to \psi \rrbracket_v = \big(\llbracket \varphi \rrbracket_v \to \llbracket \psi \rrbracket_v\big).

Definición 11.4 (Tautología)

$\varphi$ es una tautología , escrito $\mathrm{Taut}(\varphi)$ , si y solo si $\llbracket \varphi \rrbracket_v$ se cumple para toda valuación $v$ .

Nota 11.5 (Sobre la codificación de los valores de verdad como Prop)

Se toma Valuation := String → Prop, de modo que el valor de un átomo es una proposición de Lean en lugar de un booleano. Ambas presentaciones coinciden bajo lógica clásica, que se activa localmente con Classical.propDecidable; las cláusulas recursivas para $\neg$ y $\to$ usan entonces los propios $\neg$ y $\to$ de Lean a nivel meta. Esto mantiene eval definicionalmente transparente para simp. Para el lector que no usa Lean, lo único que importa es la identidad: para toda $v$ y $\varphi$ , eval v φ se cumple si y solo si la valuación de tablas de verdad $\llbracket \varphi \rrbracket_v$ es verdadera. La definición de arriba es la tabla de verdad leída cláusula por cláusula ( $\neg$ es la negación booleana y $\to$ la implicación material), y no una semántica alternativa.

Código de Lean (tal como se implementa)

Extracto de Syntax.lean.

namespace Thesis.Prop

inductive Formula : Type
| atom : String → Formula
| neg  : Formula → Formula
| impl : Formula → Formula → Formula
deriving DecidableEq, Repr

prefix:60 "~" => Formula.neg
infixr:55 " ⟶ " => Formula.impl

abbrev Valuation : Type := String → Prop

def eval (v : Valuation) : Formula → Prop
| .atom s   => v s
| .neg p    => ¬ eval v p
| .impl p q => eval v p → eval v q

def IsTautology (φ : Formula) : Prop :=
  ∀ v : Valuation, eval v φ

end Thesis.Prop

Los tres constructores de Formula son las tres producciones de la gramática de la Definición 11.2; eval es la recursión que define la Definición 11.3; IsTautology es el cuantificador universal sobre valuaciones de la Definición 11.4. Las notaciones ~ y ⟶ (implicación objeto, distinta de la flecha → de los tipos de Lean) permiten escribir las fórmulas objeto de manera legible.

Vista interna (CIC). Formula es un tipo inductivo en $\mathsf{Type}$ : sus habitantes cerrados son exactamente los árboles sintácticos finitos generados por atom, neg e impl, es decir, las fórmulas del nivel objeto como datos. El núcleo genera automáticamente el recursor Formula.rec, que es el principio de inducción estructural sobre fórmulas; las definiciones recursivas eval y (más adelante) atoms se compilan a él, y la «inducción sobre $\varphi$ » de las páginas siguientes es exactamente su aplicación.