A prop B prop ( A ∧ B ) prop ∧ F {\frac {A{\hbox{ prop}}\qquad B{\hbox{ prop}}}{(A\wedge B){\hbox{ prop}}}}\ \wedge _{F}
где круглые скобки опущены, чтобы сделать правило вывода более кратким:
A prop B prop A ∧ B prop ∧ F {\frac {A{\hbox{ prop}}\qquad B{\hbox{ prop}}}{A\wedge B{\hbox{ prop}}}}\ \wedge _{F}
Это правило вывода является схематичным: A и B могут быть созданы с помощью любого выражения. Общая форма правила вывода такова:
J 1 J 2 ⋯ J n J name {\frac {J_{1}\qquad J_{2}\qquad \cdots \qquad J_{n}}{J}}\ {\hbox{name}}
где каждое из J i J _{ i } является суждением, а правило вывода называется " name ". Суждения над чертой называются посылками, а те, что ниже черты, являются выводами. Другими распространенными логическими утверждениями являются дизъюнкция ( A ∨ B A \ vee B ), отрицание ( A \ neg A ), импликация ( A ⊃ B A \ supset B ) и логические константы истинности ( ⊤ \ top ) и ложности ( ⊥ \ bot ). Правила их формирования приведены ниже.
A prop B prop A ∨ B prop ∨ F A prop B prop A ⊃ B prop ⊃ F {\displaystyle {\frac {A{\hbox{ prop}}\qquad B{\hbox{ prop}}}{A\vee B{\hbox{ prop}}}}\ \vee _{F}\qquad {\frac {A{\hbox{ prop}}\qquad B{\hbox{ prop}}}{A\supset B{\hbox{ prop}}}}\ \supset _{F}}
⊤ prop ⊤ F ⊥ prop ⊥ F A prop A prop F {\displaystyle {\frac {\hbox{ }}{\top {\hbox{ prop}}}}\ \top _{F}\qquad {\frac {\hbox{ }}{\bot {\hbox{ prop}}}}\ \bot _{F}\qquad {\frac {A{\hbox{ prop}}}{\neg A{\hbox{ prop}}}}\ \neg _{F}}
Введение и устранение
Теперь мы обсудим " истинное" суждение. Правила вывода, которые вводят логическую связку в заключение, известны как правила введения. Для введения союзов, т.е. для вывода " A и B истинны" для предложений A и B , требуется доказательство " A истинно" и " B истинно". Как правило вывода:
A true B true ( A ∧ B ) true ∧ I {\frac {A{\hbox{ true}}\qquad B{\hbox{ true}}}{(A\wedge B){\hbox{ true}}}}\ \wedge _{I}
Следует понимать, что в таких правилах объектами являются предложения. То есть приведенное выше правило на самом деле является сокращением для: