|
|
$$\begin{array}{rlrl}
1&{_{\:\!\mathbf|}}\!\underline{\,~\neg A\lor B~}\\[-5pt]
2&\big|~{_{\:\!\mathbf|}}\!\underline{\,~A~}\\[-5pt]
3&\big|~\big|~{_{\:\!\mathbf|}}\!\underline{\,~\neg A~}\\[-5pt]
4&\big|~\big|~\big|~\bot&\rm{{\neg}E}&\rm{3,2}\\[-5pt]
5&\big|~\big|~\big|~B&\rm{X}&\rm{4}\\[-5pt]
6&\big|~\big|~{_{\:\!\mathbf|}}\!\underline{\,~B~}\\[-5pt]
7&\big|~\big|~B&\rm{{\lor}E}&\rm{1,3{-}5,6{-}6}\\[-5pt]
8&\big|~A\to B&\rm{{\to}I}&\rm{2{-}7}\\[-5pt]
9&{_{\:\!\mathbf|}}\!\underline{\,~A\to B~}\\[-5pt]
10&\big|~{_{\:\!\mathbf|}}\!\underline{\,~A~}\\[-5pt]
11&\big|~\big|~B&\rm{{\to}E}&\rm{9,10}\\[-5pt]
12&\big|~\big|~\neg A\lor B&\rm{{\lor}I}&\rm{11}\\[-5pt]
13&\big|~{_{\:\!\mathbf|}}\!\underline{\,~\neg A~}\\[-5pt]
14&\big|~\big|~\neg A\lor B&\rm{{\lor}I}&\rm{13}\\[-5pt]
15&\big|~\neg A\lor B&\rm{LEM}&\rm{10{-}12,13{-}14}\\[-5pt]
16&(A\to B)\leftrightarrow (\neg A\lor B)&\rm{{\leftrightarrow}I}&\rm{1{-}8,9{-}15}\\[-5pt]
\end{array}$$
|
|
|