6:00 PM
I see flawed logic there.
: )

@AsafKaragila maybe he's his real dad, it's a popular plot device nowadays

@tim: making a demo, dots don't work yet, but the only problem with your skeleton is a weird unicode character in "OldIte<lsjldskjdsa>m" maybe inserted by chat as a soft line break

@AlexeiAverchenko Did you just discover that the man claiming to be your real father was not your real father, and that the man who claim that he is your true father is also a liar? Heck, as far as I know you may have never had no father to begin with. You're but a figment of my imagination!

I'm bracing for tomorrow: in a moment of mental darkness I decided to do a course about philosophy of mathematics. Now it's all misery and pain. Apart from the fact that I don't understand it I think I'm not interested.
The worst bit is that it consists of student presentation, some of which are an imposition.

@AsafKaragila oh my god, you're right... I don't even know who I am anymore!

6:03 PM
-> pain to the n
@AsafKaragila: Have you considered psychological treatment?

@AlexeiAverchenko You are an element of the empty set.

: )

@Matt For Alexei? Why would I have to pay for that? He's the one without any fathers.

@AsafKaragila For yourself, I meant, obviously. : )

@AsafKaragila because the statement 'Asaf is Alexei's father' is vacuously true

6:05 PM
@Matt Oh. I see no reason to treat myself. Nothing wrong with me, only with "reality".

@AsafKaragila Funny, I've been thinking exactly the same.

@AlexeiAverchenko Wrong, the assertion 'If Alexei has a father then it is Asaf' is vacuously true. The claim you wrote is a false claim.

but i don't exist!

The set of fathers is empty, and you claim that I am a member of this set. Contradiction, let's go home.

@tim: ms.uky.edu/~jack/2011-11-22-DefenseSkeleton.tex is fully functional. sectioning requires several passes of pdflatex or xelatex to get everything right

6:06 PM
so for any alexei you are his father!

@AlexeiAverchenko The fact that you do not exist has nothing to do with me. This is clearly your problem and you must deal with it on your own.

@AsafKaragila it has everything to do with you, dad

@tim: i learned to do this by reading source code of tex packages mostly and asking other presenters for source code of their presentations

@AlexeiAverchenko Does not.

Awww, cute. He's calling you dad.

6:09 PM
@Jack: Thanks! After correction, it compiles now. How was the code for those lovely headings of each page with outlines and clickable links like?

@Matt I can't remember when I didn't! But it are only small quantities.

@AsafKaragila Alexei.

@Matt he doesn't understand me! He says I can't hang out with my friends after 10 pm or do category theory!

@Matt But he does not exist, how can he be calling me 'dad'?

6:10 PM
it's so uncool!

@JonasTeuwen I quit the drinking about 10 days ago : )

@Matt again? ;)

@AlexeiAverchenko Indeed, again.

@Tim handled automatically by beamer, the code is just the section (and subsection, grr) commands. it may require 3 or 4 passes of (pdf|xe)latex to get them working

Regarding your little family reunion: I don't know what to say : D

6:13 PM
i need to append the following to my user description: "Also, I don't exist."

@Jack: Got it. Now it looks great. Thanks! I feel so much to learn.
@Matt: "little family reunion" co-smile.

I'm learning laplace's method right now. I think @robjohn used it to solve my integral, and zarrax has phrased it again for me to compare. en.wikipedia.org/wiki/Laplace's_method

hi

hi

6:17 PM
hi?

@JonasTeuwen: Hahaha, "Henning looks so manly"? : D
I think he needs a shave.

6:31 PM
Interesting, now Jack's having the monopoly on the starred messages bar :) Can't the König do something about this?

whoah, someone went and starbombed his comments

He can, but he won't.
I am not the sort of Koenig that uses his power. Except for evil.

@JackSchmidt Which of Laplace's methods? Least squares?
@AsafKaragila And we both have comments pinned there, so why should we care? ;-)

@robjohn: if f has a maximum at 0, then f = f(0) + f"(0) * x^2, so integral exp( Mf(x) ) dx is very nearly the standard erf integral where you expect to get sqrt(pi/2)

