Математическая логика и теория алгоритмов. Стенюшкина В.А. - 20 стр.

      1) переменные есть (пропозициональные) формулы;
      2) если А,В - формулы, то ( А), (А →В) - формулы;
      - множество аксиом задается схемами (один из вариантов):
      А1: = (А→ (В → А);
      А2: = ((А → (В →С )) → ((А →В) → (А→С)):
      А3: = (( В→ А) → ((В →А→ В));
                                           A, A → B
      -множество правил задается схемой:            MP (Modus Ponens),
                                               B
      где А, В, … - любые формулы. Для получения конкретных правил и ак-
сиом используются подстановки формул вместо метасимволов А, В, .... Знак
подстановки: «/».
      В дальнейшем используются синтаксические сокращения:
      А∧В: =  (А→  В); А, ∨, В:=  А → В.

       5.2 Выводимость. Производные правила вывода

       Выводимость формул в L, как в ФT, доказывается путем построения со-
ответствующего вывода. Формулы вывода будем записывать в столбец, а спра-
ва - указывать основание для включения этих формул в вывод. В качестве при-
мера рассмотрим вывод из аксиом.
       Теорема 5.1 |−LА→ А.
       Доказательствo
       1) (А → ((А →А) → А)); А1: {А → А/В};
       2) ((А → ((А→ А) →А)) → ((А → (АА))(A→A)); А2: {А → АВ, А/С};
       3) ((А → (А → А )) → (А → А)); МР: 1,2;
       4) А → (А → А); А1: {A /В};
       5) А → А; МР: 4,3
       Всякую доказанную выводимость можно использовать как новое, произ-
водное правило вывода.
       Теорема 5.2 A|−LB→ А.
       Доказательство:
       1) А; гипотеза;
       2) А → (В →В); A1;
       3) В → А; МР: 1,2.
                                A
       Доказана выводимость        I mp ─ правило введения импликации.
                              B→A

       5.3 Теорема дедукции

      Теорема Если Г, А |−L ...В1, то Г |−L... А → В и обратно. Здесь Г - некото-
рое множество формул.
      Доказательство прямой теоремы. Пусть Е1 ..., Еn – вывод - В из Г, А. При
этом Еn =В. Применяя метод математической индукции по i (1 ≤ i ≤ n), то есть