Фигуры вывода, которые мы видели до сих пор, недостаточны для изложения правил введения импликации или устранения дизъюнкции ; для этого нам нужно более общее понятие гипотетического вывода.
Гипотетические выводы
Широко распространенной операцией в математической логике является рассуждение на основе предположений. Например, рассмотрим следующий вывод:
A ∧ ( B ∧ C ) true B ∧ C true B true ∧ E 1 ∧ E 2 {\displaystyle {\cfrac {A\wedge \left(B\wedge C\right){\hbox{ true}}}{{\cfrac {B\wedge C{\hbox{ true}}}{B{\hbox{ true}}}}\ \wedge _{E1}}}\ \wedge _{E2}}
Этот вывод не устанавливает истинность B как таковой; скорее, он устанавливает следующий факт:
Если A ∧ ( B ∧ C ) истинно , то B истинно .
В логике говорят: "предполагая, что A ∧ ( B ∧ C ) истинно , мы показываем , что B истинно "; другими словами, суждение " B истинно" зависит от предполагаемого суждения " A ∧ ( B ∧ C ) истинно". Это гипотетический вывод, который мы записываем следующим образом:
A ∧ ( B ∧ C ) true ⋮ B true {\displaystyle {\begin{matrix}A\wedge \left(B\wedge C\right){\hbox{ true}}\\\vdots \\B{\hbox{ true}}\end{matrix}}}
Интерпретация такова: " B true выводится из A ∧ ( B ∧ C ) true ". Конечно, в этом конкретном примере мы действительно знаем, как происходит " B true " от " A ∧ ( B ∧ C ) true ", но в общем случае мы можем априори не знать этого вывода. Общая форма гипотетического вывода такова:
D 1 D 2 ⋯ D n ⋮ J {\displaystyle {\begin{matrix}D_{1}\quad D_{2}\ \cdots \ D_{n}\\\vdots \\J\end{matrix}}}
У каждого гипотетического вывода есть набор предшествующих выводов ( Di ), написанных в верхней строке, и последующее суждение ( J ), написанное в нижней строке. Каждая из посылок сама по себе может быть гипотетическим выводом. (Для простоты мы рассматриваем суждение как вывод без посылок.)
Понятие гипотетического суждения усвоено как связующее звено импликации. Правила введения и исключения следующие.
A true u ⋮ B true A ⊃ B true ⊃ I u A ⊃ B true A true B true ⊃ E {\displaystyle {\cfrac {\begin{matrix}{\cfrac {}{A{\hbox{ true}}}}\ u\\\vdots \\B{\hbox{ true}}\end{matrix}}{A\supset B{\hbox{ true}}}}\ \supset _{I^{u}}\qquad {\cfrac {A\supset B{\hbox{ true}}\quad A{\hbox{ true}}}{B{\hbox{ true}}}}\ \supset _{E}}
В правиле введения предшествующее, названное u , разряжается в заключении. Это механизм для разграничения объема гипотезы: его единственная причина существования - установить " B истинно"; он не может быть использован ни для каких других целей, и, в частности, он не может быть использован ниже введения. В качестве примера рассмотрим вывод " A ⊃ ( B ⊃ ( A ∧ B )) истинно".:
A true u B true w A ∧ B true ∧ I B ⊃ ( A ∧ B ) true A ⊃ ( B ⊃ ( A ∧ B ) ) true ⊃ I u ⊃ I w {\displaystyle {\cfrac {{\cfrac {{\cfrac {}{A{\hbox{ true}}}}\ u\quad {\cfrac {}{B{\hbox{ true}}}}\ w}{A\wedge B{\hbox{ true}}}}\ \wedge _{I}}{{\cfrac {B\supset \left(A\wedge B\right){\hbox{ true}}}{A\supset \left(B\supset \left(A\wedge B\right)\right){\hbox{ true}}}}\ \supset _{I^{u}}}}\ \supset _{I^{w}}}
У этого полного вывода нет неудовлетворительных предпосылок; однако дополнительные выводы являются гипотетическими. Например, вывод " B ⊃ ( A ∧ B ) true " является гипотетическим с предшествующим " A true " (с именем u ).
Используя гипотетические выводы, мы теперь можем написать правило исключения для дизъюнкции:
A ∨ B true A true u ⋮ C true B true w ⋮ C true C true ∨ E u , w {\displaystyle {\cfrac {A\vee B{\hbox{ true}}\quad {\begin{matrix}{\cfrac {}{A{\hbox{ true}}}}\ u\\\vdots \\C{\hbox{ true}}\end{matrix}}\quad {\begin{matrix}{\cfrac {}{B{\hbox{ true}}}}\ w\\\vdots \\C{\hbox{ true}}\end{matrix}}}{C{\hbox{ true}}}}\ \vee _{E^{u,w}}}
Другими словами, если A ∨ B истинно, и мы можем вывести " C истинно" как из " A истинно", так и из " B истинно", то C действительно истинно. Обратите внимание, что это правило не устанавливает ни " A true ", ни " B true ". В нулевом случае, то есть для ложности, мы получаем следующее правило исключения:
⊥ true C true ⊥ E {\displaystyle {\frac {\perp {\hbox{ true}}}{C{\hbox{ true}}}}\ \perp _{E}}