@JackSchmidt Ah, stationary phase then.

6:36 PM
:P

@Matt That is why he looks so manly.
Hmm, my off-diagonal estimates fail for C_k(B) for k = 0 (which = B) :-). Well, those are not really off-diagonal estimates of course as they are not disjoint. Fix!

The librarian just called the computers "lie-nux"...

@anon better than eunuchs

How about you help me do some mathematical philosophy? Maybe if I share the misery it becomes more bearable...
One of the questions is "Under what conditions can Hilbert decide for an arbitrary mathematical theorem wether it can be proved from a given set of axioms or not, given the "halting problem" for second order logic has been solved?"

@Matt the key to philosophy is drinking

6:44 PM
I think the answer to this should be "If the theorem and the axioms can be expressed in second order logic."

> the "halting problem" for second order logic has been solved
is that a hypothetical?

No
It's solved for first order logic.

what theorem is it referring to?

Given an arbitrary logical formula, decide whether it's satisfiable or not.
I think. I'm not sure because I don't think I really understand the texts.

maybe it mistranslated decision-problem for halting-problem?

6:47 PM
Ah. Yes, you're right.
Decision problem.
@AlexeiAverchenko: That will explain why I don't like mathematical philosophy.
I take this silence to mean that I put all of you to sleep with my philosophical interlude.

@Matt Hilbert can't decide anything now; he's been dead for 50+ years. Are there words missing here?

Just analytically continue him into the 21st century.
2

I don't know what you mean by that.

You wrote "Under what conditions can Hilbert decide ...", and it's unclear to me who or what is doing the deciding.

I don't think second order logic is decidable

6:55 PM
@tb Ok, taken care of that now =)

@QED: I don't think it is either. I think the question is saying, "assume it was..."

but you can't assume something like that
since it's false

@HenningMakholm: "Can Hilbert decide..." makes "Hilbert" the subject of the sentence. What's unclear?
@QED: I guess that's called philosophising. : )

Hilbert died in 1943. He can't decide anything anymore. Or do you mean something else by "Hilbert" than David Hilbert (1862-1943)?

I don't think philosophy is just nonsense

6:58 PM
@HenningMakholm: I didn't write the questions.

where did this come up?

In a course called Mathematical Philosophy.

is the question in german?
or not-english

@Matt Nevertheless, the question as you quote it appears to be nonsense. I'm guessing that perhaps you have access to some information that can help de-nonsensify it.

I was thinking it might make sense if I could see the whole thing but I can't read any other languages

7:00 PM
Well, I could give you a verbatim translation but I don't think I changed the meaning.
OK, let's do that:

For example, is "Hilbert" the name of a particular logical system or imaginary device you're considering in the course?

It's David Hilbert.

And we're asking for conditions that would allow David Hilbert to decide such-and-such?
Or would have allowed him to decide it had he been alive still.

Verbatim: Under what conditions can Hilbert say, that one can decide for any given mathematical theorem, whether it is provable from a given set of axioms or not, assuming that the "decision problem" for second order logic is solvable?
@HenningMakholm: Would have allowed.

@Matt, if I was in your situation I would just reject the question for the reason I gave earlier

7:04 PM
Rejection would be too much work. I just want to get it over with.

really??
just write "the question is wrong because second order logic is undecidable"

My best guess is that the teacher must have meant: "Hilbert did say that if the decision problem for second-order logic is solvable, then we can decide for any given mathematical theorem, whether it is provable from a given set of axioms or not. What was his justification for claiming this?"

Yes, really. Why the surprise? Maybe if I write something nonsensical enough he thinks I'm a philosopher, too : D

@tb Can you explain the notation used here: math.stackexchange.com/questions/84526? My comment there should explain my confusion. But from the responses (or lack of them, thereof) it looks like I am one who's mistaken. =) Thanks.

@HenningMakholm: No. The question is purely hypothetical.

7:05 PM
you're doing the school game where you have to guess what teacher wants instead of being sensible
I don't think it's really healthy to keep that up just to get good marks

