This is the Realm of Simply Beautiful Art - 2017-02-20 (page 1 of 2)

« first day (44 days earlier) ← previous day next day → last day (1454 days later) »

Simply Beautiful Art

1:35 AM

@BrevanEllefsen Hm, I wonder what's the easiest way to prove aforementioned limits

I mean, I think my answer is the easiest way, but without my answer it's not as easy

@Simple Hello and how may I help you/how have you been?

@SimplyBeautifulArt hello, I am leaning system of ode

do you know anything about this

Simply Beautiful Art

mhm... not much

I can look at DE's and say things

and sorta understand

But I haven't learned any differential equations course

can you borrow a book from your school library to learn it?

Simply Beautiful Art

XD

Ok, sure

:|

Huh?

1:52 AM

user image

I got this graph from a system of ode

Simply Beautiful Art

Oh

Well then

it is a planar motion

Simply Beautiful Art

Mhm...

(you already lost me)

(⊙０⊙)

Simply Beautiful Art

Yup

2:01 AM

Lagrangian mechanics

Lagrangian mechanics is a reformulation of classical mechanics, introduced by the Italian-French mathematician and astronomer Joseph-Louis Lagrange in 1788. In Lagrangian mechanics, the trajectory of a system of particles is derived by solving the Lagrange equations in one of two forms, either the Lagrange equations of the first kind, which treat constraints explicitly as extra equations, often using Lagrange multipliers; or the Lagrange equations of the second kind, which incorporate the constraints directly by judicious choice of generalized coordinates. In each case, a mathematical function...

Simply Beautiful Art

As I said, I've only learned so little

@Simple But since you suggest, I'm going to see if I can learn about differential equations and stuff by the mid of next month

I know, so I show you an application

hello.

Simply Beautiful Art

@Simple Ok. You can leave stuff here, but its my bed time now, so I'll have to see you later

@Ramanujan Hello

good night

2:04 AM

@SimplyBeautifulArt Good night.

4 hours later…

6:30 AM

@Wojowu @Deedlit: I believe I have constructed an embedding of Buchholz hydras with finite labels into super-trees. If so, then according to the (Googology Wiki page here](googology.wikia.com/wiki/%CE%A8%28%CE%A9_%CF%89%29) the order type of super-trees is at least the proof-theoretic ordinal of Π[1,1]-CA0.

1 hour later…

7:49 AM

Oh oops on checking it seems wrong.

Hi @Deedlit! Do you know the order type of my super-trees and the growth rate of my function?

8:03 AM

Hi @user21820! It will take a while for me to go through your code and figure out precisely what it does, and I still have gaming tomorrow, so it might be a couple of days or more before I can answer you.

@Deedlit: Sure no hurry and thanks in advance for your time and effort!

As for the termination of the Basic Matrix System, you do raise a good point. There was a Japanese googologist who claimed a proof of termination, but it's in Japanese so I can't speak for it's correctness. So yeah, there is definitely an issue here. I just wanted to see if I could code what could be an incredibly powerful system in 256 characters. :)

Yea I am very interested in seeing the proofs of such systems.. Because I'm quite interested in reverse mathematics.

One rationale for my entry: I don't know if you have heard of the Bignum Bakeoff by David Moews, that was a previous big number competition, except it was limited to 512 characters and was in ANSI C only. The criterion for winning was if Moews could determine if your number was the largest, and if you couldn't, then all entries that could possibly the biggest were tied. So, you didn't need to prove termination - HE had to prove that your program didn't out put an enormous number.

I do like reverse mathematics as well, although my logical foundations may be a bit shaky. :)

I heard of that, but didn't know the rules. But then Moews would have had to specify a foundational system for his proving efforts.

Otherwise he could easily pick ZF plus some axiom that disproves MLTT...

That's why I said that SimplyBeautifulArt would have to pick a foundational system anyway, to make the comparison totally well-defined (even if we can't decide).

I have a good grasp of everything up to the incompleteness theorems, but beyond that I know very little. I also took an introductory course in model theory but forgot a lot of it because it just didn't appeal to me.

The rest I gleaned from online sources so it's all over the place and intertwined with philosophy hahaha...

8:17 AM

Hmm, I think most mathematicians don't specify the exact axioms that they work with, they argue in a less formal setting - still considered rigorous, but they don't specify exactly what axioms that they are using. I think most mathematicians couldn't identify what axioms they need to prove all of their results.

