Timeline for Is every Heyting algebra the Lindenbaum algebra of an intuitionistic first order theory?
Current License: CC BY-SA 3.0
9 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Apr 2, 2014 at 8:17 | comment | added | მამუკა ჯიბლაძე | So simple!! This must easily extend to second order using Pitts quantifiers. Do you understand what are obstacles to go even higher this way? | |
| Apr 1, 2014 at 19:05 | vote | accept | godelian | ||
| Apr 1, 2014 at 19:00 | comment | added | godelian | Excellent! So $H$ need not be complete since the domain just contains one element. | |
| Apr 1, 2014 at 18:14 | comment | added | François G. Dorais | @godelian: There is an $H$-valued model that separates all equivalence classes. | |
| Apr 1, 2014 at 17:30 | comment | added | godelian | 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, 2014 at 17:10 | comment | added | godelian | 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, 2014 at 16:53 | comment | added | François G. Dorais | @godelian: In the classical case, that the theory is satisfiable is equivalent to BPI, but no choice is needed to see that the theory is consistent. | |
| Apr 1, 2014 at 16:50 | comment | added | godelian | 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, 2014 at 16:28 | history | answered | François G. Dorais | CC BY-SA 3.0 |