I assumed that's what philosophy is like.
No, I'm not about good marks. I just want a pass.

no, it's not just nonsense

The course is agony.

did you choose it voluntarily?

Yes. Thinking that it might be interesting.

7:07 PM
ah well hopefully it will pick up

@Matt Why are you sure of that? It seems to be strange to ask for hypothetical conditions for allowing David Hilbert specifically to say something or other, rather than an arbitrary rational mathematician or whatever.

@HenningMakholm: No, I don't see anything strange about it at all.

@Srivatsan The notation in the question looks quite wrong to me...

@tb I am not surprised. =) Except about the bit that Davide did not catch it...

It's the limsup in the lattice of closed sets to me, as far as I can tell.

7:11 PM
@Matt Please explain to me what it means, then.
Why would there be different conditions for David Hilbert being able to say such-and-such than for, say, Gödel or Tarski to say the same thing?

@HenningMakholm: Now I understand what you're on about. Hilbert is the lecturer's favourite. I think you can replace Hilbert there with your favourite character.

Because Tarski invented the truth!!

@tb Um, I couldn't get those precise words. Nice way to put it. // Thanks @tb

2B or not(2B). That is the truth!

@HenningMakholm: I understand the question as follows: Assume Hilbert is alive and the decision problem for second order logic has been solved. Give Hilbert any mathematical theorem plus a set of axioms. Question: What do you need to assume in order for him to be able to prove or disprove the theorem?

7:17 PM
Well, first he needs to be really smart ... but it sounds like you can get away with assuming that, because David Hilbert is David Hilbert.
Second, I think it is reasonable to require that there's a second-order logic formula that determines whether any given string of symbols belongs to the given set of axioms or not.

Ah, good point.

@tb This post is also related although I don't quite follow the comment thread: math.stackexchange.com/questions/17318. See the comments.

On the other hand, if that is true, then you can encode provability as a second-order arithmetical sentence using the techniques of Gödel (1931).
Also, the natural numbers (needed for Gödel's construction) have a complete description in second-order logic (which is not true in first order logic).
Put these two components together with the theorem you want to prove, and you get a second-order sentence that is true iff the theorem is provable. Stick that sentence into your assumed second-order-logic oracle and crank its handle.

@Srivatsan You're surely aware of the notation a \vee b = max{a,b} (= sup{a,b}) and a \wedge b = min{a,b} (= inf{a,b}) now replace union by vee (and closure) and intersection by wedge and you get inf sup which is the lim sup.

@tb Yes, I do. Since my clarification was overridden by the OP in the first post, I thought I must ask others explicitly.
As long as I am missing something fundamental, I am not worried. Thanks...

7:25 PM
Here I'm assuming that "the decision problem for second order logic has been solved" means that we have a procedure for determining whether a given sentence of second-order logic is standardly valid or not.

@HenningMakholm: yes, exactly that.

@Srivatsan I like that missing "not" :)

Gödel proved that we're always missing something fundamental.

@tb People complain that I use too many negations. It's good that I decided to throw out a random sample. =)

7:29 PM
@HenningMakholm You mean to the axioms or anything provable from the axioms?

@Matt (I was merely free-associating to Srivatsan's missing negation, not addressing your problem there)

7:48 PM
@HenningMakholm: I think the answer to the question is that: assuming Hilbert can express any mathematical theorem using second order logic language then due to Gödel's first incompleteness theorem there will be a theorem that is true but cannot be proved. So he gets a contradiction to having a state machine that either proves or disproves any theorem.

Is "assuming Hilbert can express any mathematical theorem using second order logic language" a new assumption? It is different from the problem's assumption that Hilbert can decide whether a second-order formula is standardly valid. (I think you have an outline for a valid argument that the problem's assumption is false, but it is not clear to me that it would be accepted as an answer for that reason).

@HenningMakholm: Yes, it's an additional assumption I made. I think I'm allowed to make any additional assumptions I like.

True : D
Maybe that is intended by the lecturer.

It is possible that you can fish for extra points by pointing out that the assumption in the problem has been proved to be false. But I wouldn't count on it as a way to earn the main points of the exercise.
FWIW, I think my comment up here is the intended answer.

