Nivel 7 · Completitud en Lean (experto)

El lema de Kalmár constructivo

Se demuestra que toda tautología es derivable a partir de $\emptyset$ . El argumento clásico de Kalmár (Kalmár, 1935) , esbozado en el Teorema 9.12, procede en dos etapas.

Derivación por valuación (lema de Kalmár). Se fija una valuación $v$ y sea $\Gamma_v$ el contexto de literales de $v$ : para cada átomo $p$ relevante para $\varphi$ , se incluye el literal $p$ si $v(p) = \mathsf{V}$ y $\neg p$ si $v(p) = \mathsf{F}$ . Se demuestra, por inducción sobre $\varphi$ , que $\Gamma_v$ demuestra $\varphi$ cuando $\llbracket \varphi \rrbracket_v$ es verdadera, y demuestra $\neg\varphi$ cuando es falsa. Intuitivamente, la derivación «sigue la fila $v$ de la tabla de verdad».
Descarga de los átomos. Si $\varphi$ es una tautología, todo contexto de literales demuestra $\varphi$ ; los átomos se eliminan entonces uno a uno con el análisis por casos derivado. Esta etapa es el contenido de la página siguiente.

No se necesita maquinaria de conjuntos maximales consistentes / Lindenbaum: el argumento es finitario, guiado por la lista finita de átomos que aparecen en $\varphi$ . El diagrama siguiente recorre las dos etapas, con el nombre de la función de Lean que realiza cada una.

El algoritmo de Kalmár, ejecutable

De la tabla de verdad a la derivación: el contenido constructivo del teorema de completitud.

Etapa 1 · La tabla de verdad `(eval v φ)`

$p$	$p \rightarrow p$	derivación de la fila
T	T
F	T

Etapa 2 · El lema de Kalmár en la fila 1 `(kalmar_lemma)`

El contexto de literales de la fila deriva la fórmula (bilateral: derivaría su negación si la fila la falsara). Cada paso lleva su regla.

p,\, p\, \vdash p

→i

p\, \vdash p \rightarrow p

Etapa 3 · Descarga de los átomos `(discharge / byCases)`

El análisis por casos clásico (byCases, vía RAA) funde las 2 ramas en una derivación sin hipótesis. (Se muestran los últimos niveles; las hojas son las derivaciones de la Etapa 2.)

→i

p\, \vdash p \rightarrow p

→i

\neg p\, \vdash p \rightarrow p

byCases

\vdash p \rightarrow p

✓ Verificador independiente: las 3 derivaciones construidas son instancias correctas de las reglas.

Átomos, literales y contextos de literales

Definición 11.15 (Átomos de una fórmula)

$\mathrm{atoms}(\varphi)$ es la lista de átomos que aparecen en $\varphi$ (con repetición):

\mathrm{atoms}(p) = [p], \quad \mathrm{atoms}(\neg\varphi) = \mathrm{atoms}(\varphi), \quad \mathrm{atoms}(\varphi \to \psi) = \mathrm{atoms}(\varphi) \mathbin{+\!\!+} \mathrm{atoms}(\psi).

Definición 11.16 (Literal y contexto de literales)

Para una valuación $v$ y un átomo $p$ ,

\mathrm{lit}_v(p) = \begin{cases} p & \text{si } v(p) = \mathsf{V},\\ \neg p & \text{si } v(p) = \mathsf{F}. \end{cases}

Para una lista de átomos $\mathit{ats}$ , el contexto de literales es

\Gamma_v(\mathit{ats}) = \{\, \mathrm{lit}_v(p) : p \in \mathit{ats} \,\},

definido por recursión: $\Gamma_v([\,]) = \emptyset$ y $\Gamma_v(p :: \mathit{rest}) = \{\mathrm{lit}_v(p)\} \cup \Gamma_v(\mathit{rest})$ .

Lema 11.17 (Pertenencia del literal)

Si $p \in \mathit{ats}$ entonces $\mathrm{lit}_v(p) \in \Gamma_v(\mathit{ats})$ .

Demostración.

A probar: $\mathrm{lit}_v(p) \in \Gamma_v(\mathit{ats})$ , bajo la hipótesis $p \in \mathit{ats}$ . Por inducción sobre la lista $\mathit{ats}$ .

