# [isabelle] Important axiom question: can (seS q P) occur in (P x)?

Hi,

`Axioms are to be feared, so I ask this question. There is the general
``FOL formula which I modify, but given here unmodified:
`
!q. ?r. !x. (x IN r <-> (x IN q & phi(x))),

`where it is required that r not occur in the formula phi(x), and where
``phi(x) is a FOL formula with a free variable x.
`
I implement it like this:
!q. !P. !x. ( x IN (seS q P) <-> (x IN q & (P x)))
The question becomes, "Can the term (seS q P) occur in (P x)?"
The function and types are as follows:
typedecl sT
q, x :: sT
P::(sT => bool)
consts seS :: "(sT => (sT => bool) => sT)"
consts IN :: "sT => sT => bool"

`It seems like things would get circular, but then maybe there's a
``recursive way to do it.
`

`If it can be done, how would I specify that (seS q P) not be allowed in
``(P x)?
`
Thanks,
GB

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*