Лема. Ако едно множество от затворени дизюнкти е неизпълнимо, то от това множество е резолвентно изводим празният дизюнкт.

    Доказателство. Нека е дадено едно неизпълнимо множество от затворени дизюнкти. По следствието от теоремата за компактност за множества от затворени дизюнкти някое крайно негово подмножество също е неизпълнимо. Неизпълнимостта на това подмножество може да бъде установена по метода на Дейвис и Пътнам, т.е. тръгвайки от въпросното подмножество, след краен брой стъпки от прилагането на метода ще достигнем до множество от дизюнкти, на което принадлежи празният дизюнкт. Понеже всяко от множествата, които се получават в хода на прилагането на метода, се състои от дизюнкти, резолвентно изводими от първоначално даденото множество от дизюнкти, виждаме, че празният дизюнкт е резолвентно изводим от това множество.  _□

Последно изменение: 30.01.2009 г.