5 ms·

The term you want to search for is "Natural Deduction". It's what you use if you study type theory. I don't know any lightweight introductions off the top of my

The term you want to search for is "Natural Deduction". It's what you use if you study type theory. I don't know any lightweight introductions off the top of my head. https://en.wikipedia.org/wiki/Natural_deduction https://en.wikipedia.org/wiki/Natural_deduction The short version is that A B ------- C means "If A and B, then C". Any free variables in A, B, C are universally quantified outside the "if". The reason for writing the rules in this weird format is that you can combine them in a tree: A B ------- C D --------- E This proves E, given A, B, and D, via the application of two rules.

asplake 7y ago
Thanks, should suffice!
dvt 7y ago
The blog post (and your response) is actually a bit confusing, as we should be seeing inline rules -- at least that's how I've seen it in just about every textbook. The "implication" rule you suggest is actually (technically) called "elimination" (in λ-calculus, we say you eliminate a variable) and should be denoted via →e (sometimes the arrow is omitted). As a more practical example, see proposition (11) in this paper I wrote back in college[1]. There are two elimination rules, both denoted by an inline →e. [1] https://dvt.name/logic/horse2.pdf https://dvt.name/logic/horse2.pdf
- mkolosick 7y ago
  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.

asplake 7y ago

Thanks, should suffice!

dvt 7y ago

The blog post (and your response) is actually a bit confusing, as we should be seeing inline rules -- at least that's how I've seen it in just about every textbook. The "implication" rule you suggest is actually (technically) called "elimination" (in λ-calculus, we say you eliminate a variable) and should be denoted via →e (sometimes the arrow is omitted). As a more practical example, see proposition (11) in this paper I wrote back in college[1]. There are two elimination rules, both denoted by an inline →e. [1] https://dvt.name/logic/horse2.pdf https://dvt.name/logic/horse2.pdf

mkolosick 7y ago
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.