« first day (12 days earlier)      last day (278 days later) » 

Secret
Secret
10:57 AM
Refined axioms of finite naturals:
1. There is a maximum, defined to be the unique number that has no successor, and a minimum, defined to be the unique number that has no predecessor.
2. Every number is a successor of some number, except the minimum
3. Every number is either a successor or the minimum, and between any two successor there are no numbers
4. No number can have a sequence of predecessor (if any) that continues indefinitely
1. $\exists! y[S(y)=\bot] \land \exists! a \not \exists b[S(b)=a]$
2. $\forall (n \neq a) \exists m[S(m)=n]$
→ 1 message moved to trash
3. $\forall n[(n=a \lor \exists m [S(m)=n]) \land \not\exists k \forall(m,p)[S(m)<k<S(p)]]$
 
Secret
Secret
11:28 AM
[Restart]
1. There is a maximum, defined to be the unique number that has no successor, and a minimum, defined to be the unique number that has no predecessor.
2. Every number is a successor of some number, except the minimum
3. Every number is either a successor or the minimum, and between any two successor there are no numbers
4. No number can have a sequence of predecessor (if any) that continues indefinitely
5. Succession and predecession form a linear order
[Restart]
1. There is a maximum, defined to be the unique number that has no successor
2. There is a minimum, defined to be the unique number that has no predecessor
3. Every number is either a successor/predecessor, the minimum or the maximum.
4. Between any two successors there are no numbers.
5. Succession and predecession form an injective linear order.
[Restart]
1. There is a maximum, defined to be the unique number that has no successor.
2. There is a minimum, defined to be the unique number that has no predecessor.
3. Every number is either a successor/predecessor, the minimum or the maximum.
4. Between any two successors there are no numbers.
5. Every number except the minimum or maximum has both a unique successor and a unique predecessor.
6. The minimum has a unique successor, and the maximum has a unique predecessor.
1. $\not\exists n\exists! b[S(b)=n]$
2. $\not\exists! n\exists! t[S(n)=t]$
3. $\forall n\exists(a,c)\exists!(t,b)[[S(a)=n \land S(n)=c] \lor n=b \lor n=t]$
4. $\forall(a,c)\not\exists n[S(a)<n<S(c)]$
5. $\forall(n\neq b \lor n \neq t)\exists!(a,c)[S(a)=n \land S(n)=c]$
6. $\exists!(b,t,a,c)[S(b)=a \land S(c)=t]$
 
Secret
Secret
12:32 PM
0
Q: Experiment to probe the necessary and sufficient axioms to have a finite set in the same sense as finite sections of natural number in set theory

SecretRecently, I have been wondering how to define the restrictive notion of finite (i.e. the notion which in ZF a finite set $S$ will mean there exists a bijection between $S$ and an initial section of the naturals $\{0,1,2,3,4,...,n\}$) given any arbitrary foundation $F$ that only has (classical) lo...

elementary-number-theory foundations
 
 
2 hours later…
Secret
Secret
2:13 PM
Even after your changes, the only formal statement that means what I think you intend it to mean is 7. The issues aren't subtle (though many issues are caused by over-/mis-use of $\exists!$). For example, 4 basically says there are no numbers between any two (successors of) numbers. It would imply that there are no numbers between 3 and 7, for example. 1 is actually a logical contradiction. My advice is to worry about getting a better grasp on formal logic before worrying about this particular topic. Using a proof assistant or a model finder that can check your work may be helpful. — Derek Elkins 28 mins ago
 

« first day (12 days earlier)      last day (278 days later) »