Ще разглеждаме формули и субституции в сигнатура с поне една константа.

      Теорема на Ербран. Ако едно множество от безкванторни формули не притежава модел, то някое крайно множество от затворени частни случаи на формули от това множество е неизпълнимо.

      Доказателство. Нека е дадено едно множество Γ от безкванторни формули, което не притежава модел. На всяка формула φ от Γ съпоставяме по едно множество Δ_φ от дизюнкти със същите променливи, което я представя. Нека Δ е обединението на така получените множества Δ_φ. То няма модел, защото ако някоя структура би била модел за Δ, тя би била модел и за всяко от множествата Δ_φ и поради това би се оказала модел и за Γ. Щом Δ няма модел, резултатът, установен във въпроса „Свеждане на въпроса за съществуване на модел за множество от дизюнкти към същия въпрос за множество от затворени дизюнкти“, позволява да заключим, че множеството на затворените частни случаи на дизюнктите от Δ е неизпълнимо. Оттук по теоремата за компактност за множества от затворени дизюнкти следва, че и някое крайно множество Δ° от такива затворени частни случаи също е неизпълнимо. За всеки дизюнкт от Δ° избираме по една формула φ от Γ и една субституция σ, такива, че той да се получава чрез прилагане на σ към някой дизюнкт от съответстващото на φ множество Δ_φ, и след като ги изберем, образуваме формулата φσ. Така получените формули φσ съставляват едно крайно множество Γ° от частни случаи на формули от Γ. Ще покажем, че всички формули от множеството Γ° са затворени и това множество е неизпълнимо. Това, че всички формули от Γ° са затворени, е ясно от обстоятелството, че всяка от тях има вида φσ, където φ е някоя безкванторна формула, а σ е субституция, преобразуваща някой дизюнкт със същите променливи както φ в затворен дизюнкт. Да допуснем, че съществува структура S, в която всички формули от Γ° са верни. Ще стигнем до противоречие, като покажем, че и всички дизюнкти от неизпълнимото множество Δ° са верни в S. За тази цел разглеждаме произволен дизюнкт от Δ°. Нека φ и σ са съответните му формула и субституция от построението на множеството Γ°. Тогава разглежданият дизюнкт има вида δσ за някой дизюнкт δ от Δ_φ, а φσ е формула от Γ° и следователно е вярна в структурата S. Да означим с v произволна оценка на променливите в S, а с v′  –  оценката σ^S(v). От верността на φσ в S и равенството (φσ)^S,v = φ^S,v′ следва, че самата формула φ е вярна в S при оценката  v′. Тъй като Δ_φ представя φ, дизюнктът δ също е верен в S при тази оценка, т.е. някой литерал λ от δ е верен в S при нея. Щом обаче литералът λ е верен в S при оценката v′, равенството (λσ)^S,v = λ^S,v′ дава, че литералът λσ е верен в S, и значи разглежданият дизюнкт δσ се оказва верен в S._□

      Забележка 1. Според дефиниция, която дадохме във въпроса „Пренексни формули“, една формула се нарича универсална, ако тя е пренексна формула, в която всички квантори са квантори за общност. Теоремата на Ербран може да се изкаже в следния вид, равносилен на горния:  ако едно множество от затворени универсални формули е неизпълнимо, то някое крайно множество от затворени частни случаи на техни безкванторни части също е неизпълнимо.

      Забележка 2. В литературата се срещат различни версии и варианти на теоремата на Ербран. Например понякога разглежданията отговарят на специалния случай, когато множеството, за което става дума в използваната тук формулировка, е от само една формула.

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