Definizione Induttiva di un certo insieme S

• Base: ad S appartengono certi elementi b1, b2, ... , bk
• Passo 1: Se e1, e2, ..., en appartengono a S, allora anche l'elemento p(e1, e2,..., en) costruito a partire da e1,...,en appartiene a S.
• Passo 2: Se e1, ... ,em appartengono a S, allora anche l'elemento q(e1, e2, ..., em) costruito a partire da e1,...,em appartiene a S
• ....
• Altri passi (ci possono essere più passi, guardare la definizione induttiva di fbf per esempio)

Formule ben formate (fbf)

• ....
• Chiusura: Nient'altro appartiene a S

Principio di induzione su S associato alla definizione induttiva

Per ogni proprietà che riusciamo ad esprimere come fbf H(x) (una sola variabile libera), se valgono

• Base: H(b1), H(b2),..., H(bk)
• Passo 1: ∀x1∀x2...∀xn ((H(x1)∧H(x2)∧...∧H(xn))→H(p(x1, x2, ..., xn)))
• Passo 2: ∀x1∀x2...∀xm((H(x1)∧...∧H(xm))→ H(q(x1, x2,..., xm)))
• ...
• Altri passi
• ...
• Passo: ∀x1∀x2...∀xj ((H(x1)∧H(x2)∧...∧H(xj))→ H(r(x1,...,xj)))

Allora vale: ∀x H(x)