Timeline for Henkin-style completeness proofs for intuitionistic logic
Current License: CC BY-SA 4.0
8 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Sep 30, 2021 at 16:24 | comment | added | godelian | @ToucanIan The point is that in the Heyting algebra semantics the notion of provability is built-in in the Lindembaum-Tarski construction, so the connection to provability can be made constructively. For Tarski/Kripke semantics the connection is more remote and will involve non-constructive principles. | |
| Sep 30, 2021 at 15:56 | comment | added | ToucanIan | Can you give more detail on how the semantics differ? Other than just the definitions, etc. I have asked a question regarding this here: mathoverflow.net/questions/405055/…. It was suggested that maybe Heyting Algebra Semantics have less entailments. | |
| Sep 30, 2021 at 15:45 | comment | added | godelian | @ToucanIan The semantics are different. The results of Gödel and Kreisel apply to Tarski/Kripke semantics, not Heyting algebra semantics. | |
| Sep 30, 2021 at 15:42 | comment | added | ToucanIan | In Constructivism in Mathematics: An Introduction by Troelstra A.S. and Van Dalen (archive.org/details/constructivismin0002troe/page/718/mode/2up) completeness of intuitionistic predicate calculus is proven in an intuitionistic meta-theory using heyting algebra semantics. Can you assist me in reconciling this result in light of arguements by Gödel and Kreisel. Thanks! | |
| Jan 6, 2019 at 21:16 | vote | accept | Bruno Bentzen | ||
| Jan 6, 2019 at 7:51 | history | edited | Andrej Bauer | CC BY-SA 4.0 |
deleted 5 characters in body
|
| Jan 6, 2019 at 1:02 | history | edited | godelian | CC BY-SA 4.0 |
added 272 characters in body
|
| Jan 6, 2019 at 0:20 | history | answered | godelian | CC BY-SA 4.0 |