> U TS skripti u odjeljku "Pokrate i proširenja jezika", zašto u "postoji jedinstven x phi", tj. u onome za što je to pokrata, tražimo da y ne bude slobodna u phi?
Uzmite φ:=(𝒙∈𝒚). Tada biste očito htjeli da ψ:=∃!𝒙φ znači "𝒚 je jednočlan", a jednočlani skupovi postoje, pa to nije univerzalno lažna tvrdnja.
No ako biste to raspisali kao ∃𝒚∀𝒙(𝒙=𝒚↔φ), relativno se lako vidi da to jest univerzalno lažna tvrdnja (dokažite za vježbu). Dakle nije ekvivalentna onom što smo htjeli formalizirati.
To je skroz formalni odgovor, koji Vas možda zadovoljava a možda i ne -- možda mislite da samo treba malo drugačije sintaksno iskazati tu pokratu, i bit će u redu. To nije istina, i vidi se ovako: φ ima dvije slobodne varijable, 𝒙 i 𝒚. Ako vežete 𝒙 kvantifikatorom jedinstvene egzistencije, i dalje varijabla 𝒚 mora ostati slobodna. Dakle formula ψ "ovisi" o 𝒚, u smislu da govori o nekom konkretnom objektu označenom varijablom 𝒚. No ovaj raspis o kojem govorimo veže varijablu 𝒚, pa ne "ovisi" o konkretnom 𝒚.
Postoje samo dva načina kako to možemo razriješiti. Jedan je da ne vežemo nijednu varijablu osim 𝒙 u raspisu, no kako očito moramo govoriti o dvomjesnoj relaciji jednakosti, nije jasno kako to napraviti bez uvođenja nove varijable. To ne mora biti 𝒚, može biti recimo 𝒛 -- ali tada, ako je 𝒛 vezana, imamo isti problem s formulom 𝒙∈𝒛; a ako je slobodna u raspisu, odjednom raspis ovisi o nekom objektu o kojem pokrata uopće ne govori (imamo isti problem s druge strane).
Drugi način je da se pomirimo s tim da će raspis pored 𝒙 vezati još neku varijablu, recimo 𝒚, ali onda moramo zahtijevati da ta varijabla ne smije biti slobodna u φ, jer očito neće biti slobodna u pokrati.
Također, "𝒚 nije slobodna u φ" ne valja gledati kao na ograničenje na φ, već je bolje to gledati kao ograničenje na 𝒚. U smislu, nađemo neku varijablu koja se ne pojavljuje u φ, recimo (BSOMP) da je to 𝒚, i onda shvatimo ψ kao pokratu za formulu s tom varijablom. [To je osnovni razlog zašto zahtijevamo beskonačno mnogo varijabli -- sve što nam zapravo treba je da uvijek postoji "nova" varijabla koju možemo uzeti.]
Dakle, naravno da mi znamo i što znači ∃!𝒙(𝒙∈𝒚) [i naravno da zapravo nisam pazio na to ograničenje kasnije:], samo što stroga formalizacija toga zahtijeva suptilnije alate od ovih koje trenutno imamo.
