Mathworks (Not the main chat!)

user21820

03:17

@Secret As @LeakyNun said, and neither is (∀a)(∀b)(a<b⇒a+b≤b) true.

Secret

10:52

Yeah right. Not sure how to quantify the condition though other than b is a limit ordinal or contains a limit ordinal > a

user21820

12:41

@Secret Didn't the very post you linked have an answer that gives you the condition (as per the remark in comment)?

@LeakyNun: Which also means, it should be in your axioms, right?

=P

Secret

13:49

if $\beta \ge \alpha\cdot \omega$, then $\alpha+\beta=\beta$

user21820

14:11

@Secret That's only half; read the remark.

Secret

I don't see how can one include an order isomorphism as something like an abstract algebra axiom (probably what he means by syntactic induction arguments I think...)

Edit: Delete "probably what he means by syntactic induction arguments I think..."

I mean, yes we can write the line : $\beta=\alpha\cdot\omega+\delta$, but the next step (which is to prove that there is an order isomorphism) I don't see how it can be axiomised despite the isomorphism can be explicitly wrote down

I also don't recall any axioms have the structure of proofs

Self-verifying theories

Self-verifying theories are consistent first-order systems of arithmetic much weaker than Peano arithmetic that are capable of proving their own consistency. Dan Willard was the first to investigate their properties, and he has described a family of such systems. According to Gödel's incompleteness theorem, these systems cannot contain the theory of Peano arithmetic, and in fact, not even the weak fragment of Robinson arithmetic; nonetheless, they can contain strong theorems. In outline, the key to Willard's construction of his system is to formalise enough of the Gödel machinery to talk about...

Something probably unrelated. I need to figure out how to squeeze more time to continue to read the book as otherwise I am just rambling

Secret

14:30

O wait a minute, I think I should be saying iff in the first line

Another bias of mine: When someone said I am missing half of the argument, I always think at least another sentence the same length as what I quote is missing

but in this case, half of the argument is missing because it is all condensed to that extra f I forgot to type

iff $\beta \ge \alpha\cdot \omega$, then $\alpha+\beta=\beta$

user21820

15:35

@Secret That's what I meant.

Well it's just that when we ask for when something happens, we almost always mean an iff condition. Normally we don't write "iff X then Y" so I really thought you didn't see Asaf's comment.

Self-verifying theories are interesting from the viewpoint of classical mathematics.

They however fail to actually self-verify in any philosophically meaningful sense, because we need to be in a sufficiently strong meta-system to even see that they prove something which can be taken to represent their own consistency.

And the fact that they can't reason about programs makes them weird.

Secret

One impression I had about strong meta systems is that while they can ground a lot more formulae, at the same time they reduce the scope of things they can apply on, and eventually become too localised

user21820

@Secret Of course. That's why we need to invoke philosophy to decide on a meaningful meta-system.

Otherwise we could easily end up with a meta-system that is unsound for reality in the sense that there is no real-world interpretation.

That would be useless. For example, if your meta-system is TC+¬Con(TC), then it is consistent (so we will never find a contradiction) but it proves that some explicit program halts (as in my post). If we are ignorant, we could very well believe that it is true, and run that program (it is quite short so it will fit on a real computer). It will never finish, yet we will never (in our meta-system) be able to know that.

The fact that we would be compelled by that unsound meta-system to accept the truth of some false claim, and yet be unable to find out in the real world that it is false, shows us that we ought to be extremely careful in designing our meta-system.

Secret

> and yet be unable to find out in the real world that it is false

that 's one of the scariest thing to me

user21820

That's why I don't buy ZFC.

On the other hand, we don't want to end up with a meta-system that can't prove things we can actually verify in the real world.

That's why in my opinion the ideal meta-system is going to be incomplete unless we reject the notion of natural numbers as an unbounded collection.

Secret