It was only in the 20th century (or I guess late 19th) that we started talking about foundations for all of mathematics, and I think most of that work (ZFC, PA and the like) doesn't effect how mathematicans work.

For example, an interesting unsolved question is exactly what axioms are needed to prove Fermat's Last Theorem. The use of Grothendieck universes meant that, taken at face value, you would need ZFC + inaccessibles for the proof to go through. But the conjecture of many is that it can go through in PA.

Let me link Moews' analysis of the contest programs... no formal mathematics, just traditional mathematical reasoning.

djm.cc/bignum-results.txt

Yes, most ordinary mathematics is doable in ACA or even PA, so they are provable in most foundations.

I must say, if you have managed to surpass Buchholz hydras with finite labels, that is extremely impressive, and all the more impressive if you can prove termination.

Yes, most mathematics is provable very low.

However, when comparing fast-growing functions traditional mathematical reasoning isn't enough unless we don't care about inconsistency.

I remember reading that consistency of CoC needs quite a strong system to prove.

yes

And we actually need Σ1-soundness, not just consistency.

8:23 AM

because it surpasses all provably recursive functions of higher order logic, in cannot be proven from higher order logic

The faster you grow, the stronger theory you need

Without Σ1-soundness, a system might perhaps prove termination of a program (a Σ1-sentence) but it actually never terminates.

So if you don't accept theories as sound beyond a certain level, you must necessarily reject the highest contenders (that are acceptable to people who accept the higher theories)

Yea that's the issue, so the best possible program is actually affected by the contest setter's choice of system.

yes, I guess we are saying the same thing here.

The difference is in what we accept.

Yea.. By the way do you know any sentence provable in ACA that cannot be proven in Π[1,1]-CA0?

8:28 AM

The latter is strictly stronger.

I know the latter is strictly stronger than ACA0, but ACA as well?

Hmm, I think so but I guess I shouldn't say I know for certain.

This is the kind of thing that is surely answered in Simpson's SOSOA.

"Systems of Second Order Arithmetic", the bible for reverse mathematics

Ok I'll try to find the answer.

When Wojowu comes on, I'd like to ask him if he can give a convincing argument for ZFC.

I'd be glad to hear it.

8:31 AM

I do know that Wojowu is very Platonist.

I know two common kinds of ontological justifications for ZF, but from my viewpoint they are incompatible and give rise to different parts of the ZF axioms.

Specifically this, which I mentioned to Starfall in a previous conversation here about this.

Well, if w_1 is not a set, then the von Neumann hierarchy is just V_w_1. But then we are just stopping at an arbitrary point... there is no reason we cannot continue to expand the universe.

That's how I think about it.

That's indeed the common response, but the justification for not stopping is that we can conceive of all the stages labelled by previous constructed sets, which is circular if we haven't yet constructed them.

Specifically, the not stopping argument should also imply the entire universe is itself a stage.

I don't think what we need to conceive all the stages.

I think that not stopping is what makes the universe not a stage.

If it makes the universe not a stage, then it also supports not accepting replacement.

8:44 AM

but replacement never goes all the way up

so it's "safe"

The question here is not whether ZF is consistent since I believe that.

The question is whether it is ontologically justifiable.

So while I believe the arbitrary restriction on replacement to be for functionals applied to sets is 'safe', it does not justify the axiom schema.

hmm, what makes you believe ZF is consistent if you don't believe it has an ontological basis?

Specifically, how do you answer to Boolos himself that I cited?

Oh for syntactic reasons.

Con(ZF) is simply an arithmetic statement and I believe from empirical evidence that it is true.

hmm, okay

sorry, I don't feel like reading Boolos' paper right now.

However I'm not sure whether ZF is even Σ1-sound (similar to my earlier mentioned doubt in other strong systems for big number contests).

Well at least the cited portion agrees with my analysis that the usual argument does not work; namely if we grant N as a complete collection and we grant the power-set operation, and we grant closure of collections under countable sequences that can be iteratively constructed, then we cannot get to V[ω[1]].

8:49 AM

I guess you need choice to get w_1 for power sets

*from

the way I see Replacement is that, we want to build up this ever-increasing hierarchy.

We don't want any limit to this hierarchy, but we also want our sets to be at a specific level, not going "all the way up"

so Replacement is a way to tie down general predicates to sets

