« first day (760 days earlier)      last day (2071 days later) » 

12:30 AM
In the deductive system I was using, the aim is to show that a particular sentence can be derived from tautologies. Since it can be derived from them the sentence itself is one also.
For instance, ∀x. P(x) → P(f(x)) ⊢ ∀x. P(x) → P(f(f(x))) can be derived from four tautologies, although it doesn't look like a tautology itself.
So to answer your question, it would be proving it from no assumptions, expect the deductive rules of the system in use.
 
12:59 AM
I see what you are doing. f is a successor-like function
@Secret measurability is needed for position-space quantum
In particular you need the leb integral to complete your Hilbert space
Riemann will not do
 
 
2 hours later…
3:09 AM
user21820, David Reed: I am happy enough if the mathematical object does not have applications that only get stuck inside set theory and counterexamples that does not illuminate something deeper about theorems in 'core' mathematics
Because sometimes when I read about the impredicative or nonconstructive objects in ZF and ZFC, they often give me that impression all their applications have done nothing other than adding footnotes on existing theorems
footnotes that can otherwise be safely omitted without blowing up half of mathematics
For me, something is mathematically important if we taking it out and the rest of mathematics will implode, such as intermediate value theorem, where the alternative is very cumbersome ways to try to restore some notions of analysis
Not that trying to replace these important things is not encouraged, as too few people (according to a MO post) trying to work in a finitist framework to figure out what shortcuts to proving and constructing the infinite objects otherwise provided
So my hierarchy goes like this:
Stuck inside set theory or foundations < Mathematically important < Has a real life physical counterpart
But why do I care what each mathematical object belongs to which part of this hierarchy, because while I do love infinite objects, I want to know how much of this is closer to pure fantasy and any expectation that they will become mathematically important is unlikely, or we can optimistically hope that some time in the future they will become very important
$\omega_1$ always seemed to be an example of something that has done little to mathematics outside foundations other than making certain topological theorem less universal (e.g. all one manifold is metrisable is false purely because of the long line and its relatives)
 
3:41 AM
Update: O wait...
10 hours ago, by user21820
There are other uses of well-orderings in 'core' mathematics. If you do want every vector space to have a basis, then you do need a well-ordering of the vectors in that space. They seem to have no real-world implication, but hey it's still mathematics.
I guess... that will count as mathematically useful, given how so many functional analysis proofs are much nicer with a Hamel basis, and all of these are uncountable thus at least $\omega_1$...?
We'll I guess... Hamel functions, Vitali sets, $\omega_1$ and other uncountable well orderings are relatively tame compared to Bernstein sets, Large cardinals...
and banach tarski ( so far have seen no application of that in any proofs outside set theory)
Artem, we frequently deal with non-measurable sets in probability theory. For example, when we have a stochastic process $\xi_t$, we are concerned with the filtration (increasing sequence of $\sigma$-algebras) $\mathcal F_t$ generated by the process at times $s \le t$. Consequently, an event such as $\{ \xi_2 \ge 0 \}$ is not measurable with respect to the $\sigma$-algebra $\mathcal F_1$. My point with this comment is not to answer Matt's question; rather, it's to say that you can't easily dismiss it by saying that we only work with measurable sets in probability. — Tom LaGatta Aug 18 '10 at 18:33
that has not said whether Bernstein sets were involved (since those are absolutely non measurable, meaning that for any measure $\mu$, it is nonmeasurable)
63
Q: Why does research on the busy beaver function get funded?

HakaishinI saw this video about the busy beaver function and looked at the applications section of the Wikipedia article about the busy beaver function. I concluded that there is zero practical or even theoretical value in searching these numbers S(n) : n > 5. Now in the video the person says, that peopl...

It seemed to me so many impredicative objects not only have no real life counterpart, but are also mathematically unimportant
And that link is not a concrete application, because all it has done is adding footnotes (notice all those theorems presented all have the word "Bernstein set" in them, meaning that these theorem are only about Bernstein sets, thus are useless when there is no Bernstein sets)
so I don't get how that is a "concrete application" when all it has done is adding footnotes
and in this one, while it seemed nice that we can put algebraic structures on top of Bernstein sets, the application section is all about partitioning $\Bbb{R}^n$ with these sets, but why are we interested in these partitions, it tells us nothing other than Bernstein sets can be a partition of $\Bbb{R}^n$?
My point being (I don't know if I have searched deeply enough but yesterday I did crawl through all google results, MSE and MO using the search term "Bernstein set" and "Bernstein set" applications)
In theory, if we nuke every single paper that talks about Bernstein set, mathematics will not suffer a crippling loss and came crashing down
(and we cannot really ignore this implication, because Bernstein sets are the norm of nonmeasurable sets, thus it basically means that almost all nonmeasurable sets (one of the most significant byproduct of the axiom of choice) are mathematically unimportant)
Meanwhile in the ZF end, infinite Dedekind finite sets and amorphous sets are also not very optimistic either in their mathematical importance:
Here it seems to suggest $\Delta$ Dedekind cardinals can be used to talk about prime ideals, but it seemed to be focusing more on the algebraic structure on $\Delta$ itself than relations to other algebras, thus still kind of stuck inside set theory by being a footnote
 
4:22 AM
And thus, the reason why I am so interested in your predicative foundation is it will allow me and also inspires me to find the answer to this question:
> Are impredicative and nonconstructive objects like: Amorphous sets, Dedekind cardinals, Uncomputable functions, Bernstein sets, Banach Tarski paradox, Large cardinals, Hamel functions etc. have any application outside of itself (not just adding footnotes to existing theorems in core mathematics), set theory and mathematical foundations, or all they all useless artefacts of ZF and ZFC that can only exist within the world they create?
 
4:46 AM
Assuming the answer to the above is false, then that means business as usual
Assuming the answer is true, then I will be very sad, but it also does not mean that the mathematics community need to start deleting all papers that mention these things. Rather, the community need to recognise these things are mostly inside their own world and has to be treated as such until they broke free. Business as usual expect maybe a stronger awareness of the fantastical nature of these things
I don't mind playing with fantasy as long I knew it is a fantasy. What frustrates me is when I don't know whether I am playing with fantasy
 
5:03 AM
Typo: expect->except
 
 
1 hour later…
6:20 AM
@user400188 Induction is not a tautology, if that is what you are missing.
That is why I think everyone must engage with and fully understand the model of PA− that is not a model of induction, that I have just linked to. Can you see why it does not satisfy that particular statement, and can you prove that statement in PA (using induction)?
Once you can do both of these, you will fully understand why adding the induction schema to PA− makes it vastly more powerful.
It can prove many more things, which also means there are much fewer models.
 
 
2 hours later…
8:04 AM
@Secret As I said before, most logicians consider everything that ACA can construct to be obviously well-defined, and I had pointed you to this giving an informal sketch of what ACA means from a philosophical viewpoint.
If you reject the halting problem as being not well-defined, then you are basically stuck with PA or less. If you accept, as almost all logicians, then you ought to accept ACA. Many logicians accept even more, up to ATR. Of course there is a spectrum. Some consider systems with greater proof theoretic ordinal than ATR to be impredicative.
You should clearly distinguish between statements that can be stated in higher-order arithmetic and those that cannot. Those that cannot are more likely to be sensitive to the foundational system, and hence may be artifacts of the chosen system.
 
Ah I see, never thought about that before, hmm...
It is nice there is a generic way to measure the extent of something being an artefact. Will keep this in mind in my future explorations
 

« first day (760 days earlier)      last day (2071 days later) »