Аксиоматика логики Тут есть варианты. Существует два подхода к описанию логических вычислителей: гильбертовский вычислитель, генценовский (последовательный) вычислитель. Разница заключается в том, что гильбертовский вычислитель обычно состоит из множества аксиом и одного правила вывода, а последовательный вычислитель состоит из одной аксиомы и множества правил вывода. Приведем примеры эквивалентных логик, которыми мы пользуемся ежедневно: Классическая логика (гильбертовский вычислитель) Символы: →, ¬, ∧, ∨ Аксиомы: 1. A → ( B → A) 2. (A → (B → C)) → (A → B) → (A → C)) 3. A ∧ B → A 4. A ∧ B → B 5. A → (B → (A ∧ B)) 6. A → (A ∨ B) 7. B → (A ∨ B) 8. (A → C) → ((B → C) →((A ∨ B) → C)) 9. ¬ A → (A → B) 10. (A → B) → ((A → ¬ B) → ¬ A) 11. A ∨ ¬ A Правило вывода: Modus Ponens (MP) Замечание: 1. Теория исчисления предикатов первого порядка включает в себя также правило Generalization (GEN) 2. Если не вкючать последняя 11-ю аксиому исключающего третьего, то логика превратится в конструктивную. Компактная теория К (гильбертовский вычислитель) Символы: →, ¬ Аксиомы: 1. A → ( B → A) 2. (A → (B → C)) → (A → B) → (A → C)) 3. (¬ B → ¬ A) → ((¬ B → A) → B) 4. ∀xA(x) →A(y), если y свободно для x в формуле A(x) 5. ∀x(A → B(x)) →(A→∀xB (x)), если A не содержит свободных вхождений x Правило вывода: Modus Ponens (MP) Замечание: 1. Теория исчисления предикатов первого порядка включает в себя также правило Generalization (GEN) 2. Закон исключаещего третьего «прошит» в этой системе. Генценовская теория LK (последовательный вычислитель) Символы: →, ¬, ∧, ∨ Аксиома: I Леммирование: Cut Правила логики: 1. ∧ L1 8. ∧ R1 2. ∧ L2 9. ∧ R2 3. → L 10. → R 4. ¬ L 11. ¬ R 5. ∀ L 12. ∀ R 6. ∃ L 13. ∃ R 7. ∨ L 14. ∨ R Правила структурирования: 15. WL 18. WR 16. CL 19. CR 17. PL 20. PR Замечание: 1. Для того, что бы сделать теорию LK конструктивной (LJ) нужно изменить только правило 7.