Timeline for Sharp Craig interpolation theorem for $L_{\omega_1 \omega}$
Current License: CC BY-SA 4.0
10 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Nov 30, 2021 at 3:17 | vote | accept | Rachael Alvir | ||
| Nov 23, 2021 at 5:14 | history | bounty ended | Noah Schweber | ||
| Nov 22, 2021 at 17:31 | comment | added | Fedor Pakhomov | @AndreasBlass Interesting, didn't knew about that fact. Actually I think that a slight alteration of your proof gives the following. Suppose $\theta$ is a property of models that is $\Delta^1_1$ over $\mathcal{L}_{\omega_1\omega}$ matrices. Then there are infinitary $\Pi_2$ formulas $\varphi,\psi$ such that the implication $\varphi\to\lnot \psi$ is provable and any interpolant $\theta'$ for the implication is semantically equivalent to $\theta$. The point is that any $\Sigma^1_1$ over $\mathcal{L}_{\omega_1\omega}$-matrix could be Skolemized to a $\Sigma^1_1$ over an infinitary $\Pi_2$-matrix. | |
| Nov 22, 2021 at 16:30 | comment | added | Andreas Blass | I should have said to use different new function symbols in $\phi$ and $\psi$, so they won't appear in an interpolant. | |
| Nov 22, 2021 at 16:29 | comment | added | Alex Kruckman | @AndreasBlass Excellent, thanks! | |
| Nov 22, 2021 at 16:28 | comment | added | Andreas Blass | @AlexKruckman Start by Skolemizing $\theta$ to look like a block of existential second-order (function) quantifiers followed by a universal first-order formula. Delete the function quantifiers (so the function variables become new 1st-order function symbols); what's left is $\phi$. Dually, Herbrandize $\theta$ to universal 2nd-order plus 1st-order existential formula; the existential 1st-order part is $\psi$. The main point is that, before you deleted the 2nd-order quantifiers, both versions were equivalent to $\theta$, and that implies $\theta$ is the only interpolant. | |
| Nov 22, 2021 at 16:20 | comment | added | Alex Kruckman | @AndreasBlass Oh, what a nice fact. What's the proof, or where can I find a proof? | |
| Nov 22, 2021 at 15:41 | comment | added | Andreas Blass | This looks like a higher-order analog of the (known but not sufficiently well-known) fact in finitary first-order logic that, for any sentence $\theta$, there is a valid implication $\phi\to\psi$ with $\phi$ universal, $\psi$ existential, and all interpolants logically equivalent to $\theta$. | |
| Nov 22, 2021 at 12:04 | history | edited | Fedor Pakhomov | CC BY-SA 4.0 |
added 7 characters in body
|
| Nov 22, 2021 at 11:52 | history | answered | Fedor Pakhomov | CC BY-SA 4.0 |