8:00 PM
This comment is what you claimed here was referring to Srivatsan's missing negation.

I know. So what do you say to what I said there?

What I meant was that if the axioms can be described by a second-order-logic formula, then there's a different second-order formula that describes all theorems (and the latter formula can be constructed using Gödel's artihmezation of deduction).
Therefore my proposed answer is that it's enough that the axioms can be described by a 2OL formula.

Anybody think would be useful as its own tag?
Well, I think it would be, so Imma go ahead and make it.

It would be slightly more useful than (mass-point-geometry).

8:08 PM
lol... not sure how to take that. But I've seen a lot of questions on regularizing sums so it'd seem better than a lot of tags I see exist.

@anon What does this term mean?

making divergent sums/products/integrals into manageable values or forms.

@Srivatsan: It means if someone doesn't fit in then you regularise them.

it's how you ignore infinities in modern physics :)

@Matt Well, mass point geometers seem like a nice target. =)

8:10 PM
: D

@anon Any example posts from mse?

One of my questions, all of the -1/12=1+2+3+... questions, all of the things on Ramanujan summation...

@anon I thought you were merely making fun of the recent transient chunk of such questions. I wouldn't have thought myself that they are frequent enough to need a tag, but don't let me stop you.

Oh, wow. 490 posts mentioning Ramanujan summation.

@HenningMakholm: Ok. Thanks. Enough philosophy for today ; )

8:12 PM
@Sri: See, I told you ;)

@anon =) I am convinced.

@Srivatsan And so many more that don't...

@AsafKaragila That calls for a [non-regularize] tag.

@Srivatsan Next thing we'll have

And after that we'll have . Oh wait...
Hmm. Started my first bounty, lost a chunk of rep instantly. Interesting.

8:21 PM
@anon Drums

Yes, it's documented as non-refundable.

@anon Your first bounty? At least you will get a badge, I believe... "anonymous benefactor" =)

Hmm, maybe it wasn't such a good idea to create "regularization" when there's already "divergent-series" ...

Hmmm. I just noticed how awful my ability to calculate. I thought that I could hit 80 answers when the AC tag hits 100. I will only hit 70. I need to write 10 answers on past questions if I want to hit silver badge when the tag hits 100 questions.

Also, chromium crashes over a single youtube video. jeez this is a bad comp.

8:51 PM
@tb @t.b.: What does "It's the limsup in the lattice of closed sets" mean?

I am so tired...

I don't know what you're referring to, but it sounds (conceptually) like the smallest set containing all closed sets

@anon: Are you replying to me? if yes, the smallest set containing all closed sets would be the universal set. I am referring to one of t.b.'s comment in chat today.
@AsafKaragila: maybe time to sleep.

I suppose the lattice is formed by inclusion being the \le relation. The limsup would then be the highest possible item in the lattice, or something that contains any element that is in one of the lattice's sets, or something to that effect.

I have to prepare the class for tomorrow.
Do we still close puzzle questions?

8:55 PM
@Tim: do you know the definition of limsup for real sequences? That can be reinterpreted to define the limsup of a sequence of closed sets.
Giving something like: the closure of the set of points that are in infinitely many of the sequence of closed sets.

Oh, so would "any point such that every set in the lattice above a certain level contains that point" be the limsup?

@anon @Henning: t.b. said that sentence regarding this question math.stackexchange.com/questions/84526/…. He felt the OP is wrong about the definition.

@Tim A lattice is a partially ordered set in which supremum and infimum of finitely many sets exist. anon and Hendrik hit the nail on the head.

@HenningMakholm: How does "the closure of the set of points that are in infinitely many of the sequence of closed sets" look like in a math formula?

@Tim Yes, a cap of cups looks like a limsup rather than a liminf.

8:59 PM
@Tim Exactly what's written there and called "lim inf"

lol

@HenningMakholm: funny. How would you write a formula to explain that?
@t.b.: Would you write a formula to mean "It's the limsup in the lattice of closed sets"?

