```Date: Apr 21, 2013 12:03 PM
Author: Frederick Williams
Subject: Re: Matheology S 224

fom wrote:> > On 4/20/2013 3:40 PM, Frederick Williams wrote:> > Nam Nguyen wrote:> >>> >> On 20/04/2013 8:59 AM, fom wrote:> >>> On 4/20/2013 5:25 AM, Alan Smaill wrote:> >>>> Frederick Williams <freddywilliams@btinternet.com> writes:> >>>>> >>>>> Nam Nguyen wrote:> >>>>>>> >>>>>> On 19/04/2013 5:55 AM, Frederick Williams wrote:> >>>>>>> Nam Nguyen wrote:> >>>>>>>>> >>>>>>>> On 18/04/2013 7:19 AM, Frederick Williams wrote:> >>>>>> >>>>>>> >>>>>>>> >>>>>>>>> Also, as I remarked elsewhere, "x e S' /\ Ay[ y e S' -> y e S]"> >>>>>>>>> doesn't> >>>>>>>>> express "x is in a non-empty subset of S".> >>>>>>>>> >>>>>>>> Why?> >>>>>>>> >>>>>>> It says that x is in S' and S' is a subset of S.> >>>>>>> >>>>>> How does that contradict that it would express "x is in a non-empty> >>>>>> subset of S", in this context where we'd borrow the expressibility> >>>>>> of L(ZF) as much as we could, as I had alluded before?> >>>>>> >>>>> You really are plumbing the depths.  To express that x is non-empty you> >>>>> have to say that something is in x, not that x is in something.> >>>>> >>>> but the claim was that x *is in* a non-empty set --> >>>> in this case S', which is non-empty, since x is an element of S',> >>>> and S' is a subset of S.> >>>>> >>>> (Much though it would be good for Nam to realise that> >>>> some background set theory axioms would be kind of useful here)> >>>>> >>>> >>> Yes.  I thought about posting some links indicating> >>> that primitive symbols are undefined outside of a> >>> system of axioms (definition-in-use)> >>>> >>> The other aspect, though, is that Nam appears to be using an> >>> implicit existence assumption.  So,> >>>> >>> AxASES'(xeS' /\ Ay(yeS' -> yeS))> >>>> >>> clarifies the statement and exhibits its second-order nature.> >>> This is fine since he claims that his work is not in the> >>> object language.> >>> >> Right.> >> > If fom's formula is to express "x is in a non-empty subset of S" then it> > needs to have both x and S free, so delete the first two quantifiers.> >> > Do you have a particular x and S in mind?I probably misunderstood.  If Nam saying that, for every x and every setS, x is in a non-empty subset of S, then your formula expresses that. But clearly it is false.> Or are we reverting to the distinction between real> and apparent variables from the first "Principia> Mathematica"?I call them free and bound respectively.> Or are we interpreting a statement in relation to a> general usage over an unspecified domain?  My quantifiers> are in place to make clear the meaning for general usage.> > Within any context involving proof, the leading quantifiers> obey rules:> > |AxASES'(xeS' /\ Ay(yeS' -> yeS))> |ASES'(teS' /\ Ay(yeS' -> yeS))> |ES'(teS' /\ Ay(yeS' -> yeP))> ||(xeP' /\ Ay(yeP' -> yeP))> > The original statement is assumed (hence, is stroked)> > The existential statement is assumed (hence, a second stroke)> > Now the presuppostions of use are clear.> > That was my only purpose.-- When a true genius appears in the world, you may know him by this sign, that the dunces are all in confederacy against him.Jonathan Swift: Thoughts on Various Subjects, Moral and Diverting
```