Twierdzenie Herbranda

Ten artykuł od 2012-02 wymaga zweryfikowania podanych informacji.
Należy podać wiarygodne źródła, najlepiej w formie przypisów bibliograficznych.
Część lub nawet wszystkie informacje w artykule mogą być nieprawdziwe. Jako pozbawione źródeł mogą zostać zakwestionowane i usunięte.
Po wyeliminowaniu niedoskonałości należy usunąć szablon {{Dopracować}} z tego artykułu.

Twierdzenie Herbranda to jedno z najważniejszych twierdzeń konstruktywnych logiki pierwszego rzędu:

Formuła jest tautologią wtedy i tylko wtedy, gdy tautologią jest pewne rozwinięcie Herbranda tej formuły.

Ponieważ każde rozwinięcie jest właściwie skończoną formułą rachunku zdań, a więc da się rozstrzygnąć w czasie skończonym (wykładniczym), liczba rozwinięć Herbranda dla formuły natomiast jest zbiorem przeliczalnym, umożliwia to udowodnienie każdej tautologii logiki pierwszego rzędu, chociaż może to zająć nieograniczoną ilość czasu.

Algorytm

n = 0;
udowodnione = false;
while (udowodnione == false)
{
    Y = nte_rozwinięcie_Herbranda(X,n);
    Y' = przekształć_na_formułę_rachunku_zdań(Y);
    if (jest_tautologią(Y'))
        udowodnione = true;
    else
        n = n + 1;
}
wygeneruj dowód na podstawie Y;

Zobacz też