Nam Nguyen wrote: > On 13/08/2013 10:19 AM, Ben Bacarisse wrote: >> Nam Nguyen <firstname.lastname@example.org> writes: >> <snip> >>>>>> Ben Bacarisse wrote: (quoting Nam) >> <snip> >>>>>>> Def-03a: even1(x) <-> Ey[x=y+y] >>>>>>> Def-03b: even2(x) <-> Ey[x=2*y] >>>>>>> Def-03c: even(x) <-> (even1(x) \/ even2(x)) >> <snip> >>> ... _an odd number can not be defined without addition_ while >>> an even number can (as per Def-03b above). >> >> odd(x) <-> ~Ey[x=2*y] > > Yes. There's something though from my original post (link) that has > missed being mentioned here but is _quite relevant_ . In that post > I had: > > 'Def-01: A formula is "positively assertive", or just "positive", iff > the formula contains no negation sign '~' ...' > > So my answer to your question below is: >> >> In what sense does your definition of even2 avoid addition, where this >> one of odd does not? > > in the sense that the formula defining even2 is a _positive_ formula > while the formula for your odd(x) above is _not_ . >> >> Personally, I'd say that both this and Def-03b use addition since >> multiplication in PA is usually defined using addition, but my >> view of what "without addition" means is not the issue here. > > So then with the caveat above about the requirement of positive formula > here, can you define odd(x), without addition *and* using _only_ > positive formula?
odd(x) is defined to be Ey[x=2*y] -> 0=S0
Have you forgotten that you never gave a coherent account of what a positive formula is?
> > If you can't, then my comments about "overly complex" and Induction- > non-Induction duality definitions of even(x) but _not_ of odd(x), and > the implication thereof in my proof still stands. >
-- Sorrow in all lands, and grievous omens. Great anger in the dragon of the hills, And silent now the earth's green oracles That will not speak again of innocence. David Sutton -- Geomancies