Re: [isabelle] On foundation axiom in ZF

The material that you quote is from the development of the constructible universe, and is highly technical. For more information, see the following paper:

The relative consistency of the axiom of choice — mechanized using Isabelle/ZF

The foundation axiom itself is simply called foundation and is defined in ZF.thy. I suggest that you find a contradiction from {t} : t on paper first and then reconstruct it formally.

Larry Paulson

On 17 Dec 2010, at 14:48, Victor Porton wrote:

> First, I don't understand what square brackets here means:
> definition
>   foundation_ax :: "(i=>o) => o" where
>     "foundation_ax(M) ==
>         ∀x[M]. (∃y[M]. y∈x) --> (∃y[M]. y∈x & ~(∃z[M]. z∈x & z ∈ y))"
> Please clarify.
> Second, could you help to prove "not({t}: t)"?
> -- 
> Victor Porton -

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