10 ms·

While naming the different derivation rules can be useful for guiding readers the names are not formally necessary. The rules A B ----- C and A

While naming the different derivation rules can be useful for guiding readers the names are not formally necessary. The rules A B ----- C and A B ----- (→c) C are logically equivalent, the latter just gives you a name to refer to the rule by. Additionally, I would be careful about correcting others that something is "technically" called something else as programming language researchers often use many names for the same concept.

dvt 7y ago
> Additionally, I would be careful about correcting others that something is "technically" called something else as programming language researchers often use many names for the same concept. My point had nothing to do with programming language research (in fact, my academic background is logic/metalogic). And by the way, this is not a rule: A B ----- (→c) C It's a derivation (also known as a proof) -- technical terms are important when doing logic. The rule is →c -- so I know what you're doing by including the →c there. Why the →c is necessary (and, again, I've seen it in every lambda calculus/type theory book I've taken a gander at) is because there are many rules[1] (including several kinds of elimination, so things can get complicated and it's important to keep our ducks in a row). [1] https://www.irif.fr/~mellies/mpri/mpri-ens/biblio/Selinger-Lambda-Calculus-Notes.pdf https://www.irif.fr/~mellies/mpri/mpri-ens/biblio/Selinger-L...
- mkolosick 7y ago
  Perhaps using abstract names A, B, and C was unclear. The following is the rule that is commonly referred to as modus ponens: A → B A ----------- B However, modus ponens is just one of the names for this. I could also call it function elimination. I could call it →e. Or I could not bother giving it a name and just say that this is a rule in my logic call it whatever you want in your head if you so desire. Things can get complicated, but they aren't always complicated so naming rules isn't strictly necessary.

dvt 7y ago

> Additionally, I would be careful about correcting others that something is "technically" called something else as programming language researchers often use many names for the same concept. My point had nothing to do with programming language research (in fact, my academic background is logic/metalogic). And by the way, this is not a rule: A B ----- (→c) C It's a derivation (also known as a proof) -- technical terms are important when doing logic. The rule is →c -- so I know what you're doing by including the →c there. Why the →c is necessary (and, again, I've seen it in every lambda calculus/type theory book I've taken a gander at) is because there are many rules[1] (including several kinds of elimination, so things can get complicated and it's important to keep our ducks in a row). [1] https://www.irif.fr/~mellies/mpri/mpri-ens/biblio/Selinger-Lambda-Calculus-Notes.pdf https://www.irif.fr/~mellies/mpri/mpri-ens/biblio/Selinger-L...

mkolosick 7y ago
Perhaps using abstract names A, B, and C was unclear. The following is the rule that is commonly referred to as modus ponens: A → B A ----------- B However, modus ponens is just one of the names for this. I could also call it function elimination. I could call it →e. Or I could not bother giving it a name and just say that this is a rule in my logic call it whatever you want in your head if you so desire. Things can get complicated, but they aren't always complicated so naming rules isn't strictly necessary.