nprofile1qy2hwumn8ghj7un9d3shjtnddaehgu3wwp6kyqpq0p4hclaqjlup0fwjt5ke3mgxq6rtjth8u62yfv0s62xkxp04wjaqa4rs4v (nprofile…rs4v) I'll let you in on a little secret of structural proof theory that is not taught in enough sources:
Call a rule "invertible" if you can derive the premises from the conclusion. For example, in natural deduction, implication has an invertible intro rule but the elim rule is not invertible. On the other hand, disjunction has an invertible elimination rule but its introduction rules are not invertible.
Anyway, if you are faced with a goal to which any invertible rule applies, you might as well apply it right away as you'll never go wrong by doing so (where "going wrong" means ending up at a dead-end). The only thing you have to use your brain for is to decide when to apply *non-invertible* rules.
Jon Sterling /
npub1hf…9ls8k
2025-06-07 19:21:39
in reply to nevent1q…eqep
Author Public Key
npub1hfga8wmley5fzqtttpeupd8hc6s92rykfmzktm8zfdhu9h8exvqsj9ls8kSeen on
wss://relay.mostr.pubPublished at
2025-06-07 19:21:39Event JSON
{
"id": "b67968c99d73a9b3aedef6f04bf4e2f5af7ed495d8cda616daad9f68b89d2d05",
"pubkey": "ba51d3bb7fc92891016b5873c0b4f7c6a0550c964ec565ece24b6fc2dcf93301",
"created_at": 1749324099,
"kind": 1,
"tags": [
[
"p",
"786b7c7fa097f817a5d25d2d98ed060686b92ee7e69444b1f0d28d6305f574ba",
"wss://relay.mostr.pub"
],
[
"p",
"340694a5c7115fe0918fe7ec9038786592e3804f1a0e457e3e09d03ecfdadc6b",
"wss://relay.mostr.pub"
],
[
"e",
"623c14b64b04843d294c5a939130eac0cb10eada629cbe8e8309d2de12c484d2",
"wss://relay.mostr.pub",
"reply"
],
[
"proxy",
"https://mathstodon.xyz/users/jonmsterling/statuses/114643704169377861",
"activitypub"
],
[
"client",
"Mostr",
"31990:6be38f8c63df7dbf84db7ec4a6e6fbbd8d19dca3b980efad18585c46f04b26f9:mostr",
"wss://relay.mostr.pub"
]
],
"content": "nostr:nprofile1qy2hwumn8ghj7un9d3shjtnddaehgu3wwp6kyqpq0p4hclaqjlup0fwjt5ke3mgxq6rtjth8u62yfv0s62xkxp04wjaqa4rs4v I'll let you in on a little secret of structural proof theory that is not taught in enough sources:\n\nCall a rule \"invertible\" if you can derive the premises from the conclusion. For example, in natural deduction, implication has an invertible intro rule but the elim rule is not invertible. On the other hand, disjunction has an invertible elimination rule but its introduction rules are not invertible.\n\nAnyway, if you are faced with a goal to which any invertible rule applies, you might as well apply it right away as you'll never go wrong by doing so (where \"going wrong\" means ending up at a dead-end). The only thing you have to use your brain for is to decide when to apply *non-invertible* rules.",
"sig": "b0d87faaa89b4b99548c92a862f672895a913ee95cc70d5d9b4fe9b259312705a79585874dcde81585ac3e250495bec88cf66f2f2633f5189d022532897125a3"
}