При выводе формулы из множества аксиом и посылок используют два основных правила:
а) если Fi и ( Fi ® Fj ) есть выводимые формулы, то Fj также выводимая формула, т.е.
Fi; (Fi®Fj)
Fj.
это правило называют modus ponens (m.p.).
b) если формулы ùFj и (Fi®Fj) есть выводимые формулы, то ùFi также выводимая формула, т.е
ùFj; (Fi®Fj)
ùFi.
это правило называют modus tollens (m.t.).
Пример: Суждение: “Сумма внутренних углов многоугольника равна 180о (А). Если сумма внутренних углов многоугольника равна 180о (A), то многоугольник есть треугольник (В). Следовательно, дан треугольник”.
А;A®B
B.
Пример: Суждение: ”Дан не треугольник (ùB); если сумма внутренних углов многоугольника равна 180о(А), то многоугольник есть треугольник (В). Следовательно, сумма внутренних углов многоугольника не равна 180о(ùA)”.
ùB; A®B
ùA.