Калижанова, А.У. Системный анализ Учебное пособие

33 (3.4) (3.5) (3.6) (3.7) (3.8) (3.9) (3.10) (3.11) (3.12) (3.13) (3.14) (3.15) (3.16) Каждая из схем (3.2) — (3.14) порождает счетное множество аксиом, если символы A, B, C заменять конкретными формулами. Поэтому записи (1) — (13) будем называть аксиомными схемами (АС). При этом, АС с двумя формулами носят технический характер интерпретации логических операторов и отношений между ними (записи (3.2), (3.4) — (3.8), (3.10) — (3.14)). Определение 6. Правилом вывода теории L называют процедуру перехода от двух формул вида A и к одной формуле вида B для любых A и B. Это правило называют modus ponens, MP. В случае применения правила MP формулы A и называются посылками, а B — заключением этого правила. Определение 7. Формальным выводом (в теории L) формулы B из посылок A 1 , ..., A n называется конечная последовательность формул B 1 , ..., B k , заканчивающаяся формулой B(B k =B), причем каждая формула этой последовательности — или одна из посылок, или аксиома, или формула, полученная из некоторых двух предшествующих формул этой