$\mathit{ats} = [\,]$ . La hipótesis $p \in [\,]$ es imposible, así que el caso es vacuo.
$\mathit{ats} = a :: \mathit{rest}$ . Por definición, $\Gamma_v(a :: \mathit{rest}) = \{\mathrm{lit}_v(a)\} \cup \Gamma_v(\mathit{rest})$ . De $p \in a :: \mathit{rest}$ hay dos posibilidades: si $p = a$ , entonces $\mathrm{lit}_v(p) = \mathrm{lit}_v(a)$ es el elemento insertado; si $p \in \mathit{rest}$ , la hipótesis de inducción da $\mathrm{lit}_v(p) \in \Gamma_v(\mathit{rest})$ , y como $\Gamma_v(\mathit{rest}) \subseteq \Gamma_v(a :: \mathit{rest})$ , se concluye.

Extracto de Completeness.lean.

def atoms : Formula → List String
| .atom s   => [s]
| .neg p    => atoms p
| .impl p q => atoms p ++ atoms q

noncomputable def lit (v : Valuation) (p : String) : Formula :=
  if v p then .atom p else ~(.atom p)

noncomputable def litCtx (v : Valuation) : List String → Set Formula
| []        => ∅
| p :: rest => insert (lit v p) (litCtx v rest)

theorem lit_mem {v : Valuation} {p : String} {ats : List String}
    (h : p ∈ ats) : lit v p ∈ litCtx v ats := by
  induction ats with
  | nil => simp at h
  | cons a rest ih =>
      rcases List.mem_cons.1 h with rfl | h
      · exact Set.mem_insert _ _
      · exact Set.mem_insert_of_mem _ (ih h)

(lit y litCtx son noncomputable porque el test « $v\,p$ » es una proposición; bajo la instancia local Classical.propDecidable el if está bien definido.)

El lema de Kalmár

Lema 11.18 (Kalmár)

Fíjense una valuación $v$ y una lista $\mathit{ats}$ con $\mathrm{atoms}(\varphi) \subseteq \mathit{ats}$ . Entonces

\big(\llbracket \varphi \rrbracket_v \Rightarrow \Gamma_v(\mathit{ats}) \Provnd \varphi\big) \quad\text{y}\quad \big(\neg\llbracket \varphi \rrbracket_v \Rightarrow \Gamma_v(\mathit{ats}) \Provnd \neg\varphi\big).

Demostración.

A probar: para $\Gamma := \Gamma_v(\mathit{ats})$ , las dos implicaciones

\text{(P)}\quad \llbracket \varphi \rrbracket_v \Rightarrow \Gamma \Provnd \varphi, \qquad \text{(N)}\quad \neg\llbracket \varphi \rrbracket_v \Rightarrow \Gamma \Provnd \neg\varphi.

Por inducción sobre la estructura de $\varphi$ .

Caso átomo $\varphi = s$ . Como $\mathrm{atoms}(s) = [s] \subseteq \mathit{ats}$ , se tiene $s \in \mathit{ats}$ , y por el Lema 11.17, $\mathrm{lit}_v(s) \in \Gamma$ .

(P) Si $\llbracket s \rrbracket_v$ (esto es, $v(s) = \mathsf{V}$ ): entonces $\mathrm{lit}_v(s) = s$ , luego $s \in \Gamma$ y $\frac{s \in \Gamma}{\Gamma \Provnd s}\ \text{(hip.).}$
(N) Si $\neg\llbracket s \rrbracket_v$ : entonces $\mathrm{lit}_v(s) = \neg s$ , luego $\neg s \in \Gamma$ y $\frac{\neg s \in \Gamma}{\Gamma \Provnd \neg s}\ \text{(hip.).}$

Caso negación $\varphi = \neg p$ . Como $\mathrm{atoms}(\neg p) = \mathrm{atoms}(p) \subseteq \mathit{ats}$ , valen las dos hipótesis de inducción para $p$ : (P $_p$ ) y (N $_p$ ).

(P) Si $\llbracket \neg p \rrbracket_v$ , es decir $\neg\llbracket p \rrbracket_v$ : por (N $_p$ ) se obtiene directamente la meta $\Gamma \Provnd \neg p$ .
(N) Si $\neg\llbracket \neg p \rrbracket_v$ , es decir $\neg\neg\llbracket p \rrbracket_v$ : clásicamente $\llbracket p \rrbracket_v$ , así que (P $_p$ ) da $\Gamma \Provnd p$ , y la introducción de doble negación (Lema 11.9) da la meta: $\frac{\Gamma \Provnd p}{\Gamma \Provnd \neg\neg p}\ (\text{dni}).$