@Tim \limsup C_n = \overline{\bigcap_{n=1}^\infty \bigcup_{m=n}^\infty C_m}

@HenningMakholm: Thanks! What about \liminf C_n

@Tim: "@t.b." doesn't ping, you have to use "@tb".

9:04 PM
(sorry for the animated formula. Didn't notice that the question was edited just as I was trying to copy from it)
@Tim Just switch caps and cups.

...

I don't think it matters whether the closure is taken before or after the intersection. But I'm a bit tired.

Oh man. I just realized that I wrote the long forms in one of my questions without realizing what they were called.

Thanks, @tb, @Henning, @Matt. Writing LaTex in chat is painful, isn't it?

Doug Spoonwood sure likes Polish notation.
2

9:18 PM
@tb: why is limsup defined as in your formula? Is it equivalent to "xâˆˆlimâ€†supAn if and only if there exists a sequence of points {xk} and a subsequence {Ank} of {An} such that xkâˆˆAnk and xk→x as k→âˆž." (Quoted from Wiki)

@HenningMakholm It does. Let a_n be an enumeration of the rationals. Put A_n = \{a_n\} as subsets of the reals. Then what you write is empty while what I write is the entire set of reals.

@tb Oh, of course.

@HenningMakholm: Sorry, I have to ask the same question to you. why is limsup defined as in your formula? Is it equivalent to "xâˆˆlimâ€†supAn if and only if there exists a sequence of points {xk} and a subsequence {Ank} of {An} such that xkâˆˆAnk and xk→x as k→âˆž." (Quoted from Wiki)

@Tim That definition from Wikipedia works well in metric spaces, otherwise it's no good.

9:21 PM
@Tim Well, as t.b. pointed out, it isn't. It was supposed to capture "The limsup is the greatest lower bound of all points in the lattice that are above all but finitely many elements of the sequence".

@tb: Do you mean the Wiki def is equivalent to yours in metric space? I see the Wiki def does not require metric, but only topology.
@HenningMakholm: Where is that quote from?

It's not a quote.
Just what I remember about the limes superior of real sequences, expressed order-theoretically.

I don't know why Wiki writes what it writes.

The trouble with Wikipedia math articles is that they're written by volunteers quoting a bit a time from their favorite textbooks, with very little time invested by anyone in keeping the complete result internally consistent.

@HenningMakholm: I do know that. But I think having it is better than none.

9:29 PM
Sometimes you end up having roughly equivalent concepts (each with their articles) defined in terms of each other, so the entire development rests on nothing.

@tb: Since you gave limsup, what is liminf? Do you mind if there are some references?

I don't know really good references on this. Maybe Birkhoff and Mac Lane's algebra contains something and the other reference I know that might contain something is Johnstone's Stone spaces. But I haven't looked at those books in a long time.
I would say this is the liminf:

Isn't there a standard definition, at least in probability?

@tb: Thanks! So is your definition of limsup and liminf those used in real analysis?

It's what makes sense in lattice theory. If you say \bigsqcup instead of \overline\bigcup and \bigsqcap instead of \bigcap, you get a set of nicely dual general definitions. This also generalizes the real limsup and liminf when the reals are given their usual ordering.

9:37 PM
@HenningMakholm: I don't see duality in the defintions that tb gave.
could you write the complete formulas for what you meant?

@Tim Every \bigcup takes an overline because we're working in the lattice of closed sets. The duality exchanges \overline\bigcup with plain \bigcap.

Alternatively, we just put closures everywhere, even when unnecessary.

@ZhenLin The one used in probability is the limsup and liminf in the measure algebra (which is a lattice with respect to inclusion almost everywhere).

@HenningMakholm: I don't see why limsup and liminf can only apply to a sequence of closed sets. They are used for a seq of any sets.

Alternatively study FM-models.

9:39 PM
@tb: Actually, the one I remember uses plain unions and intersections, but I guess that's because we only ever needed countably many operations...

Imagine a big tree with branches, with the trunk going to single lower point x. Now make a copy of it, put it upside down and connect it with the original tree by their outstanding branches. Now you have a lattice. taking the join is like flipping it upside down and taking the meet.

@Tim Of course they can. In the present case someone has chosen that we're only looking at closed sets for some reason or other.

limsup = inf sup and liminf = sup inf, that's all there is to it.

Indeed.

@tb: I agree. But in the context of topology, the definitions change accordingly to include closure, for example as those you gave.

9:41 PM
@Tim: There is no change, because inf and sup are defined in terms of the (complete) lattice in question.

@Tim It's just a matter of there being several different complete lattice structures that we can choose to work with. Each lattice comes with its own limsup and liminf.

@ZhenLin: There is. See the definitions tb gave

@Tim: In the lattice of closed sets, sup is defined to be the closure of the union.

Okay I may miss something. What is the (complete) lattice in a topological space? How is it different from the power set?
what is inf then?

@Tim, there is no such thing as "the" complete lattice.

9:43 PM
This whisky keeps surprising me.

One complete lattice is the lattice of all closed set under inclusion.

@Tim: The lattice of open sets is a complete lattice, as is the lattice of closed sets.

Another one would be the lattice of all open sets under inclusion.

Matt! Jonas is drinking again!

A general fact about lattices is that if they have all infima, or all suprema, then they are already complete.

9:44 PM
Oh no! Call the moral police!

The lattice of all sets under inclusion is also complete, but is unrelated to the topology.

@ZhenLin: What are inf and sup? in the lattice of closed sets , and in the lattice of open sets?

@tb I was just about to comment on that : D Now I won't.

@ZhenLin I thought that was the definition of complete.

@Henning: I think categorically, so the definition of complete lattice means they have all infima and suprema.
@Tim: In the lattice of closed sets, inf is just the usual set-theoretic intersection. In the lattice of open sets, inf is the interior of the set-theoretic intersection.

9:46 PM
@JonasTeuwen What does it smell like today, rotten mice tails?

@ZhenLin Sorry, I didn't see the "or". You're right.

@tb No. Liquorice!

Although, perhaps I should say bicomplete lattice for such a thing, to make a better analogy with categories...

@JonasTeuwen ah, finally something desirable.

Also, fun fact: the lattice of open sets of a topological space does not, in general, contain enough information to recover the original space. Studying these lattices leads to pointless topology.

9:49 PM
One of the more aptly named subjects :)