My view of the historical liking for Replacement is similar; Specification was to reify definable predicate-symbols and Replacement was to reify definable function-symbols.

You've probably heard all this before

The problem is that we know that we cannot fully reify everything in classical logic.

Due to diagonalization.

So I find ZF's particular brand of reification to be ad-hoc; I think it avoids contradiction but I can't pin any meaning to it.

sorry, what does reify mean?

Firstly given a first-order theory S we can extend it conservatively by adding full abbreviation power (definitorial expansion).

Reification is the idea to let those very function-symbols and predicate-symbols be objects themselves.

Clearly the Russell predicate cannot be reified, so we can't allow all reification.

The need for reification is to allow us to reason about those definable functions and predicates.

It's like stuffing higher-order logic into a single sort.

9:01 AM

Thanks.

So the way I see it is that different foundational systems are based on different ideas of restricting reification.

Higher-order logic says don't bother. ZFC says let's try starting from an empty set and reifying only some predicates and functions on the 'small' side.

right

My question is which one is more meaningful.. Currently I'm leaning towards higher-order logic, but the same issue of "why stop at finitely many orders?" is still there.

well, you could have many axiom collections that are all true for the same structure, say the cumulative hierarchy.

and they could look ad-hoc

but it seems to me that replacement is "true" for the cumulative hierarchy.

Of course replacement is true for the cumulative hierarchy from the viewpoint of ZF.

9:06 AM

not sure I understand the qualification

If I'm not wrong, within ZF we can build the cumulative hierarchy and prove that if ZF is consistent then the hierarchy is a model of ZF.

But if you don't have ZF to start with, you can't even build the hierarchy.

I'm not thinking within ZF.

Then how do you build the hierarchy?

We have this abstract structure called the cumulative hierarchy that is not tied to ZF.

I don't agree we have it... I understand your earlier point that you want a structure of sets that satisfies certain properties, but I don't see reason to believe such a structure exists.

9:09 AM

it's just built up from the empty set and continually taking power sets and limits.

The problem is in the "limits" part.

You can form nice sequences and conceive of their limits.

But how to form an uncountably long sequence?

we know that the collection of everything is uncountable

I agree with that.

But a sequence is far more than a collection.

so the question is if the universe must necessarily stop there, or if we can continue

You must somehow give a well-ordering on an uncountable collection before you can claim existence of an uncountable sequence.

9:12 AM

We have all the countable ordinals

Right.

so the union of those can't be countable

Right.

so clearly we have an "uncountable ordinal" here.

Nah.. "countable ordinals" is a well-defined concept, but not a collection that you have constructed.

9:13 AM

The only reason not to accept it is if you think this is a proper class

That's pretty much a similar notion.

To be more precise, I accept quantifying over countable ordinals, and the precise statement that they aren't countable is just that there isn't a surjection from N onto them. But we can't do things with the countable ordinals as a single object.

Why not?

The key point is that when you form the collection of countable ordinals in ZF, it is impredicative.

I guess impredicativity doesn't bother me.

For purposes of ontological justification, it is relevant.

Because we haven't yet finished constructing the stages in the hierarchy.

So we can't construct something that involves quantifying over things we haven't yet constructed.

9:18 AM

I don't know - how can you go beyond the finite if you can't quantify over things we haven't yet constructed?

That's why I said earlier that to start the iterative conception we already assume the existence of N as a complete collection.

If not then indeed you're stuck at finite.

that's part of why I don't agree with your restriction.

You have to make an ad hoc exception for N

@user21820 <- Well I stated it here. And people who use the iterative conception already assume it. Yet surprisingly few people know about Boolos' objection to the validity of the iterative conception beyond countable stages.

By the way it's not an ad-hoc assumption, so that's why I'm willing to grant it.

The reason is that if you believe formal systems as we know it exist then you already must believe in a model of PA-.

but it seems to me that the "problem" at w_1 is the same as the problem at w.

It is, but we don't have an alternative to formal systems!

9:22 AM

so if you're willing to accept one, why not the other?

Because PA seems to be meaningful in reality at least as far as we have empirically tested it.

Whereas set theories don't.

In general.

