Timeline for Does quantification over functions (STLC) increase strength beyond first order logic?
Current License: CC BY-SA 4.0
12 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Sep 18, 2022 at 1:42 | comment | added | Ms. Molly Stewart-Gallus | @DanielMGessel I found about 3 major blockers for traditional first order logic. 1. Handling definitions is fiddly 2. Handling binders in expressions (this question) is even more fiddly. 3. Handling predicates in expressions is even more fiddly (like subset notation.) Some form of universes seems convenient to help with these sort of issues. Also FOL doesn't compute. It's not as convenient as dependent type theory for some uses. | |
| Sep 16, 2022 at 9:47 | comment | added | user1168 | Naive, possibly massively open-ended question: Why is first order logic impractical? | |
| Sep 14, 2022 at 18:36 | vote | accept | Ms. Molly Stewart-Gallus | ||
| Sep 14, 2022 at 8:44 | answer | added | Pierre-Marie Pédrot | timeline score: 4 | |
| Sep 13, 2022 at 18:20 | comment | added | Andrej Bauer | If you want a system that is usable in practice you should reconsider using first-order logic. | |
| Sep 13, 2022 at 16:16 | comment | added | Ms. Molly Stewart-Gallus | @AndrejBauer yeah there's no sort of truth values. So I think I want "many sorted logic?" I guess part of the question is figuring out the best way to make this precise to avoid impredicativity. To be precise the current in progress code is here gist.github.com/mstewartgallus/f98bd774c22ba06e7b4620377a597f9d . Set theory is just one example of a system that is nicer with binders. I want a framework with binders to be useable in practice and not just for metatheory. And I haven't even got into alternative possibilities like nominal sets. | |
| Sep 13, 2022 at 14:04 | comment | added | Andrej Bauer | It is not clear what your formalism is, and the answer depends on that. You say it is first-order logic. Is it multi-sorted? What are the sorts, does "STLC" indicate you're implementing STLC with first-order logic on top? Is there a sort of truth values? Your examples indicate that you can define $\{f(z) \mid z \in x\}$, so perhaps you're in set theory (in which case the question is moot anyhow). | |
| Sep 12, 2022 at 18:58 | comment | added | Ms. Molly Stewart-Gallus | @Trebor so STLC plus booleans and primitive recursive arithmetic right? I know there has to be stuff investigating its strength but I'm not familiar with the details | |
| Sep 12, 2022 at 15:42 | answer | added | Couchy | timeline score: 1 | |
| Sep 12, 2022 at 4:21 | comment | added | Couchy | I believe things become problematic when you start quantifying over propositions | |
| Sep 12, 2022 at 3:11 | comment | added | Trebor♦ | Have you heard of system T? | |
| Sep 11, 2022 at 18:22 | history | asked | Ms. Molly Stewart-Gallus | CC BY-SA 4.0 |