Post AvZEPy50qqroifCSrA by jonmsterling@mathstodon.xyz
 (DIR) More posts by jonmsterling@mathstodon.xyz
 (DIR) Post #AvZENJnzcVo5ENyYYi by rzeta0@mastodon.social
       2025-06-07T19:15:23Z
       
       0 likes, 0 repeats
       
       Need some help.-----I know that to prove P ⇒ Q, I assume P and derive Q.----Now to prove(A⇒B) ⇒ ((B⇒C) ⇒ (A⇒C))I need to assume (A⇒B) and derive ((B⇒C) ⇒ (A⇒C)).But I can't seem to make progress from (A⇒B)  alone, I think I need to assume A is true as well.----Intuitively the statement makes total sense. But drawing the derivation as per image attached using elim and intro rules, I get stuck unless I assume A too.Can anyone help clarify my thinking?#maths #cs #logic
       
 (DIR) Post #AvZENLA0a90lQxHeVs by jeffcliff@shitposter.world
       2025-06-27T20:48:30.060353Z
       
       1 likes, 1 repeats
       
       @rzeta0 >But I can't seem to make progress from (A⇒B)  alone, I think I need to assume A is true as well.right: If you assume A you should get C, that's generally what A⇒C means.
       
 (DIR) Post #AvZEPwiduXNYUzj5Lk by jonmsterling@mathstodon.xyz
       2025-06-07T19:19:08Z
       
       1 likes, 0 repeats
       
       @rzeta0 You started off right. Your goal was an implication, so you applied the introduction rule.Then your goal was (A => B) |- ((B => C) => (A => C)).That's another implication, so you might as well apply the introduction rule again.Now you would have:(A => B), (B => C) |- A => CHere you have another implication, so you might as well apply the intro rule once more. Then you'd have:(A => B), (B => C), A |- CNow you can start working your way downward with elim rules.
       
 (DIR) Post #AvZEPy50qqroifCSrA by jonmsterling@mathstodon.xyz
       2025-06-07T19:21:39Z
       
       1 likes, 0 repeats
       
       @rzeta0 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); it doesn't matter in what order you apply the invertible rules. The only thing you have to use your brain for is to decide when to apply *non-invertible* rules.
       
 (DIR) Post #AvZEpPJ2lI7GOqtRAW by Humpleupagus@eveningzoo.club
       2025-06-27T20:53:34.822738Z
       
       0 likes, 1 repeats
       
       Actually. A -> C, A & ~C -> Q