Description: Define the predicate which defines the set of valid Godel formulas. The
parameter n defines the maximum height of the formulas: the set
( Fmla(/) ) is all formulas of the form x e. y (which in our
coding scheme is the set ( { (/) } X. (om X. om ) ) ; see df-sat for the full coding scheme), see fmla0 , and each extra level adds to
the complexity of the formulas in ( Fmlan ) , see fmlasuc .
Remark: it is sufficient to have atomic formulas of the form x e. y
only, because equations (formulas of the form x = y ), which are
required as (atomic) formulas, can be introduced as a defined notion in
terms of e.g , see df-goeq .
( Fmla_om ) = U_ n e. _om ( Fmlan ) is the set of all valid
formulas, see fmla . (Contributed by Mario Carneiro, 14-Jul-2013)