Mathematical Logic 책을 보고 있는데 Theorem schemas of P 라는 챕터에서 P의 arbitrary한 wff인 A와 B를 주고 proof를 쓰라고 하네요.
ㅏA⊃[B⊃[A⊃B]] 를 증명하라고 하는데, 해답의 과정은

A, B, AㅏB                        (1)
A, BㅏA⊃B                (2) deduction theorem
AㅏB⊃[A⊃B]                (3) deduction theorem
ㅏA⊃[B⊃[A⊃B]]        (4) deduction theorem

이렇게 나와 있습니다. 각 과정에서 deduction theorem을 사용하는 건 알겠는데 제일 처음의 식이 어떻게 나온 건지 궁금합니다. 물론 ㅏ앞에 A,B,A가 있으니까 ㅏ뒤에는 B가 나와도 정당하다는 건 압니다. 하지만 ㅏ앞에 저렇게 마음대로 써도 되는 건가요? A, B가 arbitrary하니까 그냥 임의로 마음대로 hypothesis라고 정한건지... ㅏ앞에는 hypothesis가 나오는 건 알겠는데 A, B, AㅏB를 그냥 아무렇게나 잡아두고 증명의 과정을 전개시켰다고 이해하면 되나요? 

사실 이 문제만이 아니라 다른 증명에서도 첫번째 식이 어떻게 나왔는지 헷갈리는 경우가 많네요. 임의로 정했다면 위의 수식은 차라리 이해라도 되는데ㅏA⊃[~B⊃~[A⊃B]] 의 증명과정에서 첫번째 식은 A,~B,A⊃BㅏA가 나오더군요. 그냥 계산의 편의상 괜찮은 걸 앞에다가 잡는 것 같아 보이기도 하구요... 

hypothesis는 wff만 만족하면 그냥 자기 마음대로 잡고 식을 전개시켜나가도 되는 건가요? 그렇다면 예를 들어 ㅏ[A⊃B]⊃[~B⊃~A]를 증명할 때, A⊃Bㅏ~B⊃~A 라고 놓고 deduction theorem을 적용시켜 바로 ㅏ[A⊃B]⊃[~B⊃~A]를 이끌어내도 되는 건지요...