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


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)?


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