Timeline for Do second-order theories always have irredundant axiomatizations?
Current License: CC BY-SA 4.0
11 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Nov 11, 2022 at 19:07 | comment | added | Noah Schweber | As a very-belated comment, I think that your argument also shows independent axiomatizability for second-order logic in higher-order languages; since interpolation fails in that setting, Reznikoff's original argument doesn't trivially go through. | |
| Mar 16, 2022 at 23:26 | history | bounty ended | Noah Schweber | ||
| Mar 16, 2022 at 14:38 | comment | added | Emil Jeřábek | I see. I didn’t really study the proof in detail. | |
| Mar 16, 2022 at 14:34 | vote | accept | Noah Schweber | ||
| Mar 16, 2022 at 14:34 | history | edited | Emil Jeřábek | CC BY-SA 4.0 |
deleted 95 characters in body
|
| Mar 16, 2022 at 14:34 | comment | added | Noah Schweber | Doesn't Reznikoff use compactness? (Or did I have a fascinating logic hallucination, as one sometimes does?) BTW I can't award the bounty for another 3 hours, but as soon as I can I will. Thanks as always! | |
| Mar 16, 2022 at 14:33 | comment | added | Emil Jeřábek | Ah, ok, you are right. I didn’t really think about it, and assumed there was a problem with it, as this is the only sophisticated property of first-order logic used in Reznikoff’s proof. So why doesn’t Reznikoff’s proof apply to second-order logic? | |
| Mar 16, 2022 at 14:24 | comment | added | Noah Schweber | This is nice, and I think it works! A quick question: you say Craig isn't available in SOL, but isn't it trivialy true in SOL since we can directly quantify over the "extra symbols" in the interpolant? | |
| Mar 16, 2022 at 13:53 | history | edited | Emil Jeřábek | CC BY-SA 4.0 |
added 198 characters in body
|
| Mar 16, 2022 at 13:46 | history | edited | Emil Jeřábek | CC BY-SA 4.0 |
added 198 characters in body
|
| Mar 16, 2022 at 13:33 | history | answered | Emil Jeřábek | CC BY-SA 4.0 |