*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Important axiom question: can (seS q P) occur in (P x)?*From*: Gottfried Barrow <gottfried.barrow at gmx.com>*Date*: Thu, 14 Feb 2013 17:09:23 -0600*In-reply-to*: <511D4B08.8000909@gmx.com>*References*: <511D4B08.8000909@gmx.com>*User-agent*: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0

Thanks, GB On 2/14/2013 2:37 PM, Gottfried Barrow wrote:

Hi,Axioms are to be feared, so I ask this question. There is the generalFOL 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 wherephi(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 arecursive way to do it.If it can be done, how would I specify that (seS q P) not be allowedin (P x)?Thanks, GB

**Follow-Ups**:**Re: [isabelle] Important axiom question: can (seS q P) occur in (P x)?***From:*Gottfried Barrow

**References**:**[isabelle] Important axiom question: can (seS q P) occur in (P x)?***From:*Gottfried Barrow

- Previous by Date: [isabelle] Important axiom question: can (seS q P) occur in (P x)?
- Next by Date: [isabelle] Can't generate browser_info
- Previous by Thread: [isabelle] Important axiom question: can (seS q P) occur in (P x)?
- Next by Thread: Re: [isabelle] Important axiom question: can (seS q P) occur in (P x)?
- Cl-isabelle-users February 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list