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.pdf
chris martens /
npub15p…mwhd2
2024-10-03 15:03:26
Author Public Key
npub15pejcagya70mssj8a5dp6htdkdw93h4wzk952favkktwh40sqs3scmwhd2Seen on
wss://relay.mostr.pubPublished at
2024-10-03 15:03:26Event JSON
{
"id": "e96346ff9d396639398a13c6a2ec1c8c137f11b90850a944e04a6b6011f0c7f1",
"pubkey": "a0732c7504ef9fb84247ed1a1d5d6db35c58deae158b4527acb596ebd5f00423",
"created_at": 1727967806,
"kind": 1,
"tags": [
[
"proxy",
"https://hci.social/users/chrisamaphone/statuses/113244098161425852",
"activitypub"
]
],
"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": "ab2a3372a28eb82c634596a829dc4d8e2d733e90c24fdf093ea44bcd09464a89241adac9eb3867cb033e8434abf7846b020b5029d69a6f70da4d39a75ea01241"
}