chris martens (they/them) 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.pdf
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