Pokażemy teraz, jak przekształcić dowolną bazę wiedzy pierwszego rzędu w bazę wiedzy propozycji. Pierwsza idea polega na tym, że tak jak egzystencjalnie skwantyfikowane zdanie można zastąpić jednym egzemplarzem, tak zdanie powszechnie skwantyfikowane może zostać zastąpione zbiorem wszystkich możliwych egzemplarzy. Załóżmy na przykład, że nasza baza wiedzy zawiera tylko zdania
i że jedynymi obiektami są John i Richard . Stosujemy UI do pierwszego zdania, używając wszystkich możliwych podstawień {x/John} i {x/Richard} . Otrzymujemy
Następnie zastąp podstawowe zdania atomowe, takie jak King(John) , symbolami zdań, takimi jak JohnIsKing. Na koniec zastosuj dowolny z kompletnych algorytmów zdaniowych aby uzyskać wnioski, takie jak JohnIsEvil , co jest równoważne z Evil(John). Tę technikę propozycjonalizacji można uczynić całkowicie ogólną. Pojawia się jednak problem, gdy baza wiedzy zawiera symbol funkcji, zbiór możliwych podstawień terminów podstawowych jest nieskończony! Na przykład, jeśli baza wiedzy wymienia symbol Father, można skonstruować nieskończenie wiele zagnieżdżonych terminów, takich jak Father(Father(Father(John))).
Na szczęście istnieje słynne twierdzenie Jacques’a Herbranda (1930) mówiące, że jeśli zdanie wynika z oryginalnej bazy wiedzy pierwszego rzędu, to istnieje dowód obejmujący tylko skończony podzbiór bazy wiedzy opartej na zdaniach. Ponieważ każdy taki podzbiór ma maksymalną głębokość zagnieżdżenia wśród swoich terminów podstawowych, możemy znaleźć podzbiór, najpierw generując wszystkie instancje ze stałymi symbolami (Richard i John), następnie wszystkie wyrazy o głębokości 1 (Father(Richard) i Father(John) ), a następnie wszystkie wyrazy o głębokości 2, i tak dalej, dopóki nie będziemy w stanie skonstruować dowodu zdaniowego zdania implikowanego. Naszkicowaliśmy podejście do wnioskowania pierwszego rzędu poprzez zdanie, które jest kompletne – to znaczy, że każde zdanie, które pociąga za sobą, może być udowodnione. To duże osiągnięcie, biorąc pod uwagę, że przestrzeń możliwych modeli jest nieskończona. Z drugiej strony nie wiemy, dopóki nie zostanie wykonany dowód, że zdanie jest pociągnięte! Co się dzieje, gdy wyrok nie jest wykonywany? Czy możemy powiedzieć? Cóż, dla logiki pierwszego rzędu okazuje się, że nie możemy. Nasza procedura dowodowa może trwać i trwać, generując coraz głębiej zagnieżdżone terminy, ale nie będziemy wiedzieć, czy utknęła w beznadziejnej pętli, czy też dowód zaraz wyskoczy. Jest to bardzo podobne do problemu zatrzymania maszyn Turinga. Alan Turing (1936) i Alonzo Church (1936) w dość odmienny sposób udowodnili nieuchronność takiego stanu rzeczy. Kwestia wynikania dla logiki pierwszego rzędu jest częściowo rozstrzygalna — to znaczy, istnieją algorytmy, które mówią „tak” każdemu zdaniu pociągniętemu za sobą, ale nie istnieje algorytm, który mówi „nie” każdemu zdaniu niezawikłanemu.