```Date: Aug 23, 2013 3:46 PM
Author: Ben Bacarisse
Subject: Re: A finite set of all naturals

quasi <quasi@null.set> writes:> Ben Bacarisse wrote:>>quasi writes:>>> Peter Percival wrote:>>>>Nam Nguyen wrote:>>>>>>>>>> I certainly meant "odd(x) can _NOT_ be defined as a >>>>> positive formula ...".>>>>>>>>Prove it.>>>>>> With Nam's new definition of positive/negative, I think>>> it's immediately provable (subject to some clarification as >>> to what a formula is) that odd(x) is a negative formula.>>>>>> Let even(x) <-> Ey(x=2*y).>>>>>> Assuming Nam's definition of "formula" supports the claim>>> that even(x) is a positive formula, then odd(x) must be>>> a negative formula since odd(x) is equivalent to ~even(x).>>>>That does not match my reading of the new definition.  It >>states that a formula is positive if it can be written in a>>particular form.  That odd(x) can be written in at least one>>form that does not match the requirements for positivity does>>not mean that it can't be.>> But Nam has already agreed to the properties:>> (1) Every formula is either positive or negative, but not both.>> (4) If P is positive, ~P is negative.>> (4') If P is negative, ~P is positive.>> Hence, since even(x) is positive, it's automatic that odd(x) must> be negative.The example I gave (odd(x) <-> Ey[Sx=2*y]) is clearly positive accordingto the definition he gave.  It may well be that ~even(x) is equallyclearly negative, but that just means that my odd(x) and ~even(x) arenot logically equivalent.  Given that we've not seen the system in full,and there even seems to be some doubt about basic permitted equivalences(see the recent exchange with Peter), I don't think one can say more atthis point.I do, however, think it's premature to agree that odd(x) must /always/be a negative formula and more on from there.>>My first counter example, odd(x) <-> Ey[Sx=2*y] seems to me to be>>to as positive as Nam's version of even, but he's forgotten about>>that as far as I can tell.>> Provided Nam allows the use of 'S' in formulas.He uses 2 in his "acceptable" formula for even and what is 2 if not SS0?-- Ben.
```