You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
29 lines
899 B
29 lines
899 B
This sequent is provable.
|
|
|
|
\begin{logicproof}{2}
|
|
(s \lor \lnot u) \imp t & \prem \\
|
|
s \lor \lnot s & $\LEM$ \\
|
|
\begin{subproof}
|
|
s & \assum \\
|
|
s\lor \lnot u & $\ori{1} 3$ \\
|
|
t & $\impe 4, 1$ \\
|
|
(\lnot s \land u) \lor t & $\ori{2} 5$
|
|
\end{subproof}
|
|
\begin{subproof}
|
|
\lnot s & \assum \\
|
|
u \lor \lnot u & $\LEM$ \\
|
|
\begin{subproof}
|
|
u & \assum \\
|
|
\lnot s \land u & $\andi 7,9$ \\
|
|
(\lnot s\land u) \lor t & $\ori{1} 10$
|
|
\end{subproof}
|
|
\begin{subproof}
|
|
\lnot u & \assum \\
|
|
s \lor \lnot u & $\ori{2} 12$ \\
|
|
t & $\impe 13 1$ \\
|
|
(\lnot s\land u) \lor t & $\ori{2} 14$
|
|
\end{subproof}
|
|
(\lnot s\land u) \lor t & $\ore 8, 9-11, 12-15$
|
|
\end{subproof}
|
|
(\lnot s\land u) \lor t & $\ore 2, 3-6, 7-16$
|
|
\end{logicproof}
|