Timeline for Is every Heyting algebra the Lindenbaum algebra of an intuitionistic first order theory?
Current License: CC BY-SA 3.0
6 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Apr 1, 2014 at 14:55 | comment | added | godelian | 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, 2014 at 14:43 | comment | added | Joseph Van Name | I explained why quantifier elimination works in this theory. | |
| Apr 1, 2014 at 14:29 | history | edited | Joseph Van Name | CC BY-SA 3.0 |
added 131 characters in body
|
| Apr 1, 2014 at 12:58 | comment | added | Joel David Hamkins | Very nice argument! | |
| Apr 1, 2014 at 7:51 | comment | added | godelian | Hi Joseph, very nice! Could you expand a bit on why $T$ has quantifier elimination? | |
| Apr 1, 2014 at 5:32 | history | answered | Joseph Van Name | CC BY-SA 3.0 |