Twierdzenie Herbranda

Z Wikipedii, wolnej encyklopedii
Skocz do: nawigacja, szukaj

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), ilość 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[edytuj | edytuj kod]

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ż[edytuj | edytuj kod]