Two ways for formally define a predicate

[Dan Christensen]

Here I consider two different ways to formally define a predicate, say the predicate Even(x) which is to be interpreted as "x is even."

CASE 1

ALL(a):[a in n => [Even(a) <=> EXIST(b):[b in n & a=2*b]]]

CASE 2

ALL(a):[Even(a) <=> a in n & EXIST(b):[b in n & a=2*b]

(In both cases, n = the set of natural numbers.)

There is a subtle difference in outcomes. Even(1) will be FALSE in both cases. Even(-1), however, will be UNDEFINED in case 1, but FALSE in case 2.

Your comments?

Dan

Download my DC Proof 2.0 freeware at http://www.dcproof.com
Visit my Math Blog at http://www.dcproof.wordpress.com

[Mostowski Collapse]

You can make a better example, to show that Case 1: Dan-O-Matik
style is not well defined and Case 2: Ordinary style is well defined:

Case 1: Dan-O-Matik style natural numbers:
ALL(a):[a e z => [a e n <=> a >= 0]]

Case 2: Ordinary style natural numbers
ALL(a):[a e n <=> a e z & a >= 0]

There is an unwanted difference. 1/2 e n will be undecided
in Dan-O-Matik style whereas we can prove ~(1/2 e n) as expected

in ordinary stlye.

[Mostowski Collapse]

So there is a catastrophic information loss, when we would
bootstrap the natural numbers from the positive and negative
integers in Dan-O-Matik style. The information of a proof

~(1/2 e z), which is expected to available, is not transfered
to ~(1/2 e n). So Dan-O-Matik style definitions introduce
plenty of dark elements. I think we have even dark

elements in his Dan-O-Matik style Peano Axioms. I
guess we cannot prove:

/* Not provable in Dan-O-Matik Peano Axioms */
~(n e n) ~(n = 0)

Whereas in set theory, thanks to the axiom of
regularity, the first is provable, and the second folllows
from the way zero is constructed:

/* Provable in set theory */
~(ω e ω) ~(ω = {})

[Mostowski Collapse]

But this here could be another type of dark element.
Rather a naming problem:

> /* Not provable in Dan-O-Matik Peano Axioms */
> ~(n e n) ~(n = 0)

Not the same type of dark element like -1 or so.
Maybe this is the holy grail, that Culio was looking
for, when he talked about "proof it", with

"finite induction"? We will never know, since
Culio couldn't explain himself after asking him,
his Autism didn't allow him to formulate

what is in his mind. Maybe he was intimitated
by Jeff Barstool who wants to ban brainstorming
and brainwriting from sci.logic.

Good luck with that!

[Mostowski Collapse]

Have to revise, set theory is quite capable,
it can not only prove:

~(n e n)

But it can also prove:

~(n = 0)

So we dont need reference to ω and also no
reference to {}. The former, ~(n e n) follows from
regularity and ~(n = 0) follows from 0 e n and regularity.

Proof:
Assume towards a contradiction n = 0. Then
because 0 e n we would have n e n, contradicting
regularity, so it is ~(n = 0).

[Dan Christensen]

On Monday, May 9, 2022 at 2:15:40 AM UTC-4, Mostowski Collapse (aka Jan Burse) wrote:

> Dan Christensen schrieb am Montag, 9. Mai 2022 um 06:11:47 UTC+2:
> > Here I consider two different ways to formally define a predicate, say the predicate Even(x) which is to be interpreted as "x is even."
> >
> > CASE 1
> >
> > ALL(a):[a in n => [Even(a) <=> EXIST(b):[b in n & a=2*b]]]
> >
> > CASE 2
> >
> > ALL(a):[Even(a) <=> a in n & EXIST(b):[b in n & a=2*b]
> >
> > (In both cases, n = the set of natural numbers.)

Maybe you missed that point, Jan Burse?

> >
> > There is a subtle difference in outcomes. Even(1) will be FALSE in both cases. Even(-1), however, will be UNDEFINED in case 1, but FALSE in case 2.
> >

> You can make a better example, to show that Case 1: Dan-O-Matik
> style is not well defined and Case 2: Ordinary style is well defined:
>
> Case 1: Dan-O-Matik style natural numbers:
> ALL(a):[a e z => [a e n <=> a >= 0]]
>

Not clear what you are trying to do here, Jan Burse. I'm guessing you are trying to construct the set non-negative integers nnz. In that case, you would want something like:

ALL(a):[a e nnz <=> a in z & a>=0]

Where z = the set of integers

> Case 2: Ordinary style natural numbers
> ALL(a):[a e n <=> a e z & a >= 0]
>

Weird. Normally, you would construct the integers from the natural numbers (Peano's Axioms), not the other way around.

> There is an unwanted difference. 1/2 e n will be undecided

I chose -1 (not 1/2) in my example as an obvious non-element of the set n (the natural numbers). You could use 1/2 or an arbitrary x not in n if you prefer. The argument is still the same: E(1/2) is undefined in case 1 (as it should be), and false in case 2.

> in Dan-O-Matik style whereas we can prove ~(1/2 e n) as expected
>
> in ordinary stlye.

This needs some work, Jan Burse.

[Dan Christensen]

On Monday, May 9, 2022 at 12:11:47 AM UTC-4, Dan Christensen wrote:
> Here I consider two different ways to formally define a predicate, say the predicate Even(x) which is to be interpreted as "x is even."
>
> CASE 1
>
> ALL(a):[a in n => [Even(a) <=> EXIST(b):[b in n & a=2*b]]]
>

Then we could simply define ALL(a):[Odd(a) <=> ~Even(a)]

> CASE 2
>
> ALL(a):[Even(a) <=> a in n & EXIST(b):[b in n & a=2*b]
>

Then we could NOT simply define ALL(a):[Odd(a)<=> ~Even(a)]

Since we would then have, for example, ~Even(1/2) and Odd(1/2)?

[Mostowski Collapse]

Try:
Case 1:

ALL(a):[a in n => [Even(a) <=> EXIST(b):[b in n & a=2*b]]]

ALL(a):[a in n => [Odd(a) <=> ~EXIST(b):[b in n & a=2*b]]]

You cannot prove:
ALL(a):[Odd(a)<=> ~Even(a)]

Try:
Case 2:
ALL(a):[Even(a) <=> a in n & EXIST(b):[b in n & a=2*b] ]
ALL(a):[Odd(a) <=> a in n & ~EXIST(b):[b in n & a=2*b] ]

You cannot prove:
ALL(a):[Odd(a)<=> ~Even(a)

[FredJeffries]

On Sunday, May 8, 2022 at 9:11:47 PM UTC-7, Dan Christensen wrote:
> Here I consider two different ways to formally define a predicate, say the predicate Even(x) which is to be interpreted as "x is even."
>
> CASE 1
>
> ALL(a):[a in n => [Even(a) <=> EXIST(b):[b in n & a=2*b]]]
>
> CASE 2
>
> ALL(a):[Even(a) <=> a in n & EXIST(b):[b in n & a=2*b]
>
> (In both cases, n = the set of natural numbers.)
>
> There is a subtle difference in outcomes. Even(1) will be FALSE in both cases. Even(-1), however, will be UNDEFINED in case 1, but FALSE in case 2.
>
> Your comments?

Which case allows for the existence of even functions and even permutations and ... ?

https://en.wikipedia.org/wiki/Parity_(mathematics)

https://owl.purdue.edu/owl/general_writing/common_writing_assignments/definitions.html

By the way, every number theory textbook says that -2 is even.

[Mostowski Collapse]

What works for case 1 is:
ALL(a):[a e n => [Odd(a)<=> ~Even(a)] ]

What works for case 2 is:
ALL(a):[Odd(a) <=> a e n & ~Even(a)]

The later is called relative complement, and can be written as:

Odd = n \ Even

This is high school math. You can show Even = n \ Odd.

[Dan Christensen]

On Monday, May 9, 2022 at 1:43:23 PM UTC-4, Mostowski Collapse wrote:
> Try:
> Case 1:
> ALL(a):[a in n => [Even(a) <=> EXIST(b):[b in n & a=2*b]]]
> ALL(a):[a in n => [Odd(a) <=> ~EXIST(b):[b in n & a=2*b]]]
>
> You cannot prove:
> ALL(a):[Odd(a)<=> ~Even(a)]
>

Why would I want to "prove" a definition?

CASE 1

ALL(a):[a in n => [Even(a) <=> EXIST(b):[b in n & a=2*b]]]

Define Odd

ALL(a):[Odd(a) <=> ~Even(a)]

Reasonable Conclusion: ALL(a):[a in n => [Odd(a) <=> ~EXIST(b):[b in n & a=2*b]]]

CASE 2

ALL(a):[Even(a) <=> a in n & EXIST(b):[b in n & a=2*b]]

Wonky Conclusion : ALL(a):[~a in n => Odd(a)] (your "dark elements?")

Deal with it, Jan Burse.

[Mostowski Collapse]

Talking nonsense like always? You cannot prove:

ALL(a):[~a in n => Odd(a)]

From this here:

Mostowski Collapse schrieb am Montag, 9. Mai 2022 um 19:43:23 UTC+2:
> ALL(a):[Odd(a) <=> a in n & ~EXIST(b):[b in n & a=2*b] ]
https://groups.google.com/g/sci.logic/c/gV50jEU6fvQ/m/jLatqKbwAQAJ

Whats wrong with you?

[Dan Christensen]

On Monday, May 9, 2022 at 3:48:07 PM UTC-4, Mostowski Collapse wrote:
> Talking nonsense like always? You cannot prove:
> ALL(a):[~a in n => Odd(a)]

Wrong again, Jan Burse.

Case 2

1. ALL(a):[Even(a) <=> a in n & EXIST(b):[b in n & a=2*b]]
Axiom

2. ALL(a):[Odd(a) <=> ~Even(a)]
Axiom


Suppose...

3. ~x in n
Premise

4. Even(x) <=> x in n & EXIST(b):[b in n & x=2*b]
U Spec, 1

5. [Even(x) => x in n & EXIST(b):[b in n & x=2*b]]
& [x in n & EXIST(b):[b in n & x=2*b] => Even(x)]
Iff-And, 4

6. Even(x) => x in n & EXIST(b):[b in n & x=2*b]
Split, 5

7. ~[x in n & EXIST(b):[b in n & x=2*b]] => ~Even(x)
Contra, 6

8. ~~[~x in n | ~EXIST(b):[b in n & x=2*b]] => ~Even(x)
DeMorgan, 7

9. ~x in n | ~EXIST(b):[b in n & x=2*b] => ~Even(x)
Rem DNeg, 8

10. ~x in n | ~EXIST(b):[b in n & x=2*b]
Arb Or, 3

11. ~Even(x)
Detach, 9, 10

12. Odd(x) <=> ~Even(x)
U Spec, 2

13. [Odd(x) => ~Even(x)] & [~Even(x) => Odd(x)]
Iff-And, 12

14. ~Even(x) => Odd(x)
Split, 13

15. Odd(x)
Detach, 14, 11

As Required:

16. ALL(a):[~a in n => Odd(a)]
Conclusion, 3

[Mostowski Collapse]

Bat shit crazy and high as a kite. You didnt prove it from
ALL(a):[Odd(a) <=> a in n & ~EXIST(b):[b in n & a=2*b] ]
You only confirmed what I told you already:

> ALL(a):[Even(a) <=> a in n & EXIST(b):[b in n & a=2*b] ]

> ALL(a):[Odd(a) <=> a in n & ~EXIST(b):[b in n & a=2*b] ]

>
> You cannot prove:
> ALL(a):[Odd(a)<=> ~Even(a)

Or to rephrase it so that Dan O Matik also understands
it, the case 2 Even and Odd are not related through
unrestricted complement, we do not have Even = V \ Odd.

If they were related by unrestricted complement,
one could prove nonsense like:

ALL(a):[~a in n => Odd(a)]

as you just did. But the above is not provable for the case 2 Even
and Odd. Easy counter example: ~(-1 e n) and ~Odd(-1). In the
Case 2 Odd we do not have Odd(-1).

Whats wrong with you?

[Mostowski Collapse]

Both, Case 1 Even/Odd and Case 2 Even/Odd are not
related by unrestriced complement.
Possibly you still believe that your Case 1 Even/Odd are
related by untestriced complement, right?

I guess your hallucinations are based on the idea
that ~UNDEFINED = UNDEFINED. Where do you get this
ideas from, from SQL which has 3-valued logic? We are
still in classical logic here, even if you use case 1, its

still 2-valued logic interpretable.

[Dan Christensen]

On Monday, May 9, 2022 at 4:17:37 PM UTC-4, Mostowski Collapse wrote:
> Bat shit crazy and high as a kite. You didnt prove it from
> ALL(a):[Odd(a) <=> a in n & ~EXIST(b):[b in n & a=2*b] ]
> You only confirmed what I told you already:
> > ALL(a):[Even(a) <=> a in n & EXIST(b):[b in n & a=2*b] ]
> > ALL(a):[Odd(a) <=> a in n & ~EXIST(b):[b in n & a=2*b] ]
> >
> > You cannot prove:
> > ALL(a):[Odd(a)<=> ~Even(a)

Pay attention, Jan Burse! Again, you cannot "prove" a definition. Here we have the DEFINITION of Odd( ). Yeah, it causes our wonky definition of Even( ) with its "dark elements" to blow up real good. It does work as you would expect for the standard definition. Deal with it.

[Mostowski Collapse]

I do not prove a definition. The two definitons are:

ALL(a):[Even(a) <=> a in n & EXIST(b):[b in n & a=2*b] ]
ALL(a):[Odd(a) <=> a in n & ~EXIST(b):[b in n & a=2*b] ]

whats wrong with you? from the two definitions you cannot prove:

ALL(a):[Odd(a)<=> ~Even(a)]

Easy counter example ~Odd(-1) & ~Even(-1).

Dan Christensen schrieb:

[Mostowski Collapse]

You can check Euclid:

6. An even number is that which is divisible into two equal parts.
7. An odd number is that which is not divisible into two equal parts,
or that which differs by a unit from an even number.
http://aleph0.clarku.edu/~djoyce/elements/bookVII/defVII6.html

He doesn't define odd in terms of even with negation.

***************************************************************
The greek were very constructive sometimes,
maybe that is why Euclid avoid negation?
***************************************************************

The negation thing is a Dan Christense-ism. Namely to
connect two species, whereas the normal procedure
is to derive species from genera, and you can negate

the differentiae. But you do not negate species to
get new species. Maybe in natural language one might
tend to believe this is the case, but in natural language there

is possibly enough context so that the normal path is taken.

[Mostowski Collapse]

The genera differentiae path uses also negation,
in that it negates the differentiae. But the result
is bounded complement, which is less problematic

in set theory. Since the bounded complement of
a set with a class is a again a set. On the other hand
the Dan Christense-ism uses unbounded complement,

the unbound complement of a set leads to a class.
I think Dan Christensen proved that already here,
but maybe in his UNDEFINED delirium he forgot:

The non-existence of the set of all things that are NOT purple
https://groups.google.com/g/sci.logic/c/nzEj1sXJCUg/m/n9XUKSj3AgAJ

It we would have 3 valued sets, some fuzzy sets, we
could indeed approach the probem differently, and do
something with unbounded complement.

[Mostowski Collapse]

Maybe its an education failure. We see its not a problem of
a gap in FOL + ZFC, as Jeff Barstool might suggest. Its good
ole Aristoteles and his categories. Or as wikipedia explains:

Until the late 19th century, theories of categories based on
Porphyry's work were still being taught to students of logic.
https://en.wikipedia.org/wiki/Porphyrian_tree

[Dan Christensen]

On Monday, May 9, 2022 at 5:12:08 PM UTC-4, Mostowski Collapse wrote:

> Dan Christensen schrieb:
> > On Monday, May 9, 2022 at 4:17:37 PM UTC-4, Mostowski Collapse wrote:
> >> Bat shit crazy and high as a kite. You didnt prove it from
> >> ALL(a):[Odd(a) <=> a in n & ~EXIST(b):[b in n & a=2*b] ]
> >> You only confirmed what I told you already:
> >>> ALL(a):[Even(a) <=> a in n & EXIST(b):[b in n & a=2*b] ]
> >>> ALL(a):[Odd(a) <=> a in n & ~EXIST(b):[b in n & a=2*b] ]
> >>>
> >>> You cannot prove:
> >>> ALL(a):[Odd(a)<=> ~Even(a)
> >
> > Pay attention, Jan Burse! Again, you cannot "prove" a definition. Here we have the DEFINITION of Odd( ). Yeah, it causes our wonky definition of Even( ) with its "dark elements" to blow up real good. It does work as you would expect for the standard definition. Deal with it.
> >
> I do not prove a definition. The two definitons are:
> ALL(a):[Even(a) <=> a in n & EXIST(b):[b in n & a=2*b] ]
> ALL(a):[Odd(a) <=> a in n & ~EXIST(b):[b in n & a=2*b] ]
> whats wrong with you? from the two definitions you cannot prove:
>
> ALL(a):[Odd(a)<=> ~Even(a)]
>
> Easy counter example ~Odd(-1) & ~Even(-1).
>

A wonky definition of Odd isn't going to salvage your wonky definition of Even, Jan Burse. You still have this embarrassing result without any definition of Odd:

ALL(a):[~a in n => ~Even(a)]

You really should try to avoid such "dark elements" silliness, Jan Burse. If something is not a natural number, it makes no sense the to say here that it is even or odd. When will you learn?

Wonky definition of Even:

1. ALL(a):[Even(a) <=> a in n & EXIST(b):[b in n & a=2*b]]
Axiom

Suppose...

2. ~x in n
Premise

3. Even(x) <=> x in n & EXIST(b):[b in n & x=2*b]
U Spec, 1

4. [Even(x) => x in n & EXIST(b):[b in n & x=2*b]]
& [x in n & EXIST(b):[b in n & x=2*b] => Even(x)]
Iff-And, 3

5. Even(x) => x in n & EXIST(b):[b in n & x=2*b]
Split, 4

6. ~[x in n & EXIST(b):[b in n & x=2*b]] => ~Even(x)
Contra, 5

7. ~~[~x in n | ~EXIST(b):[b in n & x=2*b]] => ~Even(x)
DeMorgan, 6

8. ~x in n | ~EXIST(b):[b in n & x=2*b] => ~Even(x)
Rem DNeg, 7

9. ~x in n | ~EXIST(b):[b in n & x=2*b]
Arb Or, 2

10. ~Even(x)
Detach, 8, 9

Wonky result:

11. ALL(a):[~a in n => ~Even(a)]
Conclusion, 2

[Dan Christensen]

On Monday, May 9, 2022 at 4:17:37 PM UTC-4, Mostowski Collapse wrote:
> Bat shit crazy and high as a kite. You didnt prove it from
> ALL(a):[Odd(a) <=> a in n & ~EXIST(b):[b in n & a=2*b] ]
> You only confirmed what I told you already:

> > ALL(a):[Even(a) <=> a in n & EXIST(b):[b in n & a=2*b] ]

Again, from this wonky definition, you get the wonky result:

ALL(a):[~a in n => ~Even(a)]

As if you could assign any truth value to for anything not in n.

> > ALL(a):[Odd(a) <=> a in n & ~EXIST(b):[b in n & a=2*b] ]
> >

And from this wonky definition, you get the wonky result:

ALL(a):[~a in n => ~Odd(a)]

> > You cannot prove:
> > ALL(a):[Odd(a)<=> ~Even(a)

Why would I bother? It's really just and abbreviation. Your definitions here are clearly flawed as I have shown. I use this definition of Odd quite effectively in conjunction with the standard definition of Even. What are you hoping to accomplish here? Maybe I can help.

Dan

[Mostowski Collapse]

Yes Wonky, Euclid nowhere writes ALL(a):[Odd(a)<=> ~Even(a)

LoL

[Mostowski Collapse]

You can check yourself Euclid:

6. An even number is that which is divisible into two equal parts.
7. An odd number is that which is not divisible into two equal parts,
or that which differs by a unit from an even number.
http://aleph0.clarku.edu/~djoyce/elements/bookVII/defVII6.html

[Mostowski Collapse]

if we follow Euclid first defining Even and Odd from
divisible into two equal parts, and if we use your Case 1
style definition, we find a counter model to

your nonsense ALL(a):[Odd(a)<=> ~Even(a)]. In a counter
model one does not infer something. You just set some
values like Even(-1)=TRUE and Odd(-1) = TRUE, and you

see that these axiom instances are satisfied, because
these are vacuously true:

[-1 in n => [Even(-1) <=> EXIST(b):[b in n & -1=2*b]]]
[-1 in n => [Odd(-1) <=> ~EXIST(b):[b in n & -1=2*b]]]

And this conclusion is not satsified:

ALL(a):[Odd(a)<=> ~Even(a)]

Since this counter model exists, the conclusion
is not provable. If you really think the above is provable,
from Euclid Even Odd in Case 1 style, then please show a proof.

But there cannot be one, since there is a counter modeöl.

[Dan Christensen]

On Tuesday, May 10, 2022 at 3:10:33 AM UTC-4, Mostowski Collapse wrote:
> if we follow Euclid first defining Even and Odd from
> divisible into two equal parts, and if we use your Case 1
> style definition, we find a counter model to
>
> your nonsense ALL(a):[Odd(a)<=> ~Even(a)]. In a counter
> model one does not infer something. You just set some
> values like Even(-1)=TRUE and Odd(-1) = TRUE, and you
>
> see that these axiom instances are satisfied, because
> these are vacuously true:
>
> [-1 in n => [Even(-1) <=> EXIST(b):[b in n & -1=2*b]]]
> [-1 in n => [Odd(-1) <=> ~EXIST(b):[b in n & -1=2*b]]]
>
> And this conclusion is not satsified:
>
> ALL(a):[Odd(a)<=> ~Even(a)]
>

Using these definitions...

1 ALL(a):[a in n => [Even(a) <=> EXIST(b):[b in n & a=2*b]]]
Axiom

2 ALL(a):[a in n => [Odd(a) <=> ~EXIST(b):[b in n & a=2*b]]]
Axiom

It is trivial to prove: ALL(a):[a in n => [Odd(a) <=> ~Even(a)]] (32 lines in DC Proof)

Sorry, no "dark elements" allowed, Jan Burse. As you would expect, each quantifier here is restricted to the set of natural numbers n. Deal with it.

> Since this counter model exists, the conclusion
> is not provable.

No "counter model" here, Jan Burse.

[Dan Christensen]

"(∀a(Na → (Ea ↔ Pa)) ∧ ∀a(Na → (Oa ↔ ¬Pa))) → ∀a(Na → (Oa ↔ ¬Ea)) is valid."

https://www.umsu.de/trees/#~6a(Na~5(Ea~4Pa))~1~6a(Na~5(Oa~4~3Pa))~5~6a(Na~5(Oa~4~3Ea))

[Mostowski Collapse]

You are not very good in giving credit. And your brain
is slower than a snails brain. You stole this from here,
namely you stole from a post of mine from yesterday:

Mostowski Collapse schrieb am Montag, 9. Mai 2022 um 20:12:13 UTC+2:
> What works for case 1 is:
> ALL(a):[a e n => [Odd(a)<=> ~Even(a)] ]
>
> What works for case 2 is:
> ALL(a):[Odd(a) <=> a e n & ~Even(a)]
>
> The later is called relative complement, and can be written as:
>
> Odd = n \ Even
>
> This is high school math. You can show Even = n \ Odd.

https://groups.google.com/g/sci.logic/c/gV50jEU6fvQ/m/NZH1mTnyAQAJ

Whats wrong with you? Alzheimer?

[Dan Christensen]

On Tuesday, May 10, 2022 at 12:12:05 PM UTC-4, Mostowski Collapse wrote:

> > What works for case 1 is:
> > ALL(a):[a e n => [Odd(a)<=> ~Even(a)] ]
> >
> > What works for case 2 is:
> > ALL(a):[Odd(a) <=> a e n & ~Even(a)]
> >

Haven't you learned your lesson yet, Jan Burse? In mathematics, whenever possible, you must explicitly restrict every quantifier (e.g. by a set or predicate). So, scrap case 2. Use the more standard approach (case 1) and avoid embarrassing yourself like this.

[Mostowski Collapse]

The quantifier in here is restricted:

ALL(a):[Odd(a) <=> a e n & ~Even(a)]

You can transform it into two sentences,
by using (A <=> B) <=> (A => B) & (B => A) and
by using ALL(x):[A & B] <=> ALL(x):A & ALL(x):B:

ALL(a):[Odd(a) => a e n & ~Even(a)]

ALL(a):[a e n => (~Even(a) => Odd(a))]

The first sentence is restriced by positive Odd(a)
The second sentence is restricted by positive a e n.
The first sentence is restricted by a predicate as you require.
The second sentence is restricted by a set as you reguire.

Whats wrong with you? Alzheimer?

[Dan Christensen]

On Tuesday, May 10, 2022 at 2:20:07 PM UTC-4, Mostowski Collapse (aka Jan Burse) wrote:

> Dan Christensen schrieb am Dienstag, 10. Mai 2022 um 19:07:31 UTC+2:
> > On Tuesday, May 10, 2022 at 12:12:05 PM UTC-4, Mostowski Collapse wrote:
> > > > What works for case 2 is:
> > > > ALL(a):[Odd(a) <=> a e n & ~Even(a)]
> > Haven't you learned your lesson yet, Jan Burse? In mathematics, whenever possible,
> you must explicitly restrict every quantifier (e.g. by a set or predicate).

> The quantifier in here is restricted:
> ALL(a):[Odd(a) <=> a e n & ~Even(a)]
> You can transform it into two sentences,
> by using (A <=> B) <=> (A => B) & (B => A) and
> by using ALL(x):[A & B] <=> ALL(x):A & ALL(x):B:
> ALL(a):[Odd(a) => a e n & ~Even(a)]
> ALL(a):[a e n => (~Even(a) => Odd(a))]
>
> The first sentence is restriced by positive Odd(a)
> The second sentence is restricted by positive a e n.
> The first sentence is restricted by a predicate as you require.
> The second sentence is restricted by a set as you reguire.

Here is what you need, Jan Burse:

1. ALL(a):[a in n => [Even(a) <=> EXIST(b):[b in n & a=2*b]]] (Both quantifiers restricted by the set of natural numbers n)
2. ALL(a):[Odd(a) <=> ~Even(a)] (An abbreviation for ~Even)

Advantage: No wonkiness about ALL(a):[~a in n => Odd(a)] as with your preferred definition, Jan Burse.

That's probably enough time spent debating the definition of the even numbers.

[Jeff Barnett]

So Odd({}) is true?

I'm beginning to think your system approach is very unsound. You are
also resistant to help so I'll butt out and enjoy a little chuckle when
I accidentally read a few messages in one of your threads.
--
Jeff Barnett

[Dan Christensen]

In Jan Burse's preferred definition. Not in the standard definition.

Dan

[Jeff Barnett]

I don't think that you think before responding. Look at "2." above. Now
look at it again. For ALL(a) we let a be the null set, "{}". Y system
now evaluates our "Even(a)" which is false. Now the definition "Odd(a)
<=> ~Even(a)" shows that Odd(a) === Odd({}) is true. Kindergarten lesson
concluded.

My suggestion to you is 1) get your hand out of your pants, 2) use the
extra time to think about what you are doing, 3) quit typing until you
figure out what some one is trying to tell you. It will be hard for you
to break all those bad habits that you have acquired but you ought to
give it a try.
--
Jeff Barnett

[Dan Christensen]

You mean a = 0? Did you miss the point that (1) can only be applied for elements of n = the set of natural numbers as defined by Peano's Axioms?

> Y [Your?] system

> now evaluates our "Even(a)" which is false.

Even(0) will be true. Odd(0) will be false.
Even(1) will be false. Odd(1) will be true.
And so on.

I don't see a problem. Have I missed something?

[Jeff Barnett]

-----------------------------
/ \
|
You really do not take the time to read what you reply to, do you? I
used an example that was consistent in its assumptions and you couldn't
follow it because you were too busy masturbating again. I know what you
meant but failed to express within your formalism. you might have write
your 2 above as "All(a):[a in n -> Odd(a) <=> ~Even(a)]" but you failed
to do so; hence your conclusions from it are wrong. It's mistakes like
this that formal assistance systems are supposed to help their users to
avoid making. You seem to want to encourage these mistakes. Sad. It's
too bad you cut off the actual deductions one can make so some readers
will waste their time and miss an opportunity to learn reasons that our
mathematician and logician forefathers fought battles over how to build
robust and trustworthy logical systems.

> You mean a = 0? Did you miss the point that (1) can only be applied for elements of n = the set of natural numbers as defined by Peano's Axioms?



>> Y [Your?] system
>> now evaluates our "Even(a)" which is false.
>
> Even(0) will be true. Odd(0) will be false.
> Even(1) will be false. Odd(1) will be true.
> And so on.
>
> I don't see a problem. Have I missed something?
>
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

--
Jeff Barnett

[Dan Christensen]

[snip]

> I know what you
> meant but failed to express within your formalism. you might have write
> your 2 above as "All(a):[a in n -> Odd(a) <=> ~Even(a)]" but you failed
> to do so;

I posted that in a previous version. The "a in n" turned out to be redundant. It is just an abbreviation.

> > You mean a = 0? Did you miss the point that (1) can only be applied for elements of n = the set of natural numbers as defined by Peano's Axioms?
>

No comment?

>
>
> >> Y [Your?] system
> >> now evaluates our "Even(a)" which is false.
> >
> > Even(0) will be true. Odd(0) will be false.
> > Even(1) will be false. Odd(1) will be true.

You disagree?

[Mostowski Collapse]

Students Beware: Don't be a victim of Dans fake math,
its a syphilis brain on the run, claiming this:

ALL(a):[~a in n => Odd(a)]

But it is not provable from:

ALL(a):[Odd(a) <=> a e n & ~Even(a)]

Whats is wrong with you? Alzheimer?

[Dan Christensen]

On Wednesday, May 11, 2022 at 2:26:43 AM UTC-4, Mostowski Collapse wrote:
> Students Beware: Don't be a victim of Dans fake math,
> its a syphilis brain on the run, claiming this:
> ALL(a):[~a in n => Odd(a)]

That would be the case with your wonky definition, Jan Burse. Not so with my more conventional alternative. You really must explicityly restrict the quantifiers to the set of natural numbers N as follows:

ALL(a):[a in N => [Even(a) <=> EXIST(b):[b in N & a=2*b]]]

I hope this helps.

[Mostowski Collapse]

You can try both, show that general "evenness" makes no sense:

Case 1:
ALL(D):ALL(+):ALL(a):[a in D => [Even(D,+)(a) <=> EXIST(b):[b in D & a=2*b]]]

Case 2:
ALL(D):ALL(+):ALL(a):[Even(D,+)(a) <=> a e D & EXIST(b):[b e D & b+b=a]]

You will still see that EvenQ ∩ N =\= EvenN.

Proof:
EvenQ ∩ N = N. But 1 e N and ~(1 e EvenN)

[Mostowski Collapse]

With your case 1 definition that is motivated by general
evenness, you only get Dan-O-Matiks meningeal paresis:

Case 1: Dan-O-Matiks Syphilis Brain

ALL(a):[a in N => [Even(a) <=> EXIST(b):[b in N & a=2*b]]]

You can even not prove:

/* Not Provable in Syphilis Brain World */
ALL(a):[~a e n => ~Even(a)]

So we don't know what Even is outside of n. Is it EvenN
or EvenQ? For EvenQ we have EvenQ(a) when ~a e n
and a e q. So EvenQ is indeed a counter example to

the above. But EvenQ is also a counter example to the
idea to make Even open, . Since EvenQ even starts to
disagree with EvenN, we have EvenQ ∩ N =\= EvenN. So I

would say Dan Christensens problem is progressed neurosyphilis.

[Mostowski Collapse]

Dan Christensen, can you send us a picture of yourself?
Does it look like this here:

https://www.fazialis.de/de/gesichtslaehmung/#lightbox[4859]

This could improve the diagnosis of your mental
illness and progressed neurosyphilis.

[Mostowski Collapse]

Following Euclid we can also do:

Case 4:
Even = { a e n | a = 0 mod 2 }
Odd = { a e n | a = 1 mod 2 }

The notation a = m mod k does a little more, but when
m < k, then we ask for the remainder, i.e. a = k*b+ m, where
b is the result of integer division.

So the above is an alternative to Case 3 where we
used a = 2*b and a = 2*b+1. Of course we have:

ALL(a):[~a in n => ~Even(a)]

ALL(a):[~a in n => ~Odd(a)]

[Dan Christensen]

On Wednesday, May 11, 2022 at 9:19:36 AM UTC-4, Mostowski Collapse (wrote:
> With your case 1 definition that is motivated by general

> evenness...
>
> Case 1:

> ALL(a):[a in N => [Even(a) <=> EXIST(b):[b in N & a=2*b]]]
> You can even not prove:
>

> /* Not Provable */

> ALL(a):[~a e n => ~Even(a)]
>

Some natural numbers are even, some are odd. Why would I want to prove that everything that is not a natural number is ODD? That's just silly. Why do you insist on using an unconventional definition that gives such obliviously wrong results that are so easy to avoid with a more conventional definition? Very crankish indeed, Jan Burse. Like your little buddy, the troll JG.

[Mostowski Collapse]

I do not want anything. You want something.
This is pretty standard:

Even = { a e n | a = 0 mod 2 }
Odd = { a e n | a = 1 mod 2 }

Everything else is plain crazy and simply wrong. You
dont find something else in math books

or that Euclid would have said something else.

[Mostowski Collapse]

With the below standard definition you can prove
everything, that you cannot prove with your Dan
Christensen nonsense. Examples that become provable

not using the Dan Christensen nonsense:

ALL(a):[~a in n => ~Even(a)]
ALL(a):[~a in n => ~Odd(a)]
ALL(a):[a e n <=> [Even(a) v Odd(a)]]
ALL(a):[a e {} <=> [Even(a) & Odd(a)]]
Etc…

On the other hand with your syphilitic brain definition
one cannot prove these things, one is bugged with
dark elements. If you want you can be also

more specific and distinguish:

EvenN = { a e n | a = 0 mod 2 }
OddN = { a e n | a = 1 mod 2 }
EvenZ = { a e n | a = 0 mod 2 }
OddZ = { a e n | a = 1 mod 2 }

This is in case you have an application where you
also want to have a notion of odd/even integer.
Or some other EvenX/OddX. But to have a well

defined definition you need to specific.

https://en.m.wikipedia.org/wiki/Well-defined

[Mostowski Collapse]

Corr.: Typo

EvenN = { a e n | a = 0 mod 2 }
OddN = { a e n | a = 1 mod 2 }

EvenZ = { a e z | a = 0 mod 2 }
OddZ = { a e z | a = 1 mod 2 }

This is in case you have an application where you
also want to have a notion of odd/even integer.
Or some other EvenX/OddX. But to have a well

defined definition you need to be specific.

https://en.m.wikipedia.org/wiki/Well-defined

[Dan Christensen]

On Wednesday, May 11, 2022 at 2:34:13 PM UTC-4, Mostowski Collapse wrote:
> I do not want anything. You want something.
> This is pretty standard:
> Even = { a e n | a = 0 mod 2 }
> Odd = { a e n | a = 1 mod 2 }

At least you are no longer claiming everything that isn't a natural number is odd. Nice climbdown. Don't you feel silly now?

> Everything else is plain crazy and simply wrong.

As I have written repeatedly here, you can define the predicates Even and Odd in a meaningful way as follows:

1. ALL(a):[a in N => [Even(a) <=> EXIST(b):[b in N & a=2*b]]]
2. ALL(a):[Odd(a) <=> ~Even(a)] (an abbreviation)


Notice that, here, we can establish the truth value of Even(x) only if x is a natural number. And we can establish the truth value of Odd(x) only if we first establish the truth value of Even(x).

I hope this helps.

[Mostowski Collapse]

You cannot use these axioms:

1. ALL(a):[a in N => [Even(a) <=> EXIST(b):[b in N & a=2*b]]]
2. ALL(a):[Odd(a) <=> ~Even(a)] (an abbreviation)

And then prove:

ALL(a):[~a in n => ~Even(a)]
ALL(a):[~a in n => ~Odd(a)]
ALL(a):[a e n <=> [Even(a) v Odd(a)]]
ALL(a):[a e {} <=> [Even(a) & Odd(a)]]
Etc…

Whats wrong with you? Are you dumb?

P.S.: On the other hand it works with:

Even = { a e n | a = 0 mod 2 }
Odd = { a e n | a = 1 mod 2 }

[Mostowski Collapse]

ALL(a):[a e {} <=> [Even(a) & Odd(a)]] is provable with
your definition, but the others are not:

Counter Models to Dans Definition:

ALL(a):[a in N => [Even(a) <=> EXIST(b):[b in N & a=2*b]]]

ALL(a):[Odd(a) <=> ~Even(a)] (an abbreviation)

Via https://www.umsu.de/trees:

Counter Model 1: Use 0=0,2,4,... , 1=1,3,4,..., 2=-1
(∃a(Na ∧ Ea) ∧ (∃a(Na ∧ Oa) ∧
(∀a(Na → (Ea ↔ Da)) ∧ ∀a(Oa ↔ ¬Ea)))) → ∀a(¬Na → ¬Ea) is invalid.
Domain: { 0, 1, 2}
N: { 0,1 }
E: { 0,2 }
O: { 1 }
D: { 0 }

Counter Model 2: Use 0=0,2,4,... , 1=1,3,4,..., 2=-1
(∃a(Na ∧ Ea) ∧ (∃a(Na ∧ Oa) ∧ (∀a(Na → (Ea ↔ Da)) ∧ ∀a(Oa ↔ ¬Ea)))) → ∀a(¬Na → ¬Oa) is invalid.
Countermodel:
Domain: { 0, 1, 2 }
N: { 0,1 }
E: { 0 }
O: { 1,2 }
D: { 0 }

Counter Model 3: Use 0=0,2,4,... , 1=1,3,4,..., 2=-1
(∃a(Na ∧ Ea) ∧ (∃a(Na ∧ Oa) ∧ (∀a(Na → (Ea ↔ Da)) ∧ ∀a(Oa ↔ ¬Ea)))) → ∀a(Na ↔ (Oa ∨ Ea)) is invalid.
Domain: { 0, 1, 2 }
N: { 0,1 }
E: { 0,2 }
O: { 1 }
D: { 0 }

[Mostowski Collapse]

On the other hand the standard definitions pass all
tests. When we use:

ALL(a):[Even(a) <=> a in N & EXIST(b):[b in N & a=2*b]]
ALL(a):[Odd(a) <=> a in N & ~EXIST(b):[b in N & a=2*b]]

Everything works fine.

Via https://www.umsu.de/trees:

(∀a(Ea ↔ (Na ∧ Da)) ∧ ∀a(Oa ↔ (Na ∧ ¬Da))) → ∀a(¬Na → ¬Ea) is valid.
(∀a(Ea ↔ (Na ∧ Da)) ∧ ∀a(Oa ↔ (Na ∧ ¬Da))) → ∀a(¬Na → ¬Oa) is valid.
(∀a(Ea ↔ (Na ∧ Da)) ∧ ∀a(Oa ↔ (Na ∧ ¬Da))) → ∀a(Na ↔ (Ea ∨ Oa)) is valid.

[Dan Christensen]

On Wednesday, May 11, 2022 at 4:09:16 PM UTC-4, Mostowski Collapse wrote:
> ALL(a):[a e {} <=> [Even(a) & Odd(a)]] is provable with
> your definition, but the others are not:
>
> Counter Models to Dans Definition:
> ALL(a):[a in N => [Even(a) <=> EXIST(b):[b in N & a=2*b]]]
> ALL(a):[Odd(a) <=> ~Even(a)] (an abbreviation)
> Via https://www.umsu.de/trees:
>
> Counter Model 1: Use 0=0,2,4,... , 1=1,3,4,..., 2=-1
> (∃a(Na ∧ Ea) ∧ (∃a(Na ∧ Oa) ∧
> (∀a(Na → (Ea ↔ Da)) ∧ ∀a(Oa ↔ ¬Ea)))) → ∀a(¬Na → ¬Ea) is invalid.
> Domain: { 0, 1, 2}
> N: { 0,1 }
> E: { 0,2 }
> O: { 1 }
> D: { 0 }
>

We are not talk about arbitrary sets and functions here, but specifically about the set of natural numbers N, and binary operations + and * on N. Sorry, not good enough, Jan Burse

We have:
E(0) is true since 0 = 2*0 ----> Odd(0) is false
E(1) is false since 1 =/=2*n ----> Odd(1) is true
E(2) is true since 2 = 2*1 ---->Odd(2) is false
E(3) is false since 3 =/= 2*n ---->Odd(3) is true
and so on

[Mostowski Collapse]

In the tree tool "Domain" = Unverse of Discourse.
All counter models make use of -1, since ~(-1 e n).

These 3 are not provable from your definition, but
they are provable from the standard definition:

∀a(¬Na → ¬Ea)
∀a(¬Na → ¬Oa)
∀a(Na ↔ (Ea ∨ Oa))

Legend:
Na = a e n
Ea = Even(a)
Oa = Odd(a)

See countermodels here to your definition:

Counter Model 1:

(∀a(Na → (Ea ↔ Da)) ∧ ∀a(Oa ↔ ¬Ea)))) → ∀a(¬Na → ¬Ea) is invalid.

Universe of Discourse: { 0,2,4,..., 1,3,4,..., -1}
N: { 0,2,4,..., 1,3,4,... }
E: { 0,2,4,..., -1 }
O: { 1,3,4,... }
D: { 0,2,4,... }

Counter Model 2: similar
Counter Model 3: similar

[Mostowski Collapse]

Do you have problems with vacuously true again.
Confusing it with vacuously false?

If you deny that they are not provable, then
please show us a proof of the following:

∀a(¬Na → ¬Ea)
∀a(¬Na → ¬Oa)
∀a(Na ↔ (Ea ∨ Oa))

From your nonsense:

∀a(Na → (Ea ↔ Da)) ∧ ∀a(Oa ↔ ¬Ea)

Legend:
Da = EXIST(b):[b in N & a=2*b]

[Dan Christensen]

On Wednesday, May 11, 2022 at 5:58:33 PM UTC-4, Mostowski Collapse (aka Jan Burse) wrote:

> Dan Christensen schrieb am Mittwoch, 11. Mai 2022 um 23:42:02 UTC+2:
> > On Wednesday, May 11, 2022 at 4:09:16 PM UTC-4, Mostowski Collapse wrote:
> > > ALL(a):[a e {} <=> [Even(a) & Odd(a)]] is provable with
> > > your definition, but the others are not:
> > >
> > > Counter Models to Dans Definition:
> > > ALL(a):[a in N => [Even(a) <=> EXIST(b):[b in N & a=2*b]]]
> > > ALL(a):[Odd(a) <=> ~Even(a)] (an abbreviation)
> > > Via https://www.umsu.de/trees:
> > >
> > > Counter Model 1: Use 0=0,2,4,... , 1=1,3,4,..., 2=-1
> > > (∃a(Na ∧ Ea) ∧ (∃a(Na ∧ Oa) ∧
> > > (∀a(Na → (Ea ↔ Da)) ∧ ∀a(Oa ↔ ¬Ea)))) → ∀a(¬Na → ¬Ea) is invalid.
> > > Domain: { 0, 1, 2}
> > > N: { 0,1 }
> > > E: { 0,2 }
> > > O: { 1 }
> > > D: { 0 }
> > >
> > We are not talk about arbitrary sets and functions here, but specifically about the set of natural numbers N, and binary operations + and * on N. Sorry, not good enough, Jan Burse
> >
> > We have:
> > E(0) is true since 0 = 2*0 ----> Odd(0) is false
> > E(1) is false since 1 =/=2*n ----> Odd(1) is true
> > E(2) is true since 2 = 2*1 ---->Odd(2) is false
> > E(3) is false since 3 =/= 2*n ---->Odd(3) is true
> > and so on

> In the tree tool "Domain" = Unverse of Discourse.
> All counter models make use of -1, since ~(-1 e n).
>

You really don't get it, do you, Jan Burse? It only has to be true for the set of natural numbers N and for addition and multiplication on N. Concoct all the "counter-models" you want. It doesn't matter in this case.

[Mostowski Collapse]

I only show you a difference between these two
definitions, namely:

Case 1: Dan Christensens Nonsense

∀a(Na → (Ea ↔ Da)) ∧ ∀a(Oa ↔ ¬Ea)

Case 2: Standard Definition

∀a(Ea ↔ (Na ∧ Da)) ∧ ∀a(Oa ↔ (Na ∧ ¬Da))

The difference is that Case 1 cannot prove the
below formulas, whereas Case 2 can prove the
below formulas:

∀a(¬Na → ¬Ea)
∀a(¬Na → ¬Oa)
∀a(Na ↔ (Ea ∨ Oa))

Thats pretty obvious, isn't it?

[Mostowski Collapse]

This one is also a lackmus formula, not provable
from Case 1 but provable from Case 2:

∀a(Oa ↔ Na ∧ ¬Ea)

The formula is provable from the standard:

Even = { a e n | a = 0 mod 2 }
Odd = { a e n | a = 1 mod 2 }

But not from Dan Christensens nonsense.

LMAO!

[Dan Christensen]

> I only show you a difference between these two
> definitions, namely:
>
> Case 1: Dan Christensens Nonsense
> ∀a(Na → (Ea ↔ Da)) ∧ ∀a(Oa ↔ ¬Ea)

It works with no wonky results. Actually more like the standard definition.

> Case 2: Standard Definition
> ∀a(Ea ↔ (Na ∧ Da)) ∧ ∀a(Oa ↔ (Na ∧ ¬Da))

> The difference is that Case 1 cannot prove the
> below formulas, whereas Case 2 can prove the
> below formulas:
> ∀a(¬Na → ¬Ea)

Wonky.

> ∀a(¬Na → ¬Oa)

More wonky still!

So, everything that is isn't a natural number is both not even and not odd. How wonky is that? Better to restrict your attention to just the natural numbers in this case. Forget your "dark elements." They really are a non-starter.

> ∀a(Na ↔ (Ea ∨ Oa))
> Thats pretty obvious, isn't it?

Actually quite wonky. Deal with it. Just admit you were wrong and ditch your wonky definition. You are looking like a complete idiot here, Jan Burse. A true crank.

[Mostowski Collapse]

These formulas, the lackmus formulas, are all derivable

∀a(¬Na → ¬Ea)
∀a(¬Na → ¬Oa)
∀a(Na ↔ (Ea ∨ Oa))

∀a(Oa ↔ Na ∧ ¬Ea)

from the standard:

Even = { a e n | a = 0 mod 2 }
Odd = { a e n | a = 1 mod 2 }

Calling the lackmus formulas wonky makes you a crank!
Congratulatiuons your syphilis pays off.

LMAO!

[Mostowski Collapse]

Last time I mentioned the standard you wrote:

> > Even = { a e n | a = 0 mod 2 }
> > Odd = { a e n | a = 1 mod 2 }
>

> At least you are no longer claiming everything that isn't a natural number is odd. Nice climbdown.

You are quite a nut-head. I was always promoting
the standard, there was no climb down. The
standard is this form:

Case 2:

∀a(Ea ↔ (Na ∧ Da)) ∧ ∀a(Oa ↔ (Na ∧ ¬Da))

But you can also write it with non-naive set builder,
its the same thing. Whats wrong with you? Your definition
is not the standard. Its just some nonsense that

you made up. Some nonsense that has no inferential
power, since it is not well defined:

https://en.wikipedia.org/wiki/Well-defined_expression

That it doesn't have inferential power, and promotes
dark elements is seen in that your nonsense cannot
prove the following, because of your idiotic dark matter:

∀a(¬Na → ¬Ea)
∀a(¬Na → ¬Oa)
∀a(Na ↔ (Ea ∨ Oa))
∀a(Oa ↔ Na ∧ ¬Ea)

LoL

[Mostowski Collapse]

Yes Dan Christensen ultra moron you got it, almost:

Dan Christensen schrieb am Donnerstag, 12. Mai 2022 um 00:35:26 UTC+2:
> So, everything that is isn't a natural number is both
not even and not odd. How wonky is that?

https://groups.google.com/g/sci.logic/c/gV50jEU6fvQ/m/ASEgcINuAQAJ

Just spell it out correctly, or are you linguistically impaired?

everything that is isn't a natural number is both
not an even natural number and not an odd natural number .

[Dan Christensen]

On Wednesday, May 11, 2022 at 6:46:10 PM UTC-4, Mostowski Collapse wrote:
> Last time I mentioned the standard you wrote:
>
> > > Even = { a e n | a = 0 mod 2 }
> > > Odd = { a e n | a = 1 mod 2 }
> >

This defines two subsets of N, not two predicates. Subsets =/= predicates. (See Russell's Paradox) Try again, Jan Burse,

[Mostowski Collapse]

Its the same like this, provably:

Case 2:
∀a(Ea ↔ (Na ∧ Da)) ∧ ∀a(Oa ↔ (Na ∧ ¬Da))

Whats wrong with you?

BTW: Do you also claim that this is wonky:

Every one that isn't a russian is neither a femal russian
nor a male russian.

[Mostowski Collapse]

Hey Snail brain!!!!

I explained a million times that Even(a) and a e even are the same.
I explained this in this thread. I posted about this already a million
time. I explained that we can prove in set theory:

/* Existence of the Set */
EXIST(even):ALL(a):[a e even <=> a e n & EXIST(b):[b e n & a=b+b]]

And we can also prove that this here:

ALL(a):[a e even <=> a e n & EXIST(b):[b e n & a=b+b]]
ALL(a):[Even(a) <=> a e n & EXIST(b):[b e n & a=b+b]]

Implies this here, same can be done for odd and Odd:

ALL(a):[a e even <=> Even(a)]

Why do you have a Snail brain?

[Mostowski Collapse]

Another way to write this here:

ALL(a):[a e even <=> a e n & EXIST(b):[b e n & a=b+b]]

Is to write it like this:

Even = { a e n | a = 0 mod 2 }

Do you deny that as well?

[Dan Christensen]

On Wednesday, May 11, 2022 at 7:08:58 PM UTC-4, Mostowski Collapse wrote:
> Hey Snail brain!!!!
>
> I explained a million times that Even(a) and a e even are the same.
> I explained this in this thread. I posted about this already a million
> time. I explained that we can prove in set theory:
>
> /* Existence of the Set */
> EXIST(even):ALL(a):[a e even <=> a e n & EXIST(b):[b e n & a=b+b]]
>

You got your butt kicked on defining wonky predicates. Now you want to change the subject and talk about subsets. Can't blame you, I guess. Go ahead and talk about sets then. Maybe you should forget about predicates. They seem to be much trickier for you.

[Mostowski Collapse]

Euclid did not have sets. I dont need sets. I only used
sets to illustrate what Euclid says, since you seem not
to understand Euclid. I posted Euclid alreay 10.05.2022.

Now we have 12.05.2022. In as far I nowhere claimed:

Dan Christensen schrieb am Donnerstag, 12. Mai 2022 um 00:35:26 UTC+2:

> So, everything that is isn't a natural number is both
not even and not odd. How wonky is that?

https://groups.google.com/g/sci.logic/c/gV50jEU6fvQ/m/ASEgcINuAQAJ

The formulas say something else. They say the following:

„everything that isn't a natural number is neither an
even number nor an odd number.“

Why? Because Euclid doesnt define even and odd. He defined
even number and odd number:

Mostowski Collapse schrieb am Dienstag, 10. Mai 2022 um 09:06:22 UTC+2:
> You can check yourself Euclid:

> 6. An even number** is that which is divisible into two equal parts.

> 7. An odd number is that which is not divisible into two equal parts,
> or that which differs by a unit from an even number.
> http://aleph0.clarku.edu/~djoyce/elements/bookVII/defVII6.html

https://groups.google.com/g/sci.logic/c/gV50jEU6fvQ/m/_8qYXngcAgAJ

I told this already 2 days ago. You still dont have the slightest
clue. You are simply bat shit crazy and high as a kite.

Go see a doctor.

[Mostowski Collapse]

The truth of these formulas is 1% mathematics and 99% common
terminological reasoning. The formulas have the same truth as this:

„everything that isn't a russian is neither a
female russian nor a male russian“

Its the same terminological reasoning here:

„everything that isn't a natural number is neither an

even natural number nor an odd natural number.“

Still the magatron jerk that goes by the name Dan Christensen spents
2 days and after that time, he hasnt yet the slightest clue. This is

truly some archivement in the domain of being densly stupid.

[Dan Christensen]

On Monday, May 9, 2022 at 12:11:47 AM UTC-4, Dan Christensen wrote:
> Here I consider two different ways to formally define a predicate, say the predicate Even(x) which is to be interpreted as "x is even."
>
> CASE 1
>
> ALL(a):[a in n => [Even(a) <=> EXIST(b):[b in n & a=2*b]]]
>
> CASE 2
>
> ALL(a):[Even(a) <=> a in n & EXIST(b):[b in n & a=2*b]
>
> (In both cases, n = the set of natural numbers.)
>
[snip]

We have more or less settled on Case 1 as the better definition of the two. Case 2, as it turned out, has too many annoying little "issues." (See "discussion.")

DEFINITION

For any natural number x, we say that x is even if and only if there exists a natural number y such that x = 2*y.

ALL(a):[a in n => [Even(a) <=> EXIST(b):[b in n & a=2*b]]]

ABBREVIATION

x is said to be odd if and only if x is not even.

ALL(a):[Odd(a) <=> ~Even(a).

**********************************************************************************************************************

Here, we use DC Proof 2.0 to prove: ALL(a):[a in n => [Even(a) | Odd(a)] & ~[Even(a) & Odd(a)]]

Where '|' is the OR-operator

Define: Even( )

1. ALL(a):[a in n => [Even(a) <=> EXIST(b):[b in n & a=2*b]]]
Axiom

Define: Odd( )

2. ALL(a):[Odd(a) <=> ~Even(a)]

Axiom


Prove: ALL(a):[a in n => [Even(a) | Odd(a)] & ~[Even(a) & Odd(a)]]

Suppose...

3. x in n
Premise

4. Odd(x) <=> ~Even(x)
U Spec, 2

5. [Odd(x) => ~Even(x)] & [~Even(x) => Odd(x)]
Iff-And, 4

6. Odd(x) => ~Even(x)
Split, 5

7. ~Even(x) => Odd(x)
Split, 5

8. ~~Even(x) | Odd(x)
Imply-Or, 7

9. Even(x) | Odd(x)
Rem DNeg, 8


Prove: ~[Even(x) & Odd(x)]

Suppose to the contrary...

10. Even(x) & Odd(x)
Premise

11. Even(x)
Split, 10

12. Odd(x)
Split, 10

13. ~Even(x)
Detach, 6, 12

14. Even(x) & ~Even(x)
Join, 11, 13

As Required:

15. ~[Even(x) & Odd(x)]
Conclusion, 10

16. [Even(x) | Odd(x)] & ~[Even(x) & Odd(x)]
Join, 9, 15

As Required:

17. ALL(a):[a in n => [Even(a) | Odd(a)] & ~[Even(a) & Odd(a)]]
Conclusion, 3

[Mostowski Collapse]

When you are an ultra moron as you are you, that cannot
keep track of context, you should not use the same predicate
name in the same context as you do here:

Dan Christensen schrieb am Donnerstag, 12. Mai 2022 um 04:08:02 UTC+2:
> > CASE 1
> > ALL(a):[a in n => [Even(a) <=> EXIST(b):[b in n & a=2*b]]]
> > CASE 2
> > ALL(a):[Even(a) <=> a in n & EXIST(b):[b in n & a=2*b]

Better introduce two different predicate names, like here:

CASE 1
ALL(a):[a in n => [Evenness(a) <=> EXIST(b):[b in n & a=2*b]]]
CASE 2
ALL(a):[Evennumber(a) <=> a in n & EXIST(b):[b in n & a=2*b]

Then its easy to see that you didn't find any lackmus
formula, we have of course these two theorems:

ALL(a):[a in n => [Eveness(a) | Oddess(a)] &
~[Eveness(a) & Oddness(a)]]

ALL(a):[a in n => [Evennumber(a) | Oddnumber(a)] &
~[Evennumber(a) & Oddnumber(a)]]

You didn't find a lackmus formula. Try harder jerk.

Dan Christensen schrieb:

[Mostowski Collapse]

Some Lackmuss Formulas are these.
This here is not provable:

|/- ALL(a):[~a e n => ~Evenness(a)]
|/- ALL(a):[~a e n => ~Oddness(a)]
|/- ALL(a):[a e n <=> Evenness(a) v Oddness(a)]
|/- ALL(a):[Oddness(a) <=> a e n & ~Evenness(a)]

On the other hand this is provable:

|- ALL(a):[~a e n => ~Evennumber(a)]
|- ALL(a):[~a e n => ~Oddnumber(a)]
|- ALL(a):[a e n <=> Evennumber(a) v Oddnumber(a)]
|- ALL(a):[Oddnumber(a) <=> a e n & ~Evennumber(a)]

Mostowski Collapse schrieb:

[Mostowski Collapse]

Corr:

When you are an ultra moron as you are you, that cannot
keep track of context, you should not use the same predicate

name in different contexts as you do here:

Mostowski Collapse schrieb:

[Dan Christensen]

> When you are an ultra moron as you are you,

Yikes! Looks like Jan Burse is still pissed that his favourite wasn't picked. A very sore loser. (Hee, hee!)

that cannot
> keep track of context, you should not use the same predicate
> name in the same context as you do here:
> Dan Christensen schrieb am Donnerstag, 12. Mai 2022 um 04:08:02 UTC+2:
> > > CASE 1
> > > ALL(a):[a in n => [Even(a) <=> EXIST(b):[b in n & a=2*b]]]
> > > CASE 2
> > > ALL(a):[Even(a) <=> a in n & EXIST(b):[b in n & a=2*b]
> Better introduce two different predicate names, like here:
>
> CASE 1
> ALL(a):[a in n => [Evenness(a) <=> EXIST(b):[b in n & a=2*b]]]
> CASE 2
> ALL(a):[Evennumber(a) <=> a in n & EXIST(b):[b in n & a=2*b]
>
> Then its easy to see that you didn't find any lackmus
> formula, we have of course these two theorems:
>
> ALL(a):[a in n => [Eveness(a) | Oddess(a)] &
> ~[Eveness(a) & Oddness(a)]]
>
> ALL(a):[a in n => [Evennumber(a) | Oddnumber(a)] &
> ~[Evennumber(a) & Oddnumber(a)]]
>
> You didn't find a lackmus formula. Try harder jerk.

Poor Jan Burse was never one to do things the easy way, or to admit he was wrong no matter how minor the point.

Dan

[Dan Christensen]

On Wednesday, May 11, 2022 at 10:35:23 PM UTC-4, Mostowski Collapse wrote:
> Some Lackmuss Formulas are these.
> This here is not provable:
>

And a good thing, too!

> |/- ALL(a):[~a e n => ~Evenness(a)]

[snip more of the same]

In the easy-to-use, conventional definition, the truth value of Even(x) can only be determined for x in N (the natural numbers). But Jan Burse insists that he be able to determine this truth value for EVERY object in the universe (his "dark elements"). Really!

[Mostowski Collapse]

Well for Euclids predicates Evennumber this is provable:
|- ALL(a):[~a e n => ~Evennumber(a)]

On the other hand for Dan Christensens Evenness you cannot prove it,

|/- ALL(a):[~a e n => ~Evenness(a)]

there is an obstancle in the way,
the Dan Christensens definitions are not well defined:

"In mathematics, a well-defined expression or unambiguous expression
is an expression whose definition assigns it a unique interpretation or value."
https://en.wikipedia.org/wiki/Well-defined_expression

If you do the following for Dan Christensens definitions, make it twice:

ALL(a):[a in n => [Evenness1(a) <=> EXIST(b):[b in n & a=2*b]]]
ALL(a):[a in n => [Evenness2(a) <=> EXIST(b):[b in n & a=2*b]]]

For Dan Christensens one cannot prove:
|/- ALL(a):[Evenness1(a) <=> Evenness2(a)]

On the other hand for Euclids one can prove:
|- ALL(a):[Evennumber1(a) <=> Evennumber2(a)]

See the difference dumbo?

[Dan Christensen]

You are simply grasping at straws, Jan Burse. Is this really why you think we must determine the truth value of Even(x) for every object x in the universe, Jan??? . (HA, HA, HA!!!)

Dan

[Mostowski Collapse]

The thread title says two ways to formally define a predicate.
Your case 1 is not a definition because it is not well defined:

"In mathematics, a well-defined expression or unambiguous
expression is an expression whose definition assigns it a
unique interpretation or value."
https://en.wikipedia.org/wiki/Well-defined_expression

Something counts only a definition when it is well-defined.
You can make well-defined definitions either:
- Explicitly, by using the form ALL(...)(P(...) <=> ...)
- Implicitly, by using another form

In either case it must be well defined. Your case 1 is
not well defined, because from:

ALL(a):[a in n => [Evenness1(a) <=> EXIST(b):[b in n & a=2*b]]]
ALL(a):[a in n => [Evenness2(a) <=> EXIST(b):[b in n & a=2*b]]]

You cannot prove:

|/- ALL(a):[Evenness1(a) <=> Evenness2(a)]

So its not a definition. Only an axiom with where Evenness appears.
It doesn't define Evenness. This also explains why you cannot
prove ordinary stuff, that can be proved with the

well defined definition of Evennumber.

Dan Christensen schrieb:

> Here I consider two different ways to formally define a predicate, say the predicate Even(x) which is to be interpreted as "x is even."
>
> CASE 1
>
> ALL(a):[a in n => [Even(a) <=> EXIST(b):[b in n & a=2*b]]]
>
> CASE 2
>
> ALL(a):[Even(a) <=> a in n & EXIST(b):[b in n & a=2*b]
>
> (In both cases, n = the set of natural numbers.)
>

> There is a subtle difference in outcomes. Even(1) will be FALSE in both cases. Even(-1), however, will be UNDEFINED in case 1, but FALSE in case 2.
>
> Your comments?

[Mostowski Collapse]

The approach here:

is called Alessandro Padoas logical criterion for definability,
checking this here, which Dan Christensens fails:

/* Doesn't work for Dan Christensens Case 1 */

ALL(a):[a in n => [Evenness1(a) <=> EXIST(b):[b in n & a=2*b]]]
ALL(a):[a in n => [Evenness2(a) <=> EXIST(b):[b in n & a=2*b]]]

=> ALL(a):[Evenness1(a) <=> Evenness2(a)]

There is also a theorem by Evert Willem Beth, that relates
explicit and implicit definability, so that case 1, Dan
Christensens Evennesss, does not have the form:
ALL(...)[P(...) <=> ...]

Is not really the problem. The problem is that it fails
the well definedness test, so its

not a definition only an axiom.

Mostowski Collapse schrieb:

[Dan Christensen]

On Thursday, May 12, 2022 at 9:03:55 AM UTC-4, Mostowski Collapse wrote:
> The thread title says two ways to formally define a predicate.
> Your case 1 is not a definition because it is not well defined:
> "In mathematics, a well-defined expression or unambiguous
> expression is an expression whose definition assigns it a
> unique interpretation or value."

That doesn't mean that the notion of evenness must be determined for every object in the universe. It only needs to be determined for the natural numbers. Get a life, Jan Burse.

[Mostowski Collapse]

If it is not determined, it is not well defined.
BTW: Some Sigmund Freud found this definition:

ALL(a):[Wonky(a) <=> ~Danish(a)]

This means that practically all of mathematics
is wonky, because Dan Christensen doesn't

have the slightest clue...

[Mostowski Collapse]

If you cannot prove:

/* Doesn't work for Dan Christensens Case 1 */

ALL(a):[a in n => [Evenness1(a) <=> EXIST(b):[b in n & a=2*b]]]
ALL(a):[a in n => [Evenness2(a) <=> EXIST(b):[b in n & a=2*b]]]

=> ALL(a):[Evenness1(a) <=> Evenness2(a)]

Then Evenness is not self synonymous. And therefore
it is not well defined. And therefore its not a definition.

[Mostowski Collapse]

If it is not self synonymous, this means it has a lot
of dark elements. Basically it means, you have extended
your practice of poop mathematics to:
- Half-Predicates
- Black Hole Properties
- Non-Definition Definitions
- Ask the Chrystal Ball Axioms
- More Ad-Hoc Axioms Boom Boom
- I am gonna ignore Euclid mathematics
- Wonky is the new Black
-

Mostowski Collapse schrieb:

[Dan Christensen]

On Thursday, May 12, 2022 at 9:33:25 AM UTC-4, Mostowski Collapse (aka Jan Burse) wrote:

> Dan Christensen schrieb am Donnerstag, 12. Mai 2022 um 15:28:01 UTC+2:
> > On Thursday, May 12, 2022 at 9:03:55 AM UTC-4, Mostowski Collapse wrote:
> > > The thread title says two ways to formally define a predicate.
> > > Your case 1 is not a definition because it is not well defined:
> > > "In mathematics, a well-defined expression or unambiguous
> > > expression is an expression whose definition assigns it a
> > > unique interpretation or value."
> > That doesn't mean that the notion of evenness must be determined for every object in the universe. It only needs to be determined for the natural numbers. Get a life, Jan Burse.

> If it is not determined, it is not well defined.

Maybe you didn't know, but evenness is determined and well defined for every natural number. Deal with it, Jan Burse. We have no need of your wonky definition.

[Mostowski Collapse]

You didn't prove:

ALL(a):[Even'(a) <=> Even(a)]

Anyway, you are allowed to do whatever you want.
Only your nonsense is not a definition, only an axiom.

[Dan Christensen]

On Thursday, May 12, 2022 at 11:17:43 AM UTC-4, Mostowski Collapse wrote:
> You didn't prove:
>
> ALL(a):[Even'(a) <=> Even(a)]
>

Since we need only consider the natural numbers when determining evenness, it is sufficient prove:

ALL(a):[a in N => [Even'(a) <=> Even(a)]]]

Trivial in DC Proof give the proper definition of Even( ).

[Mostowski Collapse]

A definition needs to be well defined:

In mathematics, a well-defined expression or unambiguous
expression is an expression whose definition assigns
it a unique interpretation or value.

https://en.wikipedia.org/wiki/Well-defined_expression

You can even not exclude s(-1)=0 in your Peano Axioms,
since even your Peano Axioms are not well defined
concerning the function s, its not a Successor,

you should call it Successness:

/* Dans Successness, is not a Successor */
s(-1) = 0

because you always use turd mathematics.

[Mostowski Collapse]

In a few days the bat shit crazy and high as a kite
Dan Christensen, went from this being consistent
(has a model) with his Peano Axiom Successness:

s(-1) = 0

To this being consistent (has a model) with
his freaking carzy bullshit Evenness axiom,
which is not a definition:

even(-1)

Bravo, you are surely the ultimate crank.

[Dan Christensen]

On Thursday, May 12, 2022 at 11:26:45 AM UTC-4, Mostowski Collapse wrote:
> A definition needs to be well defined:
> In mathematics, a well-defined expression or unambiguous
> expression is an expression whose definition assigns
> it a unique interpretation or value.
> https://en.wikipedia.org/wiki/Well-defined_expression
>

Nothing ambiguous about: ALL(a):[a in N => [Even(a) <=> EXIST(b):[b in N & a=2*b]]]

> You can even not exclude s(-1)=0 in your Peano Axioms,

Maybe you didn't know, but Peano's Axioms state that 0 has no pre-image under the successor function. Really. (Line 5)

1. Set(n)
Axiom

2. 0 in n
Axiom

3. ALL(a):[a in n => s(a) in n]
Axiom

4. ALL(a):ALL(b):[a in n & b in n => [s(a)=s(b) => a=b]]
Axiom

5. ALL(a):[a in n => ~s(a)=0] <------------- HERE
Axiom

6. ALL(a):[Set(a) & ALL(b):[b in a => b in n]
=> [0 in a & ALL(b):[b in a => s(b) in a]
=> ALL(b):[b in n => b in a]]]
Axiom

> since even your Peano Axioms are not well defined
> concerning the function s, its not a Successor,
>

Nothing ambiguous about a Peano system. In fact, every Peano system is essentially the same structure, the only difference being possibly different names assigned to it various parts. (See my previous postings here on this topic.)

[Mostowski Collapse]

Because of your bat shit crazy stuff, you cannot prove:

/* Not Provable in the Dan Christensen Approach */
ALL(a):[Evenness(a) => Oddness(Successness(a))]

Whereas with Euclid we can prove:

/* Pretty much standard for everybody from math */
ALL(a):[Evennumber(a) => Oddnumber(Successor(a))]

[Mostowski Collapse]

So the non-standard nonsense by Dan Christensen is
totally useless. What every mathematician expects:

/* provable */
|- ALL(a):[Evennumber(a) => Oddnumber(Successor(a))]

Is depreved by Dan Christensens poop 💩 mathematics:

/* not provable */
|/- ALL(a):[Evenness(a) => Oddness(Successness(a))]

He even managed to botch the Peano axioms. To show
its not provable counter model Evenness(-1) and
Successness(-1)=0 is enougg.

[Dan Christensen]

On Thursday, May 12, 2022 at 11:55:06 AM UTC-4, Mostowski Collapse wrote:
> Because of your bat shit crazy stuff, you cannot prove:
>
> /* Not Provable in the Dan Christensen Approach */
> ALL(a):[Evenness(a) => Oddness(Successness(a))]
>

Let's see your proof of this using your wonky definition, Jan Burse.

Dan

[Mostowski Collapse]

Why proof, I wrote not provable. To show its not provable
counter model Evenness(-1) and Successness(-1)=0 is enough.

/* not provable */
|/- ALL(a):[Evenness(a) => Oddness(Successness(a))]

What do you want to prove crazy man? Do you mean
proving this here, it has Evennumber and not Evenness:

/* provable */
|- ALL(a):[Evennumber(a) => Oddnumber(Successor(a))]

And the theorem is part of Euclid explanations,
„differe by a unit from an even number“

Mostowski Collapse schrieb am Dienstag, 10. Mai 2022 um 09:06:22 UTC+2:
> You can check yourself Euclid:
> 6. An even number** is that which is divisible into two equal parts.
> 7. An odd number is that which is not divisible into two equal parts,
> or that which differs by a unit from an even number.
> http://aleph0.clarku.edu/~djoyce/elements/bookVII/defVII6.html
https://groups.google.com/g/sci.logic/c/gV50jEU6fvQ/m/_8qYXngcAgAJ

Do you say Euclid is not provable with Peano Axioms.
Maybe yes, if the Dan Christensens nonsense Peano is used.

[Dan Christensen]

On Thursday, May 12, 2022 at 12:49:56 PM UTC-4, Mostowski Collapse wrote:
> Why proof, I wrote not provable. To show its not provable
> counter model Evenness(-1) and Successness(-1)=0 is enough.

So, you cannot actually prove that Even(x) => Odd(x+1) with your wonky definition. Don't you find that problematic?

[Mostowski Collapse]

More complete interpretation of Euclid, not only
some „if“ direction, but the full „iff“ direction:

ALL(a):[Oddnumber(a) <=> EXIST(b):[Evennumber(b) & Successor(b)=a]]

[Mostowski Collapse]

This is not provable, Dan Christensens approach:

|/- ALL(a):[Oddness(a) <=> EXIST(b):[Evenness(b) & Successness(b)=a]]

This is provable, Euclids approach:

|- ALL(a):[Oddnumber(a) <=> EXIST(b):[Evennumber(b) & Successor(b)=a]]

[Mostowski Collapse]

The summer time sadness of Dan Christensen. He
cannot prove the following with his approach:

/* not provable */
|/- ALL(a):[Evenness(a) => Oddness(Successness(a))]

But dont be sad, you can still prove this here with
your approach, isn't this great?

/* provable */
|- ALL(a):[a e n => (Evenness(a) => Oddness(Successness(a)))]

Its stil a little vexing, since the unprovable formula
has the form ALL(_):[P(_) => ....] so according to
Dan Christensens rule of non-wonky formulas, it

should be non-wonky. But I guess ALL(_):[P(_) => ....]
alone does not help, P(_) needs to be also well defined,
to have more inferential punch. What is well defined?

"In mathematics, a well-defined expression or unambiguous
expression is an expression whose definition assigns it
a unique interpretation or value."
https://en.wikipedia.org/wiki/Well-defined_expression

[Dan Christensen]

On Thursday, May 12, 2022 at 4:30:48 PM UTC-4, Mostowski Collapse wrote:
> The summer time sadness of Dan Christensen. He
> cannot prove the following with his approach:
> /* not provable */
> |/- ALL(a):[Evenness(a) => Oddness(Successness(a))]

If that is unprovable in your system, that "system" is really of no use.

> But dont be sad, you can still prove this here with
> your approach, isn't this great?
>
> /* provable */
> |- ALL(a):[a e n => (Evenness(a) => Oddness(Successness(a)))]
>

In the natural numbers, an odd number must always directly follow an even number. That is obviously a true statement, but that doesn't mean it is easy to prove.

[Mostowski Collapse]

You are a little confused, arent you? Its unprovable in DC
Proof. This cannot be proved with your, Dans, Peano Axioms
and your, Dans, proposal of x is even:

/* not provable */
|/- ALL(a):[Evenness(a) => Oddness(Successness(a))]

Here is remainder of the naming that I am using:

Evenness: Yours, Dans
Oddness: Yours, Dans
Sucessnesss: Yours, Dans

Nothing to do with another system such as Euclids. In
Euclids, the names are different, there we have Evennumber,
Oddnumber and Sucessor. In Euclid its provable.

Whats wrong with you? I always wrote its not provable in Dans.

[Mostowski Collapse]

Here is the naming again:

Evenness: Yours, Dans
Oddness: Yours, Dans
Sucessnesss: Yours, Dans

Evennumber: Euclids
Oddnumber: Euclids
Successor: Euclids

It is not provable in yours, Dans, because for example,
this is not excluded, i.e. a counter model can be made:

Evenness(-1) /* possible */
Sucessness(-1)=0 /* possible */

On the other hand in Euclids, the same counter model does not
work, since Evennumber is more determined, for ~(-1 e n):

~Evennumber(-1) /* always */