[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:
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and