Propiedad algebraica o lógica de una clase de estructuras (finitas) que afirma que toda subestructura parcial finita (o álgebra parcial finita que satisface localmente el diagrama definitorio de la clase) puede ser embebida en alguna estructura plena finita de la clase; informalmente, piezas locales finitas y consistentes se extienden a miembros globales finitos de la clase.

Principio

La idea organizadora es una extensión local-a-global finita: la consistencia parcial finita (ausencia de contradicción local entre un número finito de elementos y relaciones) debe ser realizable dentro de un modelo finito de la clase completa, de modo que las restricciones locales no exijan una completación infinita.

Demostración

Ejemplo: ciertas variedades de álgebras finitas y algunas clases de estructuras relacionales tienen FEP: dada una tabla de multiplicación parcial finita compatible con las leyes de un álgebra booleana, se puede embeber esa tabla parcial en un álgebra booleana finita, mostrando que la estructura parcial se extiende a una estructura plena finita en la clase.

Aplicación incorrecta

Inferir de FEP que la clase entera es finitamente axiomatizable, decidible o cerrada bajo construcciones arbitrarias es un uso indebido; FEP solo trata sobre embebibilidad de estructuras parciales finitas y no garantiza por sí sola propiedades algebraicas o algorítmicas globales.

Consecuencia

Cuando una clase tiene FEP a menudo se puede reducir la verificación de satisfacibilidad finita o de restricciones locales a la búsqueda de modelos finitos, derivar propiedades de modelo finito para teorías universales y obtener resultados de transferencia útiles en decidibilidad y completitud para modelos finitos.

Inversión

El fracaso de FEP significa que existen estructuras parciales finitas compatibles con las relaciones definitorias que no pueden ser embebidas en ninguna estructura plena finita de la clase, por lo que la consistencia local finita no garantiza una completación finita y el razonamiento sobre modelos finitos se ve obstaculizado.

Límite

Se aplica a subestructuras parciales finitas respecto a una firma y clase especificadas; excluye declaraciones sobre estructuras parciales infinitas, embebimientos en modelos infinitos y derivabilidad sintáctica fuera del marco algebraico o relacional especificado.

Tensión semántica

Existe tensión entre FEP y propiedades de compacidad o cierre: FEP es un principio de extensión finitario que puede entrar en conflicto con construcciones infinitarias, y a cambio sacrifica cierre modelo-teórico general por un mayor control de modelos finitos.

Síntesis

FEP formaliza la idea de que piezas locales finitas y consistentes de una estructura pueden realizarse dentro de modelos globales finitos de la clase: es un puente práctico entre especificaciones locales finitas y realizaciones finitas, crucial en teoría algebraica de modelos y en la decidibilidad en modelos finitos.