Wikipedia:Reference desk/Archives/Mathematics/2021 November 12
| Mathematics desk | ||
|---|---|---|
| < November 11 | << Oct | November | Dec >> | Current desk > |
| Welcome to the Wikipedia Mathematics Reference Desk Archives |
|---|
| The page you are currently viewing is a transcluded archive page. While you can leave answers for any questions shown below, please ask new questions on one of the current reference desk pages. |
November 12[edit]
Kripke frame[edit]
I'm interested in finding out what a Kripke frame is, since they are used in model theory for intuitionistic logic. I looked at the article and found it starts out with definitions in terms of modal logic, which I'm only slightly familiar with. So to understand Kripke frames, I either have to 1) bone up on modal logic first, then read the article; or 2) read something else instead. My immediate interest area is more computer-sciency (e.g. type theory) than logic-y per se, but modal logic does seem like an important area and maybe can't be avoided anyway. Got any advice? Is there a good modern textbook that talks about this stuff? The logic class I took in school used Enderton's "Mathematical Introduction to Logic" which was good but I think rather traditional (Hilbert proof systems, companion volume on set theory, etc). Thanks. 2602:24A:DE47:B8E0:1B43:29FD:A863:33CA (talk) 00:44, 12 November 2021 (UTC)
- The definition of a Kripke frame in the section Basic definitions of the article does not assume or require any familarity with modal logic. After familiarizing yourself with it you can jump directly to the section Semantics of intuitionistic logic. --Lambiam 13:00, 12 November 2021 (UTC)
- If it helps, a Kripke frame is "just" a directed graph. Usually the set of nodes will be infinite. --Lambiam 13:11, 12 November 2021 (UTC)
- Thanks, I'll try harder on the article, but I may be better off with an introductory text with exercises. 2602:24A:DE47:B8E0:1B43:29FD:A863:33CA (talk) 18:17, 12 November 2021 (UTC)
- Let us know if you get stuck. Perhaps this may help: A Short Introduction to Intuitionistic Logic by Grigori Mints. It comes with exercises. Chapter 7, which takes up a mere six pages in print, is devoted to Kripke models. Full disclosure: I knew Grigori Mints; we briefly worked together, although not on any deep stuff. --Lambiam 21:57, 12 November 2021 (UTC)
- Thanks, that looks like a good book. I have seen some of the stuff in it but I think it is always good to work through something systematically. Do you know of something with type theory? I looked at Girard's "Proofs and Types" a few years ago and found it baffling, but maybe I'm a little more prepared by now. 2602:24A:DE47:B8E0:1B43:29FD:A863:33CA (talk) 23:57, 12 November 2021 (UTC)
- There is Mitchell and Moggi's "Kripke-style models for typed lambda calculus", available here. It is rather accessible. The paper "Higher-Order Logic Programming Languages with Constraints: A Semantics" in the Proceedings of TLCA 8, available here, discusses Kripke models for intuitionistic type theory, and the Proceedings of TLCA 9 contains a paper "Kripke Semantics for Martin-Löf's Extensional Type Theory", available on arXiv. I have not read either of the latter two, but these are research papers, so perhaps less suitable as introductory material. --Lambiam 01:18, 13 November 2021 (UTC)
- Thanks, I'll look at those. 2602:24A:DE47:B8E0:1B43:29FD:A863:33CA (talk) 09:01, 15 November 2021 (UTC)
- There is Mitchell and Moggi's "Kripke-style models for typed lambda calculus", available here. It is rather accessible. The paper "Higher-Order Logic Programming Languages with Constraints: A Semantics" in the Proceedings of TLCA 8, available here, discusses Kripke models for intuitionistic type theory, and the Proceedings of TLCA 9 contains a paper "Kripke Semantics for Martin-Löf's Extensional Type Theory", available on arXiv. I have not read either of the latter two, but these are research papers, so perhaps less suitable as introductory material. --Lambiam 01:18, 13 November 2021 (UTC)
- Thanks, that looks like a good book. I have seen some of the stuff in it but I think it is always good to work through something systematically. Do you know of something with type theory? I looked at Girard's "Proofs and Types" a few years ago and found it baffling, but maybe I'm a little more prepared by now. 2602:24A:DE47:B8E0:1B43:29FD:A863:33CA (talk) 23:57, 12 November 2021 (UTC)
- Let us know if you get stuck. Perhaps this may help: A Short Introduction to Intuitionistic Logic by Grigori Mints. It comes with exercises. Chapter 7, which takes up a mere six pages in print, is devoted to Kripke models. Full disclosure: I knew Grigori Mints; we briefly worked together, although not on any deep stuff. --Lambiam 21:57, 12 November 2021 (UTC)
- Thanks, I'll try harder on the article, but I may be better off with an introductory text with exercises. 2602:24A:DE47:B8E0:1B43:29FD:A863:33CA (talk) 18:17, 12 November 2021 (UTC)
Mobius strip problem[edit]
Make a Mobius strip and cut it exactly 1/4 of the way of its thickness. What happens?? (For 1/2 you'll get one long strip; for 1/3 you'll get 2 strips, one of which is longer than the other.) Georgia guy (talk) 20:55, 12 November 2021 (UTC)
- Similar to 1/3, except that the middle strip is now twice the width of the outer one. As for 1/3, the middle strip is again a Möbius strip; the longer outer one has two twists, and so has two distinct sides. You get this for any number x between 0 and 1/2: an outer strip of width x, and a middle strip of width 1 − 2x. As boundary cases we have x = 0, which means the outer strip has zero width, and x = 1/2, meaning the middle strip has zero width. Disclaimer: I have not tried this experimentally. --Lambiam 21:40, 12 November 2021 (UTC)