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