I always mention FLT (fermat's little theorem) as an example theorem of PA that works in real life billions of times a day in RSA decryption.

So far so good.

we have only empirically tested small finite sets though

Of course; hence my caveat above.

But I haven't seen any real-world interpretation of set theory, not to say be able to test even small parts of it that involve infinite sets.

I dunno, your reasoning seems more pragmatic that based on ontological justification.

I'm a realist, and I believe that ontology needs to be tied to reality otherwise it's just imagination and could be unsound.

I have nothing wrong with imagination per se, just that it's not convincing as an argument for meaning.

9:28 AM

but mathematical structures are all imagination.

The set of real numbers for instance.

Heheheh.. the reals and complex numbers seem to be necessary in wave-functions.

or even the natural numbers as a whole

the whole "potential infinity versus actual infinity" thing

Yes, in terms of reality I don't think of a real-world representation of N in the same way as set theorists.

what exactly is a real-world interpretation of N?

My interpretation of collections in the real-world are more like the types-as-programs view.

9:33 AM

Hmm - so you believe that the halting function is a well-defined total function?

I knew you would ask that. =) The argument for the meaning of the halting problem is that we view quantifiers over N using game semantics.

Each quantifier is one move, and arguably either one player wins or the other wins since the game ends after a fixed number of moves for any arithmetic sentence.

but but... you've been saying all along we can only accept things as true if they are provable in some foundation of choice.

but no consistent recursively enumerable formal theory can prove that all halting programs halt

That's for the purposes of the contest, because we need a rigorous and precise notion to determine winners.

For philosophical justification of the meaningfulness of the halting problem, we have no choice but to appeal to real-world intuition, however terrible it may be.

Suppose the contest-setter chose some foundation F I don't believe in. I can still agree on the winner because I can check whether a proof in F is valid or not. We only need finitely many steps to do the checking.

I may not agree that the program really halts (even with unlimited time and memory), but I agree on the winner.

However, if I am the contest-setter I wouldn't pick F of course.

It seems like you have a rather constructivist (and realist) point of view.

Yea! I do!

9:39 AM

I'm definitely more formalist than Wojowu.

but I don't think math is a "meaningless game with symbols"

I think it is a "meaningFUL game with symbols"

I am quite happy with ACA (which follows from the finite game semantics), which is why I'm so interested in programs that supposedly terminate but cannot be proven in ACA. I most probably accept predicative higher-order arithmetic in the same vein as ACA, though I admit I'm not sure whether I quite believe in LEM for quantified statements over functions on N.

So now you know why I have such interest in fast-growing functions, because I want to see whether I should accept more.

Same here. I think most mathematics is actually meaningful and that certain more esoteric branches of mathematics are less so simply because of artifacts of the chosen foundational system.

so while I don't think each individual real number necessarily has a Platonic existence, I think the mathematical structure has it's own existence, as in it follows certain rules and has consequences, and the "game" we play with mathematics is as real as the natural numbers 1,2,3.

Well a formalist only needs to believe PA- since he can certainly check validity of every proof in PA-.

what does the - mean in PA-?

PA- is described here

Basically it's equivalent to basic properties of string manipulation.

PA- plus induction gives PA.

9:44 AM

Ah, I see.

I suppose a formalist COULD only believe in PA-.

But I'm not looking to restrict what I believe in as much as possible.

Yes. That's why I currently believe in the accuracy of ACA at reasonably small scales, and am looking for what is beyond it that seems valid.

The difference between finite Jumps and beyond is that the finite game semantics do not work past that point.

okay, so you believe in 0^(n) for finite n.

but not 0^(w) I guess?

Yes to the first question. Half to the last. It's a meaningful concept but we can't use it as a decider.

So if we go back to fast-growing functions

you would accept BB_m(n) for finite m.

how about diagonalizing to get BB_omega(n)?

I'm not familiar with the subscripts, but I presume BB[k+1] uses BB[k] as an oracle.

9:51 AM

yes

Then yes BB[m] is computable by (m+1) jumps and so we can use it. But if we ask whether a program using arbitrary finite jumps halts or not, it may not have a definite answer.

interesting.

That seems impossible to me, that BB_m could exist for all finite m but BB_omega would not.

Put another way, ( N -> N ) is not a classical set in that its members include all those procedures that you can actually prove to halt, and excludes all those procedures that you can prove to not halt, but there may be a gap in-between.

So you can't quantify over that collection and expect to get a true/false answer.

By "include" I mean "include at least".

Interestingly, there is a logician Nik Weaver who has similar ideas to mine.

Though he favours intuitionistic logic for the parts with the truth-value gap, while I favour Kleene's 3-valued logic.

