« first day (28 days earlier)      last day (471 days later) » 

7:34 AM
@Secret I don't know what you're saying here and in your next 8 comments. Well-orderings come with a set and a binary operation. The well-ordering (1,0,3,2,5,4,...) is not the same as the well-ordering (0,1,2,3,4,5,...). Thus my comment shows predicatively that there are uncountably many distinct well-orderings.
@Secret Yes this is one possible way. Namely we don't assume that you can fully reify definable functions or predicates.
@Secret Yes if f is definable but not reifiable. My earlier comment was because your example for f was so simple that everyone would consider it an object.
But 8 would still exist as an object, even if f didn't.
Because f(7) is an object.
@Secret: If you still don't get my first comment, consider the C/Java function
g(m,n) { if( m==n ) return false; if( m/2<n/2 ) return true; if( n/2<m/2 ) return false; return ( f(m/2)==(m<n) ); }
For any f in func(N,bool), you get a distinct g that is a well-ordering.
 
For that one, I am kinda embarassed to say that initially when I wrote it it looks fine, but as I continue to write and re read it, it gets more and more weird and eventually whatever thought I had at the beginning completely trails off and thus the 8 comments is kinda like a derailed thought process

What I do recall is I think I am trying to write something along the lines of:
(-5,1)(-4,2)(-3,3)(-2,4)(-1,5)(0,6)(1,7)...
and then whether it is order isomorphic (below is produced by x -> 2x+1 on each entry) to:
but I think that is the same as the (1,0,3,2,5,4,..) example you pointed out, the omitted entries in the new list has to go somewhere, thus I still end up a distinct well ordering and not an isormophic one
 
Oh.
All the examples produced by g are isomorphic.
That's why I said I can't immediately see whether WO is predicatively known to be uncountable or not.
The issue is that WO is a pseudo quotient type, because the relation is not total, so you expect it to have 'more' equivalence classes than in ZFC, but I think you can't show it, because the failure of LEM for isomorphism also prevents you from being able to show that the 'different' classes are truly distinct.
Does this make sense?
 
7:53 AM
Let me check whether I have interpreted the procedure of g correctly:
 
C/Java uses integer (round-to-zero) division.
 