Locales are very nice!
(supposedly)

Have you ever needed to consider a non-sober space in "practice"?

Hausdorff spaces are trivially sober, and the underlying space of a scheme is sober, but classical algebraic varieties with the Zariski topology are not sober...

So you're saying Zariski is not sober?

Who invents these names?

9:52 PM
Drunk people :D

Espace sobre is due to Grothendieck, I believe.

There seems to be something called "stoned duality" beetween sober spaces and spaced frames.
3

reminds me of that one MO thread. "annihilating free radical ideals" or whatever, heh.

@tb Really? Surely they must have been considered by, say, Stone.

@AsafKaragila Zhen and you should rewrite the Philosophers Song. Oskar Zariski was often tipsy and very rarely stable...

9:55 PM
@tb I don't even know what the Philosophers Song is.

A gap in the Monty Python knowledge!

Then again, perhaps it's not surprising that the name is due to Grothendieck. He has a penchant for amusing names.

@ZhenLin Stone only considered the spectra of Boolean rings, I believe. The abstract framework of frames and locales was only developed after topos theory was invented. It's somewhere in SGA that the name appears, if memory serves me.

Such things makes it rather amusing to learn logic from Mendelson's book. He has a habit of saying things like "we call a formula grotesque if blah blah yada" and you never know whether it's a throwaway definition just for stating an exercise, or the presentation of a well-known technical concept.

When I first heard about Counterman order types I asked if it was a joke of some sort. Then I was told that it is actually the name of a mathematician that worked with Shelah and whatnot, but no one really met him or something like that.

9:59 PM
@tb Ah, I see. That makes some sense... I'm not really sure what the motivation for pointless topology is, really. Sites for sheaf toposes is a plausible one, I guess. But I thought there was some connection with constructive mathematics as well.