Re: [isabelle] Important axiom question: can (seS q P) occur in (P x)?
No one probably has time for this, but for myself, for the problem I
described, I'm trying answer why I can't do this:
"Define a function P::(sT => bool) such that (P == (%x. ...~(x IN seS q
The "..." is any additional formula, and the function seS is a constant
that's only defined by its use in the axiom. If I can do that, then I'm
On 2/14/2013 2:37 PM, Gottfried Barrow wrote:
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 (P x)?
This archive was generated by a fusion of
Pipermail (Mailman edition) and