Lista de símbolos

La misma notación de la tesis; esta tabla sirve de referencia rápida.

Símbolo	Significado
$\Gamma \vdash \varphi$	Derivabilidad sintáctica: φ se demuestra a partir del contexto Γ.
$\Gamma \vDash \varphi$	Consecuencia semántica: toda valuación que satisface Γ satisface φ.
$\Gamma \vdash_{\mathrm{ND}} \varphi$	Derivabilidad en el cálculo de deducción natural formalizado en Lean.
$\neg,\ \rightarrow$	Negación e implicación (el fragmento {¬, →} usado en la formalización).
$\wedge,\ \vee$	Conjunción y disyunción.
$\bot$	Falso; la contradicción.
$\Gamma$	Contexto: conjunto finito de premisas o hipótesis.
$\varphi,\ \psi,\ \chi$	Fórmulas proposicionales.
$v$	Valuación: asignación de verdad a las variables proposicionales.
$\mathrm{Taut}(\varphi)$	φ es una tautología (verdadera bajo toda valuación).
$\lambda x.\,t$	Abstracción lambda (función que liga la variable x).
$\Lambda \alpha.\,t$	Abstracción de tipo (polimorfismo, sistema λ2).
$\Pi x{:}A.\,B \ \text{ó}\ (x{:}A)\,B$	Producto dependiente; generaliza A → B cuando B depende de x.
$\Sigma x{:}A.\,B$	Suma dependiente (par dependiente).
$*,\ \square$	Sorts del cubo-λ (tipos y kinds).
$\mathrm{Prop},\ \mathrm{Set},\ \mathrm{Type}$	Sorts del CIC: proposiciones, datos y universos de tipos.
$\longrightarrow_{\beta},\ \longrightarrow_{\iota}$	Reducción β (aplicación) y ι (cómputo del recursor).
$\equiv$	Igualdad definicional o equivalencia notacional, según el contexto.
$\vec{x}$	Secuencia finita (notación vectorial) de variables o términos.
$\mathrm{qs}$	La función quicksort.
$\mathrm{Perm}(xs, ys)$	ys es una permutación de xs.
$\mathrm{Sorted}(xs)$	La lista xs está ordenada de forma no decreciente.
$|xs|$	Longitud de la lista xs.
$x :: xs,\ \ xs \mathbin{+\!\!+} ys$	Constructor «cons» y concatenación de listas.