So given a pair of naturals (m,n), if they are the same, g gives 0, if m<n g gives 1, if n<m g returns 0, otherwise (the incomparable case??) return (I don\t quite understood that final condition)
i.e. what is this condition comparing equality about and what value of g will it return?
f(m/2)==(m<n)
o wait let me read again...
20 mins ago, by user21820
For any f in func(N,bool), you get a distinct g that is a well-ordering.
$$g(m,n)=\left \{\begin{matrix}0, m\geq n \\ 1, m < n \\ f(m), \text{otherwise}\end{matrix}\right.$$
 
9:02 AM
Edit:
 
9:21 AM
$$g(m,n) = \left\{ \begin{matrix}0, m=n \\1, m\backslash 2 < n \backslash 2 \\ 0, n\backslash 2 < m \backslash 2 \\ \text{Bool}(f(m \backslash 2)==(m<n)), \text{Otherwise}\end{matrix}\right.$$
 
10:00 AM
@Secret Do you know programming? If f is a function on nats that returns a bool, then you can compare its output with (m<n).
 
I know mainly python and bash, and very little bit of C
 
Python should be the same.
Python 3 even allows ";" for separating statements. But no "{}" in Python.
 
Yeah, I just rarely see a predicate in the other side of the == sign, because I usually see a single letter or word
 
I was just lazy haha..
 
Good morning to everybody
 
10:02 AM
this is why initialy I am not familar with reading (m<n)
 
Can I have an help please?
 
It's basically you use "m<n" or "n<m" depending on what f(m/2) says.
 
@Sebastiano Set and type theory, predicative, constructive maths here only for this period. Otherwise head to main chat
 
I'm studying calculus of variations
 

 Mathematics

Associated with Math.SE; for both general discussion & math qu...
 
10:03 AM
@user21820 Ah that's more clear
 
@Secret Do you mind if we change the room title to be more explicit?
Or are you changing the topic regularly?
 
@Secret For me it is the first time after many times.
 
@user21820 Well, this room is supposed to be my giant roughwork sheet. and topic are expected to change constantly. It just happens in trying to understanding infinity (that is topic 1), I end up stuck at foundations of mathematics due to my poor background
 
@Secret excuse me for the disturbe. good morning
 
@Secret Haha I see.
 
10:06 AM
In particular, having so much traffic is an unexpected by welcoming function of this room that I initially not planned
I set up this roughwork sheet because too many people said I flood the main chat with my rambles
(commonly known as very long [random] in the main)
Since we are going to stuck at topic 1 for a while (because I will not change the topic until I get a firm grasp of many aspects of infinity and objects), this room is kinda like a foundation of mathematics room for this period
thus acts like a complementary to set theory room which (that room) explores more nonconstructive mathematics with classical logic
typo: unexpected but welcoming
 
@Secret Well I think you shouldn't bother people in the main chat with what you think you found out in philosophy of mathematics (unless they are interested of course), largely because most of them don't care about foundations and even if they do it's unlikely that they will understand you (or me) via brief explanations because this kind of predicativity is a very atypical kind of viewpoint.
 
That I am not worried, I can describe it once I understood sufficiently. and at least 3 other users (including leaky) are interested about it
as long I keep it short, it will not disrupt main
after all, the main is used to all sorts of weird things I ramble
 
@Secret In my opinion you should simply invite those interested users here.
Anyway it's not that I think it's disruptive to the main chat. They have lots of junk messages anyway.
 
That's what I am planning to do when e.g. mercio gets on next time. He seemed quite curious about predicative mathematics
and I think I might be able to get akiva on board because he too like weird or nonclassical things
The following is my old list:
in Mathematics, Jan 21 at 6:17, by Secret
List of maths fields I have interest in:
1. Group theory in terms of orbits and actions
2. Zero term algebra and division by zero algebra
3. Integration in the language of abstract algebra and as a functional, symmetry of integrands
4. Optimising proofs given axiomatic systems
5. Category theory
6. Unnatural algebraic structures
7. Patterns in expanding multiplications of polynomials
8. Set of all counterexamples given a proposition
9. Tensor visualisation and intuitions
10. Numerical analysis methods to explore special regions or points of mathematical functions or systems of equations
(Warning 2 is a personal project, thus it is not mainstream, it was dealt in another room a year ago for 5 months. Most of the regulars of the main are aware of that, and they give mixed but useful feedback to improve the process, but also keep errors in check so it does not degenerate into crankery)
I had not thought of the new list yet, since I am not the type of person who like to conform to schedules
3. In simple terms is about how to evaluate integrals and why
 
10:24 AM
@Secret Lol. Since you mention it, did you know that your kind of 'math' on first glance sounds a lot like crankery (and probably looks a lot like it to mainstream logicians or set theorists). It's only because I have had similar thoughts before that I recognized what you were trying to understand.
 
That's pretty normal. I, like most people, have alien thoughts that sound nonsense, but I have been trying to learn the language of the mainstream and explain to them and let them to contribute and work together
 
Also, I saw a few of your posts about proof structures. Some logicians call it "the moral" of the proof, a vague notion referring to 'the essential core' of the proof.
Many proofs have the same 'moral' but different arrangements.
 
In general, I like to analyse big picture of things, be it the "skeleton" or moral of the proof, the topology of a space and so on
 
I know what you mean.
 
3, which is known as the Integral Project, is trying to analyse what governs all integrals, for any integrable function
 
10:28 AM
I like finding the 'cleanest' explanations for things.
 
Some users in main said I will love category theory because it emphasize a lot of the big picture of maths structures
and I also suspect, since 3 is basically a question of a rewriting system in the context of differential algebra and special functions, I suspect my type theory reading might help me on that (though this thought only occurs to me today)
 
@Secret Hmm in some sense integration is as incompletable as PA.
In symbolic computation (or computer algebra), at the intersection of mathematics and computer science, the Risch algorithm is an algorithm for indefinite integration. It is used in some computer algebra systems to find antiderivatives. It is named after the American mathematician Robert Henry Risch, a specialist in computer algebra who developed it in 1968. The algorithm transforms the problem of integration into a problem in algebra. It is based on the form of the function being integrated and on methods for integrating rational functions, radicals, logarithms, and exponential functions. Risch...
 
Yup, I am familar with that. What I am wondering about is integrating special functions, which is basically writing one special function into another
Semiclassical and I have been discussing about whether a galois group for special function exists
 
@Secret But the addition of special functions doesn't solve the problem in the same way that adding independent sentences in a computable way cannot make a consistent extension of PA complete.
So it's not clear exactly what you want to achieve.
 
It does not make it complete (because rische algorithm said that those have no elementary antiderivative), but it is more about whether they are patterns on determing how we "integrate" special functions by writing the integral of one of them in terms of other special functions, whoose behaviour are more known
 
10:34 AM
Hmm.
So you do not intend to have a 'theory' that captures integration of those special functions themselves?
 
I don't think that is possible (because there might be an incompleteness condition to how far we can decide how a special function can be expressed in terms of another), but I want to capture as many of them as possible
Let me show you what I mean:
13
Q: How to evaluate $\int_0^\infty\frac{\frac{\pi^2}{6}-\operatorname{Li}_2\left(e^{-x}\right)-\operatorname{Li}_2\left(e^{-\frac{1}{x}}\right)}{x}dx$

Nik Z.I need to evaluate the following integral with a high precision: $$ I=\int_{0}^{\infty}\left[% {\pi^{2} \over 6} - {\rm Li}_2\left({\rm e}^{-x}\right) -{\rm Li}_2\left({\rm e}^{-1/x}\right)\right]\,{{\rm d}x \over x}, $$ where ${\rm Li}_{2}$ denotes the dilogarithm $\displaystyle{% \left(~\mbox{n...

So this integral is nonelementary and kinda scary
but those who have been working it for years will recognise which groups of terms they will put together and simplify or rewrite it in terms of some other functions, thus getting a closed form
 
Yea I get what you mean.
But in my opinion it's just ad-hoc.
Anyway I will be away intermittently. See you later!
(ad-hoc meaning that you need ever more ad-hoc special functions to solve integrals of special functions)
 
so the project tries to categories closed forms, because they are slightly easier to implement in programs
and yes, the collection of special function is going to grow indefintely, it's not even a set or class like object, it is a culturally dependent construct
but a portion of them does behave nice enough that is worth to investigate, I think...
The issue of numerical techniques is that errors pile up, but an analytic expression the error may not grow as big
 
10:54 AM
@Secret What would be nice is if there is a systematic way to extend the 'class' of special functions, so that we don't have to rely on current culture.
 
Yeah, as right now, special functions are defined based on whether they are from "interesting" problems which is too unsystematic
and they are kinda ad hoc because e.g. $$\int e^{-x^2}dx = \frac{2}{\sqrt{\pi}}\text{erf}(x)$$ is basically renaming something you cannot "solve analytically"
 

« first day (28 days earlier)      last day (471 days later) »