He's active on MO and disavows the power-set axiom of ZF!

Yeah, I've seen discussions between Nik Weaver with other members of the FOM community.

It seems like he's largely been met with opposition.

Haha I find many of his ideas actually philosophically tenable, even if I disagree with his choice of non-classical logic.

Anyway he seems to be accepted as a proper mathematician on MO.

10:01 AM

I hope that you don't take this the wrong way.

I don't know about the FOM mailing list.

But I wonder if there is a divide between "working mathematicians" and logicians who think more on the philosophical side.

I don't see how I could take it a wrong way, since I believe that the divide arises between working mathematicians and set theorists, rather than logicians per se.

It's just that I don't know how much "regular mathematics" you do :P

Working in mainstream mathematics probably affects your worldview a lot, but I guess we can't say that their positions are more justified because of that.

Haha.. it's well-known that nearly all real analysis can be done easily in ACA.

That's why I currently believe that predicative higher-order arithmetic is good enough for all practical purposes. When I see a counter-example I'll change my mind. =)

10:06 AM

yeah, it's not that you can't do mathematics in very restricted systems.

I mean naturally too, without coding.

I jus speculate that the process of doing mainstream mathematics affects your ontological views.

That's true.

But I'm personally of a logic inclination and I don't want arbitrary restrictions.

I recall a quote that "mathematicians are Platonists during the workweek and formalists on the weekends", or something like that

Probably the other way, since they push symbols during their work but handle real things outside.

For me I try to find a particular type of justification for some inference rules and then apply it to its maximum potential rather than stop halfway.

My CS background definitely influenced my viewpoints, as you probably can see.

10:10 AM

Yeah :)

Are you a logician?

Haha..

haha, I'm one of those "mainstream mathematicians" that never consider what axioms they use :P

but you probably figured that as well.

Ah I couldn't really tell, because you play with such large numbers that no ordinary mathematician would even dream of.

well, they do for fun sometimes.

This stuff is considered "recreational mathematics"

Besides you said you were interested in reverse mathematics, which majority of mathematicians have not even heard of.

10:13 AM

hmm, you think?

Really!

Majority of math professors at my university cannot even write down the axiom schemas for ZFC! Some have not even heard of the name!

yeah, I do have an interest in set theory and logic.

But I never really got a firm foundation, so I'm not that confident with it.

Wojowu has a more firm grounding than me.

I see.

Is he also a 'non'-logician like you?

yes.

(Who happens to be able to name very large numbers using 256 chars.)

(Like you.)

=D

10:15 AM

haha

We actually met on the Googology Wiki

Nice. Not in real life though?

nope.

I guess birds of a feather drink from the same water....

Including myself.. I'm actually officially in CS not mathematics.

nice

Working on very concrete algorithms that terminate in less than linear steps...

10:17 AM

But apparently you've learned a lot of logic on the side :)

out of curosity, algorithms for what?

Dynamic data structures.

cool

I majored in both Math and CS, and took some of the logic modules available.

And then after I graduated I continued studying logic stuff because that's my primary interest!

I went into CS for practical reasons hahahaha..

Yeah, I getcha.

Sometimes I wonder if I should have gone into CS myself.

Anyway, this has been a fun discussion.

Hmm.. If you're already working in Math, it's not convenient to switch right?

Even if you wanted to, that is.

10:22 AM

oh yeah, I was thinking earlier.

Ah I see.

I need to get up tomorrow, so have a good night!

Sure good night!

I will definitely look at your programs sometime.

Thanks a lot! =)

3 hours later…

Simply Beautiful Art

1:33 PM

Good morning!

1:58 PM

@SimplyBeautifulArt It is "Good night!" (For me).

:)

You here?

Well, I'll take my leave.

Simply Beautiful Art

2:16 PM

@S.C.B. Bye man

Simply Beautiful Art

2:57 PM

@theideasmith Hello and welcome to my realm!

What brings you to these parts?

« first day (44 days earlier) ← previous day next day → last day (1454 days later) »

Transcript for

Feb '1720

$Mathematics$ This is the Realm of Simply Beautiful…

Room for totally bored people to hang. Open discussions.

abstract-algebra big-numbers geometry logic recreational-mathematics

join this room
about this room

00:00

06:00

12:00

18:00

all times are UTC

$Mathematics$

site design / logo © 2024 Stack Exchange Inc; legal

mobile