Языки и исчисления


Аксиомы и правила вывода - часть 4


(квадратные скобки указывают порядок действий, не являясь частью формулы);

  • подстановка терма вместо переменной в формулу корректна, если она корректна для обеих формул и , при этом

    аналогично для формул и ;

  • наконец, подстановка вместо в формулу корректна в двух случаях:

    (1) если не является параметром формулы (это возможно, когда не является параметром или когда совпадает с ); при этом подстановка ничего не меняет в формуле;

    (2) переменная является параметром формулы , но переменная не входит в терм и подстановка корректна; при этом

    Аналогично определяется корректная подстановка в формулу .

  • Главная часть в этом определении — последний его пункт, который, во-первых, говорит, что вместо связанных вхождений переменных ничего подставлять не надо, а во-вторых, требует, чтобы при корректной подстановке переменные из терма не подпадали под действие одноименных кванторов.

    После всех этих приготовлений мы можем сформулировать две оставшиеся схемы аксиом исчисления предикатов: формула

    (12)

    и двойственная ей формула

    (13)

    будут аксиомами исчисления предикатов, если указанные в них подстановки корректны.

    Два частных случая, когда подстановка заведомо корректна: во-первых, можно безопасно подставлять константу (или любой терм без параметров), во-вторых, подстановка переменной вместо себя всегда корректна (и ничего не меняет в формуле).

    Отсюда следует, что формулы

    и будут аксиомами исчисления предикатов (для любой формулы и переменной ).

    Нужны ли нам еще какие-нибудь аксиомы и правила вывода? Конечно, нужны, поскольку уже сформулированные аксиомы не полностью отражают смысл кванторов. (Например, они вполне согласуются с таким пониманием этого смысла: формула всегда ложна, а формула

    всегда истинна.) Поэтому мы введем в наше исчисление два правила вывода, называемые правилами Бернайса, и на этом определение исчисления предикатов будет завершено. (Позже мы рассмотрим дополнительные аксиомы, отражающие специальный статус предиката равенства.

    Если переменная не является параметром формулы , то правила Бернайса разрешают такие переходы:




    - Начало -  - Назад -  - Вперед -



    Книжный магазин