Re: realizing and omitting types


Torkel Franzen wrote:
> "Per Freem" <perfreem@xxxxxxxxx> writes:
>
> > the point is that
> > i want to have some formula of one free variable to imply everything in
> > X.
>
> If T proves (x)(y)(F1(x)&F1(y)->x=y) and T proves
> (Ex)(F1(x)&Fk(x)) for every k, T proves (x)(F1(x)->Fk(x)) for every k.

sorry to be thick but that's precisely the step i am missing. what is
the inbetween step? if T proves (Ex)F1(x)&Fk(x)) for every k, how does
(x)(y)(F1(x) &...&Fk(x) & F1(y) &...&Fk(y)->x = y) get you from the
existential to the universal claim, i.e. (x)(F1(x)->Fk(x))?

.

Relevant Pages

  • Re: realizing and omitting types
    ... >> sorry to be thick but that's precisely the step i am missing. ... two distinct values, a!= b, each satisfy F1 but do not satisfy all the ... Prev by Date: ...
    (sci.logic)
  • Re: realizing and omitting types
    ... > sorry to be thick but that's precisely the step i am missing. ... > existential to the universal claim, ... Prev by Date: ...
    (sci.logic)
  • Re: Compact connected Hausdorff
    ... > of U are also open in X (a relatively open subset of an open set is ... > What am I missing? ... Prev by Date: ...
    (sci.math)
  • Form.SetBounds
    ... missing something here? ... Letting is become visible and then setting ... Steve ... Prev by Date: ...
    (microsoft.public.dotnet.languages.vb)
  • Re: Exclusive checkboxes
    ... only one option button on the whole page/sheet can be selected. ... I dont know if there is a way of grouping the options together. ... let me know if I am missing something. ... Prev by Date: ...
    (microsoft.public.excel)