Timeline for Proving things about a formal logical system
Current License: CC BY-SA 4.0
6 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Aug 11, 2022 at 13:14 | comment | added | Peter Gerdes | Also, I should add, that all the big sets and cardinal stuff doesn't really come into play. Since you are interested in results (codeable as) statements about the natural numbers ZFC is just a conveinient way to state a theory that extends PA with some strong (regular) induction...indeed you can probably find a reference somewhere where someone has shown that ZFC is conservative over so and so's arithmetic | |
| Aug 11, 2022 at 13:11 | comment | added | Peter Gerdes | I realized I could have given a better answer. Suppose that you prove some result about an intuitionistic system I in ZFC, e.g.,the double negation of anything provable in classical logic is provable in I. If you later find a finite instance where that claim actually fails you can turn it into a proof of contradiction in ZFC itself (ok, if it's not a pure existential statement you'd show that ZFC has no standard model but still an earthshattering mathematical result) | |
| Jun 1, 2021 at 19:09 | comment | added | Peter Gerdes | Because if you are interested in the applications I'm presuming what you care about is being convinced that it actually works and ZFC appears not to prove false claims about the integers. So if you provide in ZFC that you can decide a question of intuitionistic entailment about such and such length inputs in in k^2 steps you really will be able to. | |
| Jan 20, 2021 at 7:22 | comment | added | Wei | Thanks! It makes sense to explicitly specify the ambient assumptions (e.g. ZFC, etc.) under which we prove things about a formal system. You said that "if your interest is in the practical use of intuitionistic logic in certain CS applications you'll be happy with proofs about it in ZFC." Could you enlighten why this is the case? | |
| Jan 20, 2021 at 7:17 | vote | accept | Wei | ||
| Dec 2, 2020 at 22:04 | history | answered | Peter Gerdes | CC BY-SA 4.0 |