958 reputation
11015
bio website people.su.se/~cesp
location Stockholm, Sweden
age
visits member for 3 years, 5 months
seen 6 hours ago

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


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?
Apr
1
revised Is every Heyting algebra the Lindenbaum algebra of an intuitionistic first order theory?
added 162 characters in body
Apr
1
comment Is every Heyting algebra the Lindenbaum algebra of an intuitionistic first order theory?
Excellent! So $H$ need not be complete since the domain just contains one element.
Apr
1
comment Is every Heyting algebra the Lindenbaum algebra of an intuitionistic first order theory?
What about the injectivity of the map? I see how to prove it using BPI, but did you have a choice free proof in mind?
Apr
1
comment Is every Heyting algebra the Lindenbaum algebra of an intuitionistic first order theory?
Oh, I see...so every finite subset of the axioms is satisfiable since one can find an ultrafilter (without choice) in the countable subalgebra generated by the elements of $H$ they involve. But then the theory is indeed consistent...
Apr
1
comment Is every Heyting algebra the Lindenbaum algebra of an intuitionistic first order theory?
François, I think this could work once you prove that your theory is consistent (otherwise the map is not injective), maybe there one needs BPI. Besides that, I think this works, doesn't it?
Apr
1
comment Is every Heyting algebra the Lindenbaum algebra of an intuitionistic first order theory?
Thanks! I'll check the paper to see if it helps.
Apr
1
comment Is every Heyting algebra the Lindenbaum algebra of an intuitionistic first order theory?
Excellent, thanks! I tried to see if this argument could be used for the Heyting case, adding the condition $c_a \to c_b=c_{a \to b}$, but the only problem is that when you want to prove that $L$ is injective one should use Heyting algebra homomorphisms, which correspond to ultrafilters if the codomain is $2$. Unfortunately, ultrafilters (unlike prime filters) do not separate points in the Heyting case (for instance, they do not distinguish between $1$ and an instance of excluded middle)
Apr
1
revised Is every Heyting algebra the Lindenbaum algebra of an intuitionistic first order theory?
added 525 characters in body
Apr
1
comment Is every Heyting algebra the Lindenbaum algebra of an intuitionistic first order theory?
I was rather thinking on sentences, so it's ok. I'm however not sure if this could be generalized to the Heyting case since it seems to rely on the fact that $b \vee \neg b=1$
Apr
1
comment Is every Heyting algebra the Lindenbaum algebra of an intuitionistic first order theory?
Hi Joseph, very nice! Could you expand a bit on why $T$ has quantifier elimination?