953 reputation
1915
bio website
location
age
visits member for 3 years, 2 months
seen 16 hours ago

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}$.