Доказательство в логике первого порядка.

[Yorick]

Я тренируюсь писать доказательства, используя логику первого порядка. И заодно изучаю NBG.
https://www.dropbox.com/s/zcwfvbunhgzs7 ... s.pdf?dl=0
На седьмой странице данного pdf, я доказал утверждение $\vdash (\exists_1 x)(\forall y)(y \notin x)$.
Я хотел бы, чтобы кто-нибудь более опытный посмотрел это доказательство.
а) оно верно?
б) как можно улучшить?

Трудность данного занятия для меня - в том, что чтобы понимать теоремы(о дедукции, о корректности, о полноте) про логические выводы - надо понимать основания математики(NBG), а чтобы понимать как применяются основания математики - надо владеть логикой 1го порядка. Тем не менее что-то получается .

Верны ли следующие утверждения?
1) каждое новое определение - это новый введённый n-местный предикатный символ($n\in \{0,1,2,...\}$) и, опционально, аксиома, использующая данный символ.
2) Определение можно добавлять, если из имеющихся аксиом доказал, что, при ряде предположений, некоторый класс существует и единственный.
3) Есть ли пруверы с такого вида выводом?
4) Формулы с несколькими $\forall$ могут быть просто избавлены от самых внешних кванторов всеобщности. (т.е. правило $\frac{A(X)}{\forall X, A(X)}(Gen)$ - оно в обе стороны работает?)
5)Если да, то понятие общезначимости(или даже истинности?) можно продолжить с замкнутых формул на открытые?
6) Какой припоминаете часто используемый в анализе пример, где явным образом используется логика 2го порядка?
У меня не получится записать такое утверждение, пользуясь основаниями NBG, верно? Тогда какие основания использовать для доказательства такого рода утверждений?

Вопросов много, надеюсь на какие-нибудь получу ответ.:)