Ще докажем следното твърдение.
Теорема за представимост в пренексен вид. Всяка формула е еквивалентна на някоя формула в пренексен вид, имаща същите свободни променливи като дадената.
Доказателство. За нуждите на това доказателство ще съпоставим на всяка формула неотрицателно цяло число, което ще наричаме нейно тегло. Ще направим това с помощта на следната индуктивна дефиниция:
а) атомарните формули имат тегло 0;
б) теглото на отрицанието на една формула е равно на удвоеното тегло на самата формула;
в) теглото на конюнкцията и на дизюнкцията на две формули е равно на удвоения сбор от техните тегла;
г) за всяка формула θ и всяка променлива ξ теглото на формулата ∀ξθ и на формулата ∃ξθ е с 1 по-голямо от теглото на θ.
Сега ще отбележим някои следствия от горната дефиниция. Ако θ е формула с тегло t, а ∂ξ и ∂°ξ са двата квантора относно дадена променлива ξ, то формулите ¬∂ξθ и ∂°ξ¬θ имат тегла съответно 2(t+1) и 2t+1, следователно втората от тях има по-малко тегло от първата. Чрез индукция, съответна на дефиницията за формула, се доказва, че при заместване на променлива с терм в дадена формула получената формула има същото тегло като дадената. Като използваме това, виждаме, че ако са дадени две формули θ и φ с тегла съответно t и u, ∂ξ е квантор за общност или за съществуване относно дадена променлива ξ, ∂η е същият вид квантор относно някоя променлива η, за която θ[ξ/η] е дефинирано, а • е знак за конюнкция или знак за дизюнкция, то формулите ∂ξθ•φ и ∂η(θ[ξ/η]•φ) имат тегла съответно 2(t+1+u) и 2(t+u)+1, следователно втората от тях има по-малко тегло от първата. Аналогично е положението и с двойката формули φ•∂ξθ и ∂η(φ•θ[ξ/η]).
Очевидно теоремата ще бъде доказана, ако покажем, че всяка формула, която не е в пренексен вид, е еквивалентна на някоя формула с по-малко тегло, имаща същите свободни променливи. Ще постигнем това, като докажем, пак чрез индукция, съответна на дефиницията за формула, че всяка формула притежава свойството да е в пренексен вид или да е еквивалентна на формула с по-малко тегло, имаща същите свободни променливи. За атомарните формули свойството е налице, защото те са безкванторни и значи са в пренексен вид. Преминаваме към разглеждане на различните възможни случаи при индуктивната стъпка.
Нека свойството е налице за дадена формула φ (т.е. φ е в пренексен вид или е еквивалентна на формула с по-малко тегло, имаща същите свободни променлививи). Ще покажем, че и формулата ¬φ има това свойство. Ако формулата φ е в пренексен вид, то тя е безкванторна или има вида ∂ξθ за някоя променлива ξ и някоя формула θ, където ∂ξ е квантор за общност или квантор за съществуване относно ξ. Ако φ е безкванторна, то ¬φ също е безкванторна и следователно е в пренексен вид. Ако пък φ=∂ξθ, то формулата ¬φ е еквивалентна на формулата ∂°ξ¬θ, където ∂°ξ е другият квантор относно ξ. Лесно се проверява обаче, че тези две формули са с едни и същи свободни променливи, а от друга страна втората има по-малко тегло от първата. Най-сетне, ако φ е еквивалентна на някоя формула ψ с по-малко тегло и със същите свободни променливи, то ¬φ ще бъде еквивалентна на ¬ψ, като връзките между теглата на тези две еквивалентни формули и между множествата на техните свободни променливи пак ще бъдат такива, каквито трябва.
Нека разглежданото свойство е налице за дадена формула φ1 и за дадена формула φ2 (т.е. всяка от тези две формули е в пренексен вид или е еквивалентна на формула с по-малко тегло, имаща същите свободни променливи). Ще покажем, че свойството е налице и за формулата φ1•φ2, където • е знакът за конюнкция или знакът за дизюнкция. Ако формулата φ1 е еквивалентна на някоя формула ψ с по-малко тегло и със същите свободни променливи, то формулата φ1•φ2 е еквивалентна на формулата ψ•φ2, а тя е с по-малко тегло и е със същите свободни променливи. Аналогично се разглежда и случаят, когато φ2 е еквивалентна на формула с по-малко тегло и със същите свободни променливи. Да предположим сега, че всяка от формулите φ1 и φ2 е в пренексен вид. Тогава всяка от тях е безкванторна или има вида ∂ξθ за някоя променлива ξ и някоя формула θ, където ∂ξ е квантор за общност или квантор за съществуване относно ξ. Ако и двете формули φ1 и φ2 са безкванторни, то и формулата φ1•φ2 също е безкванторна и значи е в пренексен вид. Ако φ1 има вида ∂ξθ, то при подходящо избрана променлива η формулата φ1•φ2 е еквивалентна на формула ∂η(θ[ξ/η]•φ2) със същите свободни променлива, но с по-малко тегло. Аналогично се разглежда и случаят, когато φ2 има вида ∂ξθ.
За да завършим доказателството, остава да проверим, че разглежданото свойство се запазва и при поставяне на квантор пред формула с това свойство. Нека φ е формула с въпросното свойство, а ∂ξ е квантор за общност или квантор за съществуване относно дадена променлива ξ. Ще покажен, че и формулата ∂ξφ притежава същото свойство. Ако φ е в пренексен вид, то формулата ∂ξφ също е в пренексен вид, когато ξ е свободна променлива на φ, а в случай, че ξ не е свободна променлива на φ, формулите ∂ξφ и φ са еквивалентни и имат едни и същи свободни променливи, като втората е с по-малко тегло от първата. Ако пък φ е еквивалентна на някоя формула ψ с по-малко тегло и със същите свободни променливи, то ∂ξφ е еквивалентна на ∂ξψ, като тези две формули са с едни и същи свободни променливи, но втората е с по-малко тегло от първата. □
Забележка 1. Горното доказателство фактически дава начин, позволяващ всяка формула, която не е в пренексен вид, да бъде заменена с някоя еквивалентна на нея формула със същите свободни променливи, но с по-малко тегло, като в общия случай начинът може да предлага няколко такива възможности за замяна. Правейки последователно подходящ брой пъти такива замени, можем за коя да е формула действително да намерим еквивалентна на нея формула в пренексен вид, която има същите свободни променливи. Видът на тази формула може обаче да зависи от нашите избори на възможност при отделните стъпки, които правим. Например за формулата ∀x p(x)& ∃y q(y) имаме възможност при първата стъпка да я заменим било със ∀x(p(x)& ∃y q(y)), било със ∃y(∀x p(x)& q(y)). Който и от двата избора да направим, след втората стъпка ще получим формула в пренексен вид, но в единия случай тя ще бъде ∀x∃y(p(x)& q(y)), а в другия ще бъде ∃y∀x(p(x)& q(y)).
Забележка 2. Ние доказахме теоремата за представимост в пренексен вид без да използваме възможността за едновременно изнасяне на квантор за общност от двата члена на конюнкция и за едновременно изнасяне на квантор за съществуване от двата члена на дизюнкция. Методът, за който става дума в предходната забележка, може да бъде усъвършенстван така, че да допуска използване и на тези две възможности. Понякога това усъвършенстване позволява да получим като краен резултат по-проста формула. Например чрез прилагане на метода в първоначалния му вид можем от формулата