« first day (1482 days earlier)      last day (1324 days later) » 

user21820
user21820
6:04 AM
@user76284 I believe it is very weak, like PA−. For comparison, PA+RCF, which I had called T in the preceding discussion, is exactly as strong as PA/ACA0, and SRA is exactly as strong as ACA. ACA0 interprets PA+RCF because you can interpret ℝ to be subsets of ℕ in ACA0 that encode a downward-closed subset of the fraction field F of ℕ that correspond to roots of odd-degree polynomials over F.
 
user21820
user21820
6:30 AM
I'm not sure how to prove that PA− interprets your theory, but I believe it is of that strength because you lack anything that can provide induction. You may also be interested to note that Internal Sup proves Induction over SRA minus Induction: 
First note that Internal Sup implies Internal Inf (every "≤" replaced by "≥").
Take any property Q on ℕ such that Q(0) and ∀k∈ℕ ( Q(k)⇒Q(k+1) ).
If ∃k∈ℕ ( ¬Q(k) ):
	Let c∈ℕ such that ¬Q(c) and let f = ( ℕ k ↦ Q(k) ? c : k ).
	Clearly f ≥ 0, so let m = inf(f).
	Then m∈ℕ because m ≤ ceil(m) ≤ f.
	Thus ¬Q(m) and so m > 0 since Q(0).
	Thus Q(m−1) because m−1 < inf(f).
	Thus Q(m) since ∀k∈ℕ ( Q(k)⇒Q(k+1) ).
	Contradiction.
@user76284: So it is a fun thing to develop real analysis within a theory that only has the ordered field axioms for ℝ plus a predicate to pick out ℕ plus comprehension axioms to construct sequences from ℚ (or ℝ, or equivalently subsets of ℕ), plus Internal Sup!
In particular, you might want to pick out ℤ instead of ℕ using 0∈ℤ ∧ ¬∃x∈ℤ ( 0<x<1 ) ∧ ∀x∈ℝ ( x∈ℤ ⇔ x+1∈ℤ ).
And then pick out ℕ by defining x∈ℕ ≡ x∈ℤ ∧ x≥0.
 
 
9 hours later…
user21820
user21820
3:54 PM
In mathematical practice, you do not need to know about ordinals, and actually all you need to know is the well-ordering theorem. It turns out that there is in fact a short proof of that theorem along the same lines as this short proof of Zorn's lemma: Take any set S. Let F be a choice-function that maps each strict subset A of S to a member of S not in A. We say that (T,<) is a tower iff T is a subset of S and < is a well-ordering of T and ∀x∈T ( x = F(T[<x]) ). Any two towers agree (i.e. one order-embeds into the other). Union all the towers. — user21820 1 min ago
 

« first day (1482 days earlier)      last day (1324 days later) »