bio | website | people.su.se/~cesp |
---|---|---|
location | Stockholm, Sweden | |
age | ||
visits | member for | 3 years, 6 months |
seen | 1 hour ago | |
stats | profile views | 1,200 |
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 ﬁelds" (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? |