Caso implicación $\varphi = p \to q$ . Como $\mathrm{atoms}(p \to q) = \mathrm{atoms}(p) \mathbin{+\!\!+} \mathrm{atoms}(q) \subseteq \mathit{ats}$ , valen las hipótesis de inducción para $p$ y para $q$ .

(P) $\llbracket p \to q \rrbracket_v \Rightarrow \Gamma \Provnd p \to q$ . Se distingue según $\llbracket p \rrbracket_v$ .

Si $\llbracket p \rrbracket_v$ : de $\llbracket p \to q \rrbracket_v = (\llbracket p \rrbracket_v \to \llbracket q \rrbracket_v)$ se sigue $\llbracket q \rrbracket_v$ ; por (P $_q$ ), $\Gamma \Provnd q$ . Entonces:

\Gamma \vdash_{\mathrm{ND}} q

debil.

\Gamma, p \vdash_{\mathrm{ND}} q

→I

\Gamma \vdash_{\mathrm{ND}} p \to q

Si $\neg\llbracket p \rrbracket_v$ : por (N $_p$ ), $\Gamma \Provnd \neg p$ . Se deriva $\Gamma, p \Provnd q$ y se cierra con $\to$ I:

\Gamma \vdash_{\mathrm{ND}} \neg p

debil.

\Gamma, p \vdash_{\mathrm{ND}} \neg p

p \in \Gamma, p

hip.

\Gamma, p \vdash_{\mathrm{ND}} p

¬E

\Gamma, p \vdash_{\mathrm{ND}} \bot

⊥E

\Gamma, p \vdash_{\mathrm{ND}} q

→I

\Gamma \vdash_{\mathrm{ND}} p \to q

(N) $\neg\llbracket p \to q \rrbracket_v \Rightarrow \Gamma \Provnd \neg(p \to q)$ . De $\neg(\llbracket p \rrbracket_v \to \llbracket q \rrbracket_v)$ se obtiene clásicamente $\llbracket p \rrbracket_v$ (si no, la implicación sería vacuamente verdadera) y $\neg\llbracket q \rrbracket_v$ (si no, también lo sería). Por (P $_p$ ), $\Gamma \Provnd p$ ; por (N $_q$ ), $\Gamma \Provnd \neg q$ . Se cierra con $\neg$ I, descargando el supuesto $p \to q$ :

\Gamma \vdash_{\mathrm{ND}} \neg q

debil.

\Gamma, (p \to q) \vdash_{\mathrm{ND}} \neg q

(p \to q) \in \Gamma, (p \to q)

hip.

\Gamma, (p \to q) \vdash_{\mathrm{ND}} p \to q

\Gamma \vdash_{\mathrm{ND}} p

debil.

\Gamma, (p \to q) \vdash_{\mathrm{ND}} p

→E

\Gamma, (p \to q) \vdash_{\mathrm{ND}} q

¬E

\Gamma, (p \to q) \vdash_{\mathrm{ND}} \bot

¬I

\Gamma \vdash_{\mathrm{ND}} \neg(p \to q)

Código de Lean (tal como se implementa)

Extracto de Completeness.lean.

