chris martens on Nostr: as poetic as i find frank's use of the term "harmony" to describe local soundness and ...
as poetic as i find frank's use of the term "harmony" to describe local soundness and completeness (cf. local reduction and expansion of proofs) in natural deduction*, i am not sure that it really works as a music metaphor.
maybe i'm missing something? but musical harmony is about deriving "new" sounds from individual sounds, whereas logical harmony is about checking you *can't* do (something like) that with your inference rules.
*see, e.g., part 11 here
https://www.cs.cmu.edu/~fp/courses/15814-f21/lectures/17-natded.pdfPublished at
2024-10-03 15:03:26 UTCEvent JSON
{
"id": "4cb7f39c81ec254f1fad73618c4c5e0e2d949e85d4fb343118a653d1e6726b63",
"pubkey": "20620c8fffc921adb198ad4e702673713d1543b1c59fbc83c4e652226a62dfa4",
"created_at": 1727967806,
"kind": 1,
"tags": [
[
"proxy",
"https://hci.social/@chrisamaphone/113244098161425852",
"web"
],
[
"proxy",
"https://hci.social/users/chrisamaphone/statuses/113244098161425852",
"activitypub"
],
[
"L",
"pink.momostr"
],
[
"l",
"pink.momostr.activitypub:https://hci.social/users/chrisamaphone/statuses/113244098161425852",
"pink.momostr"
],
[
"-"
]
],
"content": "as poetic as i find frank's use of the term \"harmony\" to describe local soundness and completeness (cf. local reduction and expansion of proofs) in natural deduction*, i am not sure that it really works as a music metaphor. \n\nmaybe i'm missing something? but musical harmony is about deriving \"new\" sounds from individual sounds, whereas logical harmony is about checking you *can't* do (something like) that with your inference rules.\n\n*see, e.g., part 11 here https://www.cs.cmu.edu/~fp/courses/15814-f21/lectures/17-natded.pdf",
"sig": "dce0beefadbae882c28ccfa98afaae5045a1081c9cc41e0d00a28992fafbf12dfbd17f31edc264d5c41afcb72c10b837c2aecc3a27e95d58a870447549aaa580"
}
