Teorema da compacidade

O Teorema da Compacidade assegura que um conjunto qualquer formado por fórmulas bem formadas de um cálculo de predicados de primeira ordem é satisfazível se, e somente se, todo subconjunto finito de também é satisfazível. Ou seja, se , então, qualquer que seja , com , tem-se que ; reciprocamente, se, qualquer que seja , tem-se que , então . Este teorema denota uma importante propriedade para a lógica de predicados, pois garante que toda e qualquer fórmula é derivável (ou logicamente implicada, no caso semântico) a partir de um conjunto finito de premissas. No caso proposicional, a propriedade da compacidade é consequência do Teorema de Tychonoff (que assegura que o produto de espaços compactos também é compacto) aplicado a , e daí segue o nome do teorema.