@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.
@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
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
@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)
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!
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 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.
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?
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?"
@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.
@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: 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.
@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?
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.
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.
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: 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).
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.
Argh, no, that was this one. I missed the backlink on your question, sorry. Clearly I couldn't have commented on Srivatsan's statement before I made it.
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.
@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.
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.
@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.
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.
@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.
@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 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".
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.
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.
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.
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.
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 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.
@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.
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.
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...
@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.
@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.
