Twierdzenie Herbranda

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 natomast 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ęce_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ż

• Jacques Herbrand