Twierdzenie Herbranda
Z Wikipedii, wolnej encyclopedia
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.
Ten artykuł od 2012-02 wymaga zweryfikowania podanych informacji. |
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.