Matematické Fórum

Zdravím,

už delší dobu mám problém s jednou otázkou typu "slepice-vejce":

Při formulování ZF teorie množin se zřejmě předpokládá, že už je zavedená nějaká predikátová logika prvního řádu (kterou se řídí odvozovací pravidla v dokazování, vlastnosti symbolu = apod.). Wikipedia dokonce povídá: "Formally, ZFC is a one-sorted theory in first-order logic."
Speciálně, je zdůrazňováno, že prvky množiny jsou opět jen množiny, že formule nejsou množiny (tedy formule nemohou být ani prvky množiny).
Nicméně prakticky každý materiál, týkající se predikátové logiky (1. řádu), který jsem našel, zavádí pojmy jako "nejmenší množina formulí, obsahující ... ", "zobrazení z množiny formulí do přirozených čísel...", a podobně. Tedy logika prvního řádu se tváří, jako by předpokládala nějakou teorii množin.
Tak jak to teda je? To je několik "vrstev" teorie množin nebo predikátové logiky, že jedno umožňuje zavedení druhého a to potom zavedení opět toho prvního?

Zvlášť by mě zajímalo:

V ZF teorii množin je princip důkazu matematickou indukcí hezky zakotven díky dobrému uspořádání přirozených čísel (které jsou zavedeny jako množiny).
Nicméně v matematické logice se běžně dokazuje "indukcí podle složitosti formule". To by přitom znamenalo, že umím "očíslovat formule" (resp. přiřadit formuli číslo, udávající složitost formule). Nebo jde o nějakou "jinou indukci"?

Předem se omlouvám, jestli takový dotaz působí příliš zmateně, snad je ale jasné, o co mi jde.