Язык первого порядка

    Алфавитом \(A\) называется всякое непустое конечное множество символов. Символы алфавита называются буквами.
    Словом в алфавите \(A\) называется всякая конечная последовательность букв алфавита \(A\). Пустая последовательность букв называется пустым словом и обозначается через \(\Lambda\).
    Будем говорить, что два конкретных слова \(a_{1}a_{2}...a_{n}\) и \(b_{1}b_{2}...b_{k}\) алфавита \(A\) равны и писать \(a_{1}a_{2}...a_{n}=b_{1}b_{2}...b_{k}\) если \(n=k\) и \(a_{1}=b_{1}, a_{2}=b_{2},...,a_{n}=b_{n}\). При этом число \(n\) называют длиной этого слова.
    Пусть \(T\) некоторая теория. Обозначим через \(A (T)\) алфавит этой теории. Множество \(E (T)\) слов алфавита \(A (T)\) называют множеством выражений теории \(T\).
    Пару \(\left < A(T), E (T) \right>\), состоящую из алфавита \(A (T)\) и множества выражений \(E (T)\) теории \(T\) называют языком теории \(T\).
    Языки первоrо порядка обслуживают теории первого порядка. В алфавит всякой теории \(T\) первого порядка входят по существу те же символы, которые были введены ранее. Это символы логических операций \(\wedge , \vee , \rightarrow , -\); символы кванторных операций \( \forall \), \( \exists \); вспомогательные символы - скобки, запятые; счетное множество \(n\) - местных предикатных букв \(A^{n}_{j} ( n, j\geq 1)\), где верхний индекс указывает на число мест, а нижний - номер предикатной буквы; конечное (возможно, и пустое) или счетное множество функциональных букв \(f^{n}_{j} ( n, j\geq 1)\), где верхний индекс указывает на число переменных, входящих в функцию, а нижний - номер функциональной буквы; конечное (возможно пустое) или счетное множество предметных констант \(a_{i} ( i\geq 1)\).
    В частности, под функциональной буквой может пониматься цепочка логических операций.
    Множество предикатных букв вместе с множеством функциональных букв и констант называется сигнатурой языка данной теории и является его специфической частью.
    Таким образом, в теории \(T\) первого порядка могут отсутствовать некоторые или даже все функциональные буквы и предметные константы, а также некоторые, но не все предикатные буквы.
    Различные теории первого порядка могут отличаться друг от друга по составу букв в алфавите.

    Термы и формулы

    Дальнейшее описание теории \(T\) требует прежде всего индуктивных определений терма и формулы. Термы и формулы - это два класса слов множества \(E(T)\).
    Определение терма.
    1. Предметная переменная и предметная константа суть термы.
    2. Если \(r_{1},r_{2},...,r_{n}\) - термы и \(A\) - символ \(n\)-местной операции, то \(A_{i}^{n} (r_{1},r_{2},...,r_{n})\) терм.
    3. Никаких других, термов кроме определенных в п. 1 и п. 2, в \(T\) нет.
    Согласно естественной интерпретации, терм - это имя некоторого предмета. Кроме переменных и предметных констант, термами являются цепочки, образованные из переменных и предметных констант посредством символ операций, так как в подразумеваемой интерпретации он истолковывается как значение некоторой функции.
    Определение формулы.
    1. Если \(A\) - символ \(n\)-местного отношения (предикат или функция), а \(r_{1},r_{2},...,r_{n}\) - термы, то \(A (r_{1},r_{2},...,r_{n})\) - формула. В частности, если \(A\) - предикатная буква \(A_{i}^{n}\), то \(A_{i}^{n}(r_{1},r_{2},...,r_{n})\) называется элементарной формулой.
    2. Если \(A\) и \(B\) формулы, то \(A\wedge B , A \vee B, A \rightarrow B, \bar{A}\) формулы.
    3. Если \(A\) - формула, а \(y\) - предметная переменная, которая входит в \(A\) свободно или не содержится в \(A\), то выражения \( \forall y A \), \( \exists y A \) - формулы. При этом \(A\) называется областью действия квантора.
    4. Никаких дрyrих формул, кроме определенных в п. 1 - 3, нет.

    Логические и специальные аксиомы. Правила вывода

    Аксиомы теории первоrо порядка \(T\) разбиваются на два класса: логические аксиомы и специальные (нелогические или собственные аксиомы).
    Логические аксиомы. Каковы бы ни были формулы \(A\), \(B\) и \(C\) теории \(T\), следующие формулы являются логическими аксиомами теории \(T\):
    1) \(A\rightarrow (B \rightarrow A)\);
    2) \(( A\rightarrow (B \rightarrow C) ) \rightarrow (( A \rightarrow B)\rightarrow (A \rightarrow C))\);
    3) \((\bar{B}\rightarrow \bar{A}) \rightarrow ((\bar{B} \rightarrow A) \rightarrow B)\);
    4) \(\forall x_{i} A x_{i} \rightarrow A (t)\), где \(A (x_{i})\) есть формула теории \(T\) и \(t\) есть терм теории \(T\), свободный в \(A (x_{i})\). Отметим, что \(t\) может совпадать с \(x_{i}\), и тогда мы приходим к аксиоме \(\forall x_{i} A x_{i} \rightarrow A (x_{i})\);
    5) \(\forall x_{i} ( A \rightarrow B) \rightarrow ( A \rightarrow \forall x_{i} B)\),если \(x_{i}\) не входит свободно в формулу \(A\).
    Замечание. Ранее было построено классическое исчисление высказываний, которое содержало 11 аксиом. Однако может быть построено исчисление высказываний с меньшим числом аксиом (в частности, с логическими аксиомами 1) - 3).
    Специальные аксиомы. Они не могут быть сформулированы в общем случае, так как меняются от теории к теории.
    Теория первого порядка, не содержащая собственных аксиом, очевидно, представляет собой чисто логическую теорию. Она носит название исчисления предикатов первого порядка.
    Во многих теориях, которые могут быть аксиоматизированы как теории первого порядка, используется понятие равенства. Оно вводится путем добавления двухмерного предиката "\(x=y\)" и в связи с этим добавляются две специальные аксиомы:
    1) \(\forall x (x=x)\).
    2) Если \(x\), \(y\), \(z\) - различные предметные переменные \(F (z) \) - формула, то \(\forall x \forall y (x= x\rightarrow F(x)=F(y) )\).
    Правила вывода. Как и в исчислении высказываний, будем пользоваться понятиями вывода из совокупности формул (высказываний) \(H\). Высказывания, входящие в \(H\), будем называть допущениями (или посылками). Если последним высказыванием в выводе из \(H\) стоит высказывание \(A\), то будем говорить, что предложение \(A\) выводимо из \(H\) и записывать: \(H\vdash A\). В частном случае, если \(H = \oslash\), то пишут \(\vdash A\).
    В число правил вывода теории первого порядка включаются два правила:
    1. Правило заключения (или modus ponens): $$\frac{\vdash A,\vdash A \rightarrow B}{\vdash B}.$$
    2. Правило связывания квантором всеобщности (или правило обобщения): $$\frac{\vdash A}{\vdash \forall x_{i} A}.$$


2012-11-14 • Просмотров [ 2781 ]