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 P)...))".

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 doomed.


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:

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.