1,158 reputation
11116
bio website people.su.se/~cesp
location Stockholm, Sweden
age
visits member for 3 years, 6 months
seen 1 hour ago

I'm a graduate student deeply interested in foundations (logic, set theory, model theory, metamathematics) and category theory.


Aug
17
comment How short can we state the Axiom of Choice?
It seems to me that François' solution is near optimal, considering that all usual equivalents of AC (which are gather in Rubin & Rubin's book rather than in Jech's), use notions which, when unwound in the language, are considerably larger.
Aug
13
comment Relationship between fragments of the axiom of choice and the dependent choice principles
Oh, good, then I won't have to go to the construction myself :) I just had read that it was Solovay who proved result 3 in this model. So now the real challenge is result 4, since the book only mentions permutation models for that.
Aug
13
comment Relationship between fragments of the axiom of choice and the dependent choice principles
Sure, the book refers to page 166 of Felgner, U. "Models of ZF set theory", Springer-Verlag, Berlin. I run into this model from the "Consequences..." web page, where I just searched for something validating form 40 ($\forall \kappa AC_{\kappa}$) but not form 44 ($DC_{\omega_1}$) and that was not a permutation model.
Aug
13
comment Relationship between fragments of the axiom of choice and the dependent choice principles
Oh, I'm referring to the model $\mathcal{M}13$, called in the book "Feferman/Solovay", it's just one model which extends $\mathcal{M}2$, called "Feferman" model there. Are we using different terminology or you meant to say something else?
Aug
13
comment Relationship between fragments of the axiom of choice and the dependent choice principles
I've just checked Howard-Rubin and it seems that at least for result 3 it can be done as Asaf says; Feferman/Solovay model does the trick. You have to add $\omega_1$ generic reals to the base model without collecting them in a set. For result 4, however, it seems the only available model is Jech's permutation model...
Aug
13
comment Relationship between fragments of the axiom of choice and the dependent choice principles
The references seem to be interchanged: 3 corresponds to Theorem 8.9 and 4 to Theorem 8.12
Aug
11
comment Can one live without actual infinity?
I think the distinction lies on the cognitive aspect rather than on the mathematical one. I understand the quote as expressing that mathematical concepts are necessarily finitistic and that looking for examples in the physical world of an actual infinity is doomed to fail; saying space or time are infinite is not the same as saying they are unlimited. The second is a finitistic notion, while the first simply does not make sense.
Aug
11
awarded  Good Answer
Aug
9
awarded  Nice Answer
Aug
9
answered Examples of unexpected mathematical images
Jul
11
comment How does one justify funding for mathematics research?
Wow, that's a reminder that it's not the individual who is important, but the species. Interesting.
Jul
11
comment How does one justify funding for mathematics research?
@Asaf: Those are quite big jumps you're making there. It's not clear to me that saving people's lives could rely on measure theory, topology or large cardinals
Jul
4
awarded  Civic Duty
May
3
comment Is it possible for a theorem to be constructive only in a non-constructive metatheory?
@Ingo: Thanks a lot for this material! I'll study it, and if there are questions to discuss I'll contact you privately
Apr
30
comment Is it possible for a theorem to be constructive only in a non-constructive metatheory?
@Ingo: That is very interesting, thanks! I would be certainly interested in reading the details, as well as the topology that you need to use for Friedman's translation
Apr
29
comment Is it possible for a theorem to be constructive only in a non-constructive metatheory?
@Zhen: I believe the methods of Erik's proof could be adapted as soon as one develops a sort of geometric version of Gödel-Gentzen negative translation (and Friedman's translation as well). Note, however, that this would only eliminate the uses of excluded middle in the proof, and does not answer whether eventual uses of stronger principles, like, e.g., the axiom of choice, could also be eliminated.
Apr
29
comment Is it possible for a theorem to be constructive only in a non-constructive metatheory?
Eduardo, I think you're confusing two issues here. One is the conservativity result of Barr's theorem, which has a classical topos-theoretic proof, and another whether that result can be established in a constructive metatheory. Also I don't understand your last sentence, "...since we accept the conclusion as true without requiring any other proof"
Apr
29
comment Is it possible for a theorem to be constructive only in a non-constructive metatheory?
Erik Palmgren, in "An intuitionistic axiomatisation of real closed fields" (MLQ, 2002) indicates a proof-theoretic proof by showing that coherent sequents are stable under the Dragalin-Friedman translation. Another proof is given in Sara Negri's "Contraction-free sequent calculi for geometric theories with an application to Barr's theorem" (Arch. Math. Log. 2003) using cut-free systems for the coherent fragment (Warning: In Negri's paper she calls geometric theories/implications what should actually be called coherent theories/sequents)
Apr
29
comment Is it possible for a theorem to be constructive only in a non-constructive metatheory?
Regarding the coherent version of (2), there exists a constructive proof of conservativity of classical logic over coherent logic, and thus every coherent sequent provable classically from coherent axioms admits already a coherent proof and this is established constructively.
Apr
1
accepted Is every Heyting algebra the Lindenbaum algebra of an intuitionistic first order theory?