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