Btw, regarding ZFC, I was rambling in the Rambles recently as I tried to figure out how actual infinity and all those crazy infinite notions in ZF arises from considering potential infinity (and try to temporary purge myself from ZF knowledge to pretend I don't know anything except basic counting) and more importantly, to figure what is a minimalistic notion of infinities, and I realise I got stuck very easily

If one thing, infinity being so weird in modern mathematics seemed to heavily tied to the way ZF and set theory in general is structured. I am having more suspicion that perhaps a lo…

user21820

15:49

@Secret That is in fact true. A lot of 'facts' about infinity are actually artefacts of the foundational system.

Secret

Currently in my investigation, only potential infinity can be motivated, by considering the philosophical notion of something that goes forever.

But actual infinity is in some sense quite ad hoc

there is basically no reason in real life application for us to imagine something larger than anything we can access. Like why will we be interested in a notion of inaccessibility (that seemed to be the minimal requirement for something to be any of the large infinities)

user21820

@Secret That's why it is an artefact of the foundational system. Even ω[1] does not seem to make sense from a constructive point of view.

No need to go so far as inaccessibles.

ω[1] as a classical set, I mean.

Or as a von Neumann ordinal.

Countable ordinals as a type makes sense, in the same way natural numbers as a type makes sense. Namely whatever you can prove is a countable ordinal gets accepted into that type. Nothing ever gets rejected once it is accepted.

Secret

Well, leaky and I pretty much had a preliminary conclusion, that $\omega_1$ is already inaccessible in a sense no countable fundamental sequences or repetitions of it in any number of iterations below $\aleph_1$ itself can access it.

I am suspecting the thing that really characterise the notion of uncountability is "inaccessible from countably many steps" and in general a successor cardinal is basically "inaccessible from predecessor cardinal many steps"

Indeed, some of the rambles I made earlier (which I later deleted as Mathworks need major cleanup due to its unexpected gain in purpose)…

And in type theory, it is much simpler as you said, all countable ordinals are of the same type, done, nothing ambigurous about it

user21820

@Secret Well I don't know whether I linked you to the post I made on replacement:

1

A: Why is replacement true in the intuitive hierarchy of sets?

Suppose that as each stage $S$ is completed, we take each $y$ in $x$ which is formed at $S$ and complete the stage $S_y$. When we reach the stage at which $x$ is formed, we will have formed each $y$ in $x$ and hence completed each stage $S_y$ in $\mathbf S$. This is actually a circular justi...

My answer is actually the correct one, but as you can see people are afraid to face the truth. At least the logician Boolos was forthright about it.

Secret

That's a new post indeed. I am reading it now. Meanwhile I had some comments about asaf's:

But if you don't have $V_{\omega_1}$, how can you prove Borel determinacy? :( — Asaf Karagila Oct 18 '16 at 11:38

user21820

16:01

You can see that even granting the powerset and union capabilities, you can't get an uncountable number of stages, and so can't construct the stage in the cumulative hierarchy containing ω[1], without already having ω[1] to furnish you all the labels you need for your stages...

Boolos confirms my initial guess (in my original post before I found his remark) that V[ω[1]] forms a model of the iterative conception of sets.

Note that you still can construct the set of all countable well-orderings on N.

But you can't extract the canonical ordinal from this.

Secret

(cont.)
It is true we now knew how ad hoc $\omega_1$ is. The problem is what should we do to fix borel algebra since that thing defines measure theory and it turns out borel algebra is a set $G^{\omega_1}$

$\omega_1$ also appear in an important topological counterexample the long line. The nonexistence of $\omega_1$ means we need to figure out how to retain these important cases

Basically on those few days ago when I realise $\omega_1$ is so arbitrary, it seems a lot of things from measure theory will fall apart, and then question is then how to prevent is since measures are so important …

user21820

@Secret ω[1] is not important in the part of measure theory that is needed in the real world.

Are you surprised?

I know about the long line too, and it's true that ω[1] can be used in ZFC to do all sorts of interesting things. But at the end of the day I don't see any practical use.

47

Q: Physical meaning of the Lebesgue measure

Question (informal) Is there an empirically verifiable scientific experiment that can empirically confirm that the Lebesgue measure has physical meaning beyond what can be obtained using just the Jordan measure? Specifically, is there a Jordan non-measurable but Lebesgue-measurable subset of ...

Secret

@user21820 I think I am quite surprised, cause I do see it pop up in quite a lot of real analysis textbook where various closure properties of spaces were discussed

user21820

@Secret I'm quite sure most of them are about counter-examples to something.

@LeakyNun: By the way, if you read my post on replacement and find it okay, you could help to downvote the silly circular answer by the asker. It can't be removed by deletion.

Secret

The way I handle replacement nowadays is to ensure every function I use (unless I am explicitly using the axiom of choice for certain applications like Baire category theorem) can be wrote as a finite string of instructions so that the function becomes an algorithm that if plug into a computer, should compute its image as required

so perhaps I might be using the constructive or possibly predicative portion of replacement

user21820

16:13

Your programs include oracles?

If not even the halting problem is not accessible to you, and you don't even need any set theory; just PA will do.

Secret

No unless I need some important uncomputable reals

Yeah I think PA with its induction scheme will compute the image of those functions for me, I think that's how I think of them since I tend to treat functions as a list where inputs feed in and spits out a list

user21820

Well if you have finite Turing jumps, and consider every object as some description, then you can have replacement for functions on N, and you still won't get any weird things like ω[1].

Because countable stuff are closed under countable stuff anyway.

Secret

Indeed, and one of my rambles I deleted discussed that in a finite turing jump model, the collection of all ordinals will be $[0,\omega_{n+1}^{CK})$ which is powerful enough to do most analysis

user21820

Yes as I said earlier I'm sure that all applicable real analysis can be done in higher-order arithmetic (HOA), and virtually all in just ACA.

ACA has all finite jumps.

Secret

16:30

Another footnote about set theory: Even $\omega$ will become unreachable if axiom of infinity is not part of the default axioms of ZF (thus in such hypothetical scenario, one will need to introduce it as some models of ZF)

So in general, my conjecture is that actual infinities does not exists before they are being defined by axioms

→ 4 messages moved to Mathematics

@AsafKaragila: Yea but some people want AC, and hence can't have AD, even if AD is the natural generalized version of determinacy. So for them, my question is how they determine which determinacy is the 'right' one. In a sense, $ω_1$ and $ω_1^{CK}$ are like large cardinals, each in their own sense, the first from the constructive perspective and the second from the computability perspective. And just a while ago I was going to suggest some stronger iterative principle that might get us up to $V_{\beth_{ω_1}}$ but no further... — user21820 Oct 18 '16 at 13:53

Well, why not $V_{\beth_{\beth_{\omega_1}}}$? In fact, why not go all the way until the first fixed point? Or maybe the first fixed point which is a limit of fixed points? Or the first one which has a club of fixed points below it? Why not any of them? :P — Asaf Karagila Oct 18 '16 at 13:58

I think the more important question for people who are interested in a foundation of mathematics that models real world applicable modern mathematics and want to convince infinite set theorist is the following:

Ask them why we need a hierarchy of unreachable actual infinities in sequence and whether there are theorems that explicitly demand it with no alternatives

(The above is basically a very broad way of saying: Justify why we need uncountable well orderings and want these to be linearly ordered)

8

A: Bijection between closed uncountable subset of $\Bbb R$ and $\Bbb R$.

This is a nice result due to Cantor that is good to understand well. Let me expand André Nicolas's answer. We need a modicum of set theory, specifically, a working understanding of $\omega_1$, the first uncountable ordinal. 1. First, we need the Cantor-Baire stationary principle: Suppose tha...

hmm...

but then, the $n$-computable reals are dense but countable, so topology should not be broken when we took $\omega_1$ away from it

hmm...

Other things to think about: Non separable hilbert spaces. These don't have a countable hilbert basis. They arise in many areas in quantum mechanics and quantum field theory

so we need to investigate how will these hilbert space and their analysis changes when we replace the reals with the n-computable reals. If something too significant is lost and cannot be satisfactorily replaced, then it might justify we need some notion of uncountably. Will investigate this later

11

Q: Is there any physical system with a non-separable Hilbert space?

It seems that all the usual physical systems have a separable Hilbert space. Is there any example with a non-separable Hilbert space? BTW, I am actually always baffled by the fact that a continuous model like the 1d harmonic oscillator defined on $\mathbb{R}$ has a separable Hilbert space. It i...

quantum-mechanics mathematical-physics hilbert-space

Hmm... this is more complicated than I thought. It seems while QM and QFT will do fine by construction, some quantum gravity stuff and symmetry breaking phenomenon will run into problems. But I guess it is still too early and rare to consider them, I think...

user21820

17:06

Did you look at the linked post about the Lebesgue integral? Terence Tao's answer essentially shows that you need hardly anything to get the results that have real-world consequences.

That said, having the standard reals has nothing to do with ω[1].

Secret

Not yet, I just finished reading your reaplcement post

user21820

Just like V[ω[1]] has the set of countable well-orderings of N but does not have ω[1].

Secret

Actually I am thinking about something broader, not $\omega_1$: Throwing away powersets, since powersets are known to make things impredicative. This is why I talk about computable reals

user21820

When you throw away the classical power set, you still can retain the notion of function types.

This would be agnostic regarding whether func(N,bool) is uncountable in the sense of size.

So it would be compatible with both the standard reals as well as the computable reals.

Secret

Ok I see, so we basically make the (un)countability of reals ungrounded, but we can still retain most of its properties

~~I always thought things like non separability will be gone if we cannot ground the notion of uncountability~~ O wait, my brain overshoot my typing, let me reprocess...

user21820

17:11

You still have uncountability in the sense of complexity. No surjection from N onto func(N,bool). But without the classical power-set notion you cannot prove or disprove that func(N,bool) injects into N.

Secret

I see. Btw an unrelated question. We knew that in cardinality there's the notion of potential vs actual infinity. What are the computational theory analogues? Is it halting problems and turing jumps?

user21820

@Secret That's the usual analogous notions for potential and actual infinity, but that's nothing to do with cardinality...

Cardinality is about the existence of bijections, and in ZFC it is also about the existence of a bijection with a well-ordering.

I'll have to think about the uncountable closed subset of R. Not now though; have to go off soon.

Secret

I mean, in terms of size, potential infinity is about "increasing something forever" and actual infinity is "something that is larger than everything else"

in terms of complexity and computability, what will be the corresponding concepts?

user21820

@Secret "forever" has nothing to do with size.

Size and sequences are totally different, as I said earlier with V[ω[1]] having uncountable sets but only countable sequences.

Finite sizes and indices coincide. From ω onwards they clearly diverge.

ω+1 is longer than ω but both are the same size.

Secret

17:28

Complexity also form a hierarchy, like 2 is more complex than 1 (need 2 bits to express instead of 1) 3 is more complex than 2 etc.. Is there a name for the limit of moving up this complexity hierarchy indefinitely and is there a name for a complexity so complex that you cannot reach it from below (similar to how only oracles can solve halting problems while turing machines cannot)?

O wait, I think you answered the second one already (Turing jumps) So I guess my question will be whether there's a name for the notion of "going arbitrarily close to a turing jump"?

user21820

You may be interested in recursion theory investigating what is between computable stuff and the first Turing jump.

I do not know much about it, but I think the computability degrees (Turing-equivalent) are dense below the first jump.

Secret

Turing degree

In computer science and mathematical logic the Turing degree (named after Alan Turing) or degree of unsolvability of a set of natural numbers measures the level of algorithmic unsolvability of the set. == Overview == The concept of Turing degree is fundamental in computability theory, where sets of natural numbers are often regarded as decision problems. The Turing degree of a set is a measure of how difficult it is to solve the decision problem associated with the set, that is, to determine whether an arbitrary number is in the given set. Two sets are Turing equivalent if they have the same level...

Ouch...
It is a partial ordering, and it is not even dense

user21820

Turing degree

In computer science and mathematical logic the Turing degree (named after Alan Turing) or degree of unsolvability of a set of natural numbers measures the level of algorithmic unsolvability of the set. == Overview == The concept of Turing degree is fundamental in computability theory, where sets of natural numbers are often regarded as decision problems. The Turing degree of a set is a measure of how difficult it is to solve the decision problem associated with the set, that is, to determine whether an arbitrary number is in the given set. Two sets are Turing equivalent if they have the same level...

Secret

(sniped)

user21820

Yea it's not dense.

But click on my link to go to the order properties.

> Every countable partially ordered set can be embedded in the Turing degrees.

I'm not sure whether the facts listed there addresses my claim that it is dense below zero jump.

It looks like it is false because of:

> No infinite, strictly increasing sequence of degrees has a least upper bound.

If so, I'm a bit surprised; I did think we can get arbitrarily close to zero jump from below.

Secret

17:42

> For any set X the notation X′ denotes the set of indices of oracle machines that halt when using X as an oracle. The set X′ is called the Turing jump of X. The Turing jump of a degree [X] is defined to be the degree [X′]; this is a valid definition because X′ ≡T Y′ whenever X ≡T Y. A key example is 0′, the degree of the halting problem.

Hmm, it seems every poset can be use to implement a turing jump for something less complex that it

::Realises I need to read up what is a jordan measure in order to fully understand that post::

Leaky Nun

23:08

@Secret after playing with a proof-assistant, this is my set of axioms:

class ordinal (α : Type u) extends
  linear_order α, has_zero α, has_add α, has_mul α :=
(omega : α)
(succ : α → α)
(zero_le : ∀ x : α, 0 ≤ x)
(zero_lt_omega : 0 < omega)
(zero_or_succ_of_lt_omega : ∀ x : α, x < omega → (x = 0 ∨ ∃ y, x = succ y))
(succ_ne_zero : ∀ x : α, succ x ≠ 0)
(succ_ne_omega : ∀ x : α, succ x ≠ omega)
(succ_inj : ∀ x y : α, succ x = succ y → x = y)
(lt_succ : ∀ x : α, x < succ x)
(le_of_lt_succ : ∀ {x y : α}, x < succ y → x ≤ y)
(add_zero : ∀ x : α, x + 0 = x)
(add_limit_le : ∀ {x y z : α}, y ≠ 0 → (∀ w : α, w < y → x + w < z) → x + y ≤ z)

Transcript for

$Mathematics$ Mathworks (Not the main chat!)