bio | website | |
---|---|---|
location | ||
age | ||
visits | member for | 3 years, 2 months |
seen | 16 hours ago | |
stats | profile views | 1,159 |
I'm a graduate student deeply interested in foundations (logic, set theory, model theory, metamathematics) and category theory.
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? |
Apr 1 |
comment |
Sigma-complete Lindenbaum algebras?
@Joel: That sounds interesting! I posted a new more general question here mathoverflow.net/q/162007/12976, but of course you are welcome to answer it for the Boolean case. |
Apr 1 |
asked | Is every Heyting algebra the Lindenbaum algebra of an intuitionistic first order theory? |
Mar 31 |
comment |
Sigma-complete Lindenbaum algebras?
Yes, that was the assertion I was referring to. Is that true? Sorry, I cannot see it immediately, perhaps it's obvious to you... |
Mar 31 |
comment |
Sigma-complete Lindenbaum algebras?
Joel, do you have a proof of your first assertion? for propositional theories is obvious, but for a first-order theory I'm not even sure it's true... |
Mar 7 |
answered | Sum of digits of repeating end of reciprocal of prime over period is $\frac{9}{2}$ |
Feb 14 |
awarded | Yearling |
Feb 10 |
comment |
Godel's Second Incompleteness theorem and Models
Note that even if $\Gamma$ is consistent, it could still prove $\neg \mathcal{C}on(\Gamma)$, so the situation is different from the usual undecidable sentences. Also, the second incompleteness theorem assumes as hypothesis (among others) that $\Gamma$ is indeed consistent, so while you will have at least one model where $\mathcal{C}on(\Gamma)$ does not hold, your theory is still consistent though, it's just that this particular model is not "aware" of it. |
Jan 26 |
comment |
Characterization of Angles Trisectable with Straightedge and Compass
The example I gave shows that there can be no general procedure for trisecting a given angle, whether that angle is constructible or not. It does not appeal to the transcendence of $\pi$; Lindemann's proof settles the question of the impossibility of squaring the circle, but is not needed to show the impossibility of trisecting an angle. |
Jan 26 |
comment |
Characterization of Angles Trisectable with Straightedge and Compass
The problem of the trisection of the angle has been settled much before Lindemann's proof, since while the angle $\pi/3$ is constructible, $cos (\pi/9)$ satisfies a degree 3 irreducible polynomial over $\mathbf{Q}$. |