Greg Restall on Nostr: This morning, one of my hardworking intermediate logic students (prepping for her ...
This morning, one of my hardworking intermediate logic students (prepping for her exam next week), came to me with a query about how to prove the constructively invalid quantifier negation inference (from ∀x(A(x)∨B(x)) to ∀xA(x)∨∃xB(x)) in natural deduction with Double Negation Elimination.
It was natural that she would struggle with this exercise, since any proof of this (in that natural deduction framework at least), requires a quite bit of fancy footwork.
After we worked through that, I wondered whether the proof is much simpler in classical natural deduction with alternatives (basically the λμ calculus). If you help yourself to the derivable (and simpler to work with) ∨E* variant rule, it turns out that the proof shrinks from 14 steps to 10, and it seems much more direct.
Published at
2024-12-11 09:48:33Event JSON
{
"id": "f39a0c624a0985cfeca4aad73291800d4472dfa1569c881ec10977953e9c67e8",
"pubkey": "43968fa6d05208dd17eff0d9bf3fa311f7009fbba42f73f158327923b91a1637",
"created_at": 1733910513,
"kind": 1,
"tags": [
[
"imeta",
"url https://spaces.hcommons.social/media_attachments/files/113/633/559/297/323/896/original/bd9b9dd888275afe.jpg",
"m image/jpeg",
"dim 3233x2565",
"blurhash U3Ss89~p~p4:9Z9F%M-pWCM{Rjay?HxaofIo"
],
[
"imeta",
"url https://spaces.hcommons.social/media_attachments/files/113/633/559/293/971/910/original/de1889608b91fa83.jpg",
"m image/jpeg",
"dim 3104x2672",
"blurhash U4S$owxu~pRkR*4oRj?Ht6IVD*WBt7WBIoNG"
],
[
"proxy",
"https://hcommons.social/users/consequently/statuses/113633559388679275",
"activitypub"
]
],
"content": "This morning, one of my hardworking intermediate logic students (prepping for her exam next week), came to me with a query about how to prove the constructively invalid quantifier negation inference (from ∀x(A(x)∨B(x)) to ∀xA(x)∨∃xB(x)) in natural deduction with Double Negation Elimination.\n\nIt was natural that she would struggle with this exercise, since any proof of this (in that natural deduction framework at least), requires a quite bit of fancy footwork. \n\nAfter we worked through that, I wondered whether the proof is much simpler in classical natural deduction with alternatives (basically the λμ calculus). If you help yourself to the derivable (and simpler to work with) ∨E* variant rule, it turns out that the proof shrinks from 14 steps to 10, and it seems much more direct.\n\nhttps://spaces.hcommons.social/media_attachments/files/113/633/559/297/323/896/original/bd9b9dd888275afe.jpg\nhttps://spaces.hcommons.social/media_attachments/files/113/633/559/293/971/910/original/de1889608b91fa83.jpg",
"sig": "ceb3e54239e50c72c7164e42ee83564059042db3263b2881f3049268e84fdee6d3272c96abde654ae180cdcde49bb22b4c5692e185a749ecca8256982266d467"
}
