Timeline for Constructive compactness for countable models?
Current License: CC BY-SA 3.0
30 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Nov 5 at 14:20 | history | edited | Mikhail Katz |
edited tags
|
|
| Apr 13, 2017 at 12:58 | history | edited | CommunityBot |
replaced http://mathoverflow.net/ with https://mathoverflow.net/
|
|
| S Feb 8, 2016 at 9:10 | history | bounty ended | Mikhail Katz | ||
| S Feb 8, 2016 at 9:10 | history | notice removed | Mikhail Katz | ||
| Feb 8, 2016 at 9:10 | vote | accept | Mikhail Katz | ||
| Feb 8, 2016 at 9:09 | answer | added | Semen Kutateladze | timeline score: 1 | |
| Feb 8, 2016 at 7:51 | history | edited | Mikhail Katz | CC BY-SA 3.0 |
added 103 characters in body
|
| Feb 7, 2016 at 13:34 | history | edited | Mikhail Katz | CC BY-SA 3.0 |
added 192 characters in body
|
| Feb 7, 2016 at 10:01 | history | edited | Mikhail Katz | CC BY-SA 3.0 |
added 10 characters in body
|
| Feb 4, 2016 at 17:21 | comment | added | Mikhail Katz | @Peter, thanks. It may make sense to convert these to an answer. | |
| Feb 4, 2016 at 17:12 | comment | added | Peter LeFanu Lumsdaine | On the other hand, while constructive model theory casts its net much wider than classical model theory (including Kripke models and much more), it certainly includes ordinary “Tarski” models as a special case of these. So there is no problem with speaking of “compactness for (countable) (Tarski) models”. The reason Tarski models are less-studied constructively isn’t because they’re problematic, it’s just that there may not exist enough of them for completeness, so one is forced (no pun intended) to look at more general kinds of models. | |
| Feb 4, 2016 at 17:07 | comment | added | Peter LeFanu Lumsdaine | I don’t know the answer, I’m afraid; but unlike other commenters, I think this is a good and well-posed question. Formal constructive reverse mathematics has been investigated by e.g. Ishihara, Nemoto, and colleagues, who have certainly considered what intuitionistic formal systems are required for equivalences between WKL, LLPO, and related principles; I have heard several conference talks by them on such issues, though I don’t remember their results precisely. (cont’d) | |
| Feb 4, 2016 at 15:37 | history | edited | Mikhail Katz |
edited tags
|
|
| S Jan 31, 2016 at 15:35 | history | bounty started | Mikhail Katz | ||
| S Jan 31, 2016 at 15:35 | history | notice added | Mikhail Katz | Draw attention | |
| Jan 24, 2016 at 21:26 | comment | added | Vladimir Kanovei | Being a total ignorant of constructive mathematics, still it seems that any sort of "constructive NSA" would better be developed syntactically rather than model-theoretically, e.g. something like a baby-IST under intuitionistic logic | |
| Jan 21, 2016 at 8:13 | comment | added | Mikhail Katz | @ErfanKhaniki, sticking to lower-level models, it would be interesting to establish in what constructive setting things like compactness, WKL, and LLPO are equivalent. There seems to be disagreement among editors in the comments above about what is needed here. One editor seems to think that this requires ZF, while another seems to think that a weaker system would suffice. I would appreciate any clarification. | |
| Jan 21, 2016 at 8:11 | history | edited | Mikhail Katz | CC BY-SA 3.0 |
added 264 characters in body
|
| Jan 20, 2016 at 21:24 | comment | added | Erfan Khaniki | @katz: you are right, there exists a second order axiomatization for BISH, but your question is about countable model, which needs a framework for model theory and I don't see any model theory framework for BISH. It is an axiomatization with intutionistic logic as underlying logic | |
| Jan 20, 2016 at 16:14 | history | edited | Mikhail Katz | CC BY-SA 3.0 |
added 164 characters in body
|
| Jan 19, 2016 at 14:29 | comment | added | Mikhail Katz | @CarlMummert, could one ask such a question with regard to your axiomatisation? | |
| Jan 19, 2016 at 11:23 | comment | added | Carl Mummert | @katz: I would find that quite surprising. One common aspect of constructive mathematics is an avoidance of formalization, and of formal systems in general. Sometimes logicians like myself will impose a particular axiomatic framework on BISH, but strictly speaking this is a departure from the intentions of the authors. Even in constructive reverse mathematics the base system is often unspecified. | |
| Jan 19, 2016 at 8:47 | comment | added | Mikhail Katz | @ErfanKhaniki as far as I know Douglas Bridges (Bishop's coauthor) does have a specific axiomatisation in mind when he talks about BISH. | |
| Jan 18, 2016 at 11:34 | comment | added | Carl Mummert | @Noah Schweber: in a professional context of logic, I would read "constructive" to mean something like "in intuitionistic logic", rather than the weaker informal meaning that some mathematicians use for it (e.g. "provable in ZF"). | |
| Jan 18, 2016 at 11:33 | comment | added | Carl Mummert | The compactness theorem is a classical theorem about classical models. It would be very unusual for someone in constructive mathematics to worry about such a result. On one hand, constructivists such as Bishop avoid formalization entirely, and thus also avoid model theory. Bishop's interest, essentially, is core math only. On the other hand, constructive metamathematics is done with alternative kinds of models that are relevant to constructive logic. The concept of a model (in the sense of classical model theory) has classical logic through and through (e.g. in the T-schema). | |
| Jan 18, 2016 at 10:49 | comment | added | Erfan Khaniki | As much as I know Bishop does not suggest any "model theoretic" framework in his book "Constructive analysis", actually it is like you work in a specific model name "standard model" in analysis like working in analysis in classical logic, without talking about models of real analysis. | |
| Jan 18, 2016 at 10:48 | comment | added | Noah Schweber | I believe both the proof of compactness for countable models from WKL and the reversal are constructive, according to most definitions of the term; so my understanding is that the status of the two are identical. (But I could be wrong.) | |
| Jan 18, 2016 at 10:14 | comment | added | Mikhail Katz | I had in mind mostly Bishop's framework, with a suitable interpretation of "countability" so as hopefully to obtain a positive result for compactness. Is there any chance of that? | |
| Jan 18, 2016 at 10:07 | comment | added | Erfan Khaniki | There are different frames for models of intutionistic logic, like kripke model, beth model and a model theory in real line. So you should specify what do you mean by countable model. | |
| Jan 18, 2016 at 9:58 | history | asked | Mikhail Katz | CC BY-SA 3.0 |