Dubbio su formula ben formata nella logica predicativa

Ciao, sto affrontando questo argomento che ahimè non mi è del tutto chiaro.
Partendo dalla teoria sulle formule ben formate nella logica predicativa, sappiamo che si considerano formule:

1- un termine A(t1,...,tn) (il predicato (A) applicato a termini t1,....,tn) è una formula
2- se F è una formula e x una variabile individuale, allora ∃x.F e ∀x.F sono formule
3- se F è una formula, allora lo sono anche ¬F, (F)
4- se P e A sono formule, lo sono anche P˄A, P˅A, P→A
5- niente altro è una formula (clausola di chiusura)

Ok, detto questo prendendo tre esempi:

A) ∃t.P(t) → ¬A(t)

Questa qui direi che rispetta tutti i punti. P(t) è una formula per la regola 1, quindi questo rende valido anche ∃t.P(t) per la regola 2. ¬A(t) è una formula sempre per il punto 1. Quindi tutta la formula nel suo complesso è ben formata per la regola al punto 4.

B) ∀t.P(t) ^ A(z)

Anche questa mi pare sia ben formata. P(t) è una formula per il punto 1, quindi anche ∀t.P(t) è una formula per il punto 2. A(z) è una formula per il punto 1, quindi tutta la formula nel suo complesso è ben formata per il punto 4.

C) ∀t.(P(t) → ∃z.¬A(t, z))

Per questa ho forti dubbi, qualcuno potrebbe aiutarmi a capire se è ben formata o meno e soprattutto che ragionamento ha seguito?

Grazie

Ti stai perdendo in bicchier d'acqua mi sa...
\(A(t,z)\) è una formula, quindi (punto 3) pure \(\neg A(t,z)\) lo è; (punto 2) è una formula \(\exists z.A(t,z)\); (punto 2) parallelamente, essendo \(P(t)\) una formula, pure \(\forall t.P(t)\) lo è; (punto 4) infine \(\forall t.P(t) \to \exists z.A(t,z)\).

Ciao Kaspar grazie per la risposta. Sono d'accordo con te, ma il dubbio mi viene per via delle parentesi che mi sa non hai considerato. La formula infatti è:

$∀t.(P(t) → ∃z.¬A(t, z))$

dopo l'iniziale $∀t.$ tutto è messo dentro parentesi, e non capisco se questa è una cosa consentita o meno...

Caspita, non avevo visto la coppia di parentesi, ti avevo risposto da telefono.
Comunque sì, se gli assiomi per la costruzione di FBF sono quelli sì. Ti basterà far vedere che la la formula tra le parentesi è ben formata, e lo è. Alla fine anche quella col quantificatore universale davanti al tutto è una FBF. (FBF sta per "formula ben formata").

Ok, io era proprio su questo che avevo il dubbio.

Quindi dopo $ ∀t. $ ci può essere anche una formula posta tra parentesi purché ovviamente questa sia ben formata.

Grazie mille del chiarimento!

Sì, proprio così: da FBF con quegli assiomi ti costruisci altre FBF (e solamente quelle!).