МАТ_ ЛОГИКА / TAB_Сод вывод

Исчисление высказываний

Г a В - секвенция (из множества формул Г={A1, A2,…, An} следует В, возможно Г= )

aВ - формула В доказуема

Гa - множество формул Г противоречиво

Содержательные правила вывода

Логическая	Введение	Удаление
операция

Ù

Г a А, Г a В

Г a (А Ù В)

Г a (А Ù В)

Г a В

Г a (А Ù В)

Г a А

→ Ù

Ù →

Ú

Г a А

Г a (А Ú В); Г, A a C; Г, B a C

Г a (А Ú В)

Г a C

Г a В

Г, А a C; Г, B a C

Г,(А Ú В) a C

Г a (А Ú В)

→ Ú

Ú →

Þ

Г, А, a В

Г a А, Г a (А Þ В)

Г a (А Þ В)

Г a В

→ Þ

→ Þ

Û

Г a (А Þ В); Г a (В Þ А)

Г a (А Û В)

Г a (А Û В)

Г a (А Þ В)

Г a (А Û В)

Г a (В Þ А)

→ Û

Û →

Ø

Г, А a

Г, ØА a

Г a (ØА)

Г a А

Г, А a В; Г, А a (ØВ)

Г a (ØА)

→ Ø

Ø →