How can I show that the problem that : Whether an FO(PFP) formula is totally defined is not decidable?
I have these:
PFP-formula: partial fixed point formula.
A formula is totally defined if for all its subformulas of the form $[ PFP_{\overline x, X}\phi]\overline t$ the fixed point $F_\infty^{\phi}$ exists in every structure and for all assignments.
Every formula of partial fixed-point logic is equivalent to a formula containing exactly one occurrence of the $PFP$ operator.
Trahtenbrot's theorem:Finite satsfiability is not decidable.