theorem kalmar (v : Valuation) (ats : List String) :
    ∀ φ : Formula, atoms φ ⊆ ats →
      (eval v φ → ND (litCtx v ats) φ) ∧ (¬ eval v φ → ND (litCtx v ats) (~φ)) := by
  intro φ
  induction φ with
  | atom s =>
      intro hsub
      have hs : s ∈ ats := hsub (by simp [atoms])
      refine ⟨?_, ?_⟩
      · intro hev
        have hvs : v s := hev
        have hmem := lit_mem (v := v) hs
        rw [lit, if_pos hvs] at hmem
        exact ND.hyp hmem
      · intro hev
        have hvs : ¬ v s := hev
        have hmem := lit_mem (v := v) hs
        rw [lit, if_neg hvs] at hmem
        exact ND.hyp hmem
  | neg p ih =>
      intro hsub
      have hsub' : atoms p ⊆ ats := hsub
      obtain ⟨ihpos, ihneg⟩ := ih hsub'
      refine ⟨?_, ?_⟩
      · intro hev; exact ihneg hev
      · intro hev; exact dni (ihpos (not_not.1 hev))
  | impl p q ihp ihq =>
      intro hsub
      have hsp : atoms p ⊆ ats := by
        intro a ha; exact hsub (by simp only [atoms, List.mem_append]; exact Or.inl ha)
      have hsq : atoms q ⊆ ats := by
        intro a ha; exact hsub (by simp only [atoms, List.mem_append]; exact Or.inr ha)
      obtain ⟨ihp_pos, ihp_neg⟩ := ihp hsp
      obtain ⟨ihq_pos, ihq_neg⟩ := ihq hsq
      refine ⟨?_, ?_⟩
      · intro hev
        by_cases hp : eval v p
        · exact ND.impI (weakening (ihq_pos (hev hp)) (Set.subset_insert _ _))
        · apply ND.impI
          have h1 : ND (insert p (litCtx v ats)) (~p) :=
            weakening (ihp_neg hp) (Set.subset_insert _ _)
          have h2 : ND (insert p (litCtx v ats)) p := ND.hyp (Set.mem_insert _ _)
          exact ND.botE (ND.negE h1 h2)
      · intro hev
        have hp : eval v p := by by_contra h; exact hev (fun hpp => absurd hpp h)
        have hq : ¬ eval v q := fun hq => hev (fun _ => hq)
        apply ND.negI
        have hpq : ND (insert (p ⟶ q) (litCtx v ats)) (p ⟶ q) := ND.hyp (Set.mem_insert _ _)
        have hpp : ND (insert (p ⟶ q) (litCtx v ats)) p :=
          weakening (ihp_pos hp) (Set.subset_insert _ _)
        have hnq : ND (insert (p ⟶ q) (litCtx v ats)) (~q) :=
          weakening (ihq_neg hq) (Set.subset_insert _ _)
        exact ND.negE hnq (ND.impE hpq hpp)

El código sigue, rama por rama, la demostración anterior: las tres ramas de induction φ (atom, neg, impl) son los tres casos ya probados, y cada paso matemático reaparece como una línea de Lean.

Nota (Traducción de tácticas a contenido lógico)

Para el lector que no lee Lean, vale la pena traducir los nombres de las tácticas a su contenido lógico: not_not.1 es la eliminación de la doble negación ( $\neg\neg A \to A$ ), clásicamente válida, que interviene en el caso de la negación; by_cases hp : eval v p es el análisis por casos según se cumpla o no $\llbracket p \rrbracket_v$ , en el caso positivo de la implicación; y las dos líneas by_contra/absurd extraen $\llbracket p \rrbracket_v$ y $\neg\llbracket q \rrbracket_v$ a partir de $\neg(\llbracket p \rrbracket_v \to \llbracket q \rrbracket_v)$ , apoyándose en la equivalencia clásica $\neg(P \to Q) \Leftrightarrow P \wedge \neg Q$ .

Vista interna (CIC). Aquí induction φ es Formula.rec (no ND.rec): se recurre sobre la sintaxis, con motivo

C\,\varphi \;:=\; \texttt{atoms}\ \varphi \subseteq \mathit{ats} \to \big(\texttt{eval}\ v\ \varphi \to \texttt{ND}\ \Gamma\ \varphi\big) \wedge \big(\neg\,\texttt{eval}\ v\ \varphi \to \texttt{ND}\ \Gamma\ (\neg\varphi)\big).

En las ramas neg e impl el recursor proporciona las hipótesis de inducción ih, ihp, ihq para las subfórmulas inmediatas; la demostración consume esas hipótesis (a nivel meta) y produce términos ND con constructores (ND.impI, ND.negI, ND.botE, ND.negE, …) y la regla derivada dni. Así, una sola ejecución de Formula.rec convierte el valor de verdad de $\varphi$ bajo $v$ en un árbol de derivación efectivo: este es el contenido de «completitud como programa» del Lema 11.18 hecho literal.

El lema de Kalmár constructivo

Etapa 1 · La tabla de verdad (eval v φ)

Etapa 2 · El lema de Kalmár en la fila 1 (kalmar_lemma)

Etapa 3 · Descarga de los átomos (discharge / byCases)

Átomos, literales y contextos de literales

El lema de Kalmár

Código de Lean (tal como se implementa)

Etapa 1 · La tabla de verdad `(eval v φ)`

Etapa 2 · El lema de Kalmár en la fila 1 `(kalmar_lemma)`

Etapa 3 · Descarga de los átomos `(discharge / byCases)`