Conversation

Notices

1. Embed this notice
   ?? Humpleupagus ?? (humpleupagus@eveningzoo.club)'s status on Saturday, 28-Jun-2025 05:53:37 JST ?? Humpleupagus ??

   in reply to

   • Jon Sterling
   Actually.
   
   A -> C, A & ~C -> Q
   • Embed this notice
     Jon Sterling (jonmsterling@mathstodon.xyz)'s status on Saturday, 28-Jun-2025 05:53:38 JST Jon Sterling

     in reply to

     • rzeta0

     @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.

   • Embed this notice
     Jon Sterling (jonmsterling@mathstodon.xyz)'s status on Saturday, 28-Jun-2025 05:53:40 JST Jon Sterling

     in reply to

     • rzeta0

     @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 => C

     Here you have another implication, so you might as well apply the intro rule once more. Then you'd have:

     (A => B), (B => C), A |- C

     Now you can start working your way downward with elim rules.

   • Embed this notice
     rzeta0 (rzeta0@mastodon.social)'s status on Saturday, 28-Jun-2025 05:53:41 JST rzeta0

     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