5.2: Мови першого порядку

Last updated
Save as PDF

Page ID: 53076

\( \newcommand{\vecs}[1]{\overset { \scriptstyle \rightharpoonup} {\mathbf{#1}} } \) \( \newcommand{\vecd}[1]{\overset{-\!-\!\rightharpoonup}{\vphantom{a}\smash {#1}}} \)\(\newcommand{\id}{\mathrm{id}}\) \( \newcommand{\Span}{\mathrm{span}}\) \( \newcommand{\kernel}{\mathrm{null}\,}\) \( \newcommand{\range}{\mathrm{range}\,}\) \( \newcommand{\RealPart}{\mathrm{Re}}\) \( \newcommand{\ImaginaryPart}{\mathrm{Im}}\) \( \newcommand{\Argument}{\mathrm{Arg}}\) \( \newcommand{\norm}[1]{\| #1 \|}\) \( \newcommand{\inner}[2]{\langle #1, #2 \rangle}\) \( \newcommand{\Span}{\mathrm{span}}\) \(\newcommand{\id}{\mathrm{id}}\) \( \newcommand{\Span}{\mathrm{span}}\) \( \newcommand{\kernel}{\mathrm{null}\,}\) \( \newcommand{\range}{\mathrm{range}\,}\) \( \newcommand{\RealPart}{\mathrm{Re}}\) \( \newcommand{\ImaginaryPart}{\mathrm{Im}}\) \( \newcommand{\Argument}{\mathrm{Arg}}\) \( \newcommand{\norm}[1]{\| #1 \|}\) \( \newcommand{\inner}[2]{\langle #1, #2 \rangle}\) \( \newcommand{\Span}{\mathrm{span}}\)

Template:MathJaxZach

Вирази логіки першого порядку будуються з базового словника, що містить змінні, постійні символи, символи предикатів і іноді функціональні символи. З них разом з логічними зв'язками утворюються квантори, а також розділові символи, такі як дужки і коми, терміни і формули.

Неофіційно символи предикатів - це імена властивостей і відносин, постійні символи - це імена для окремих об'єктів, а символи функцій - імена для відображення. Вони, крім присудка ідентичності\(\eq[][]\), є нелогічними символами і разом складають мову. Будь-яка мова першого порядку\(\Lang L\) визначається його нелогічними символами. У самому загальному випадку\(\Lang L\) містить нескінченно багато символів кожного виду.

У загальному випадку ми використовуємо такі символи в логіці першого порядку:

Логічні символи
1. Логічні зв'язки:\(\lnot\) (negation),\(\land\) (conjunction),\(\lor\) (disjunction),\(\lif\) (conditional),\(\lforall{}{}\) (universal quantifier),\(\lexists{}{}\) (existential quantifier).
2. Пропозиційна константа для фальші\(\lfalse\).
3. Двомісне присудок ідентичності\(\eq[][]\).
4. Зліченно нескінченний набір змінних:\(\Obj v_0\)\(\Obj v_1\),,\(\Obj v_2\),...
Нелогічні символи, що складають стандартну мову логіки першого порядку
1. Зліченно нескінченний набір символів\(n\) -place присудок для кожного\(n>0\):\(\Obj A^n_0\),\(\Obj A^n_1\),\(\Obj A^n_2\),...
2. Зліченно нескінченний набір постійних символів:\(\Obj c_0\),\(\Obj c_1\),\(\Obj c_2\),,...
3. Зліченно нескінченний набір символів функції\(n\) -place для кожного\(n>0\):\(\Obj f^n_0\),\(\Obj f^n_1\),\(\Obj f^n_2\),...
Знаки пунктуації: (,), і кома.

Більшість наших визначень та результатів буде сформульовано для повної стандартної мови логіки першого порядку. Однак, залежно від програми, ми також можемо обмежити мову лише кількома символами предикатів, постійними символами та символами функцій.

Приклад\(\PageIndex{1}\)

Мова\(\Lang L_A\) арифметики містить один двомісний предикатний символ\(<\), єдиний постійний символ\(\Obj 0\), один символ\(\prime\) функції одного місця та два два символи функції\(+\) та \(\times\).

Приклад\(\PageIndex{2}\)

Мова теорії\(\Lang L_Z\) множин містить лише єдиний двомісний присудковий символ\(\in\).

Приклад\(\PageIndex{3}\)

Мова ордерів\(\Lang L_\le\) містить тільки двомісний присудковий символ\(\le\).

Знову ж таки, це умовності: офіційно, це просто псевдоніми, наприклад\(<\),\(\in\),, і\(\le\) є псевдонімами for\(\Obj A^2_0\),\(\Obj 0\) for\(\Obj c_0\),\(\prime\) for\(\Obj f^1_0\), \(+\)для\(\Obj f^2_0\),\(\times\) для\(\Obj f^2_1\).

Крім примітивних зв'язків і квантифікаторів, представлених вище, ми також використовуємо такі визначені символи:\(\liff\) (biconditional), truth \(\ltrue\).

Визначений символ офіційно не є частиною мови, але вводиться як неформальна абревіатура: він дозволяє нам скорочувати формули, які б, якби ми використовували лише примітивні символи, отримати досить довгі. Це, очевидно, перевага. Однак більшою перевагою є те, що докази стають коротшими. Якщо символ примітивний, він повинен розглядатися окремо в доказах. Отже, чим примітивніше символи, тим довше наші докази.

Можливо, ви знайомі з іншою термінологією та символами, ніж ті, які ми використовуємо вище. Логічні тексти (і вчителі) зазвичай використовують або\(\sim\)\(\neg\), і! для «заперечення»,\(\wedge\)\(\cdot\), і\(\&\) для «кон'юнкції». Загальноприйняті символи для «умовного» або «імплікації» є\(\rightarrow\)\(\Rightarrow\), і\(\supset\). Символи для «біумовного», «бі-імплікації» або «(матеріальної) еквівалентності» є\(\leftrightarrow\), \(\Leftrightarrow\), and \(\equiv\).\(\lfalse\) symbol is variously called “falsity,” “falsum,” “absurdity,” or “bottom.” The\(\ltrue\) symbol is variously called “truth,” “verum,” or “top.”

Звичайним є використання малих літер (наприклад,,\(a\)\(b\),\(c\)) від початку латинського алфавіту для постійних символів (іноді їх називають іменами), а малі літери з кінця (наприклад,,,\(x\),\(y\), \(z\)) для змінних. Квантори поєднуються зі змінними, наприклад,\(x\); нотаційні варіації включають\(\forall x\)\((\forall x)\),\((x)\),\(\Pi x\),,\(\bigwedge_x\) для універсального квантора і\(\exists x\), \((\exists x)\),\((Ex)\),\(\Sigma x\),\(\bigvee_x\) для екзистенціального квантора.

Ми можемо розглядати всі оператори пропозиції та обидва квантори як примітивні символи мови. Ми могли б замість цього вибрати менший запас примітивних символів і розглядати інші логічні оператори, як визначено. «Істина функціонально повна» множини логічних операторів включають\(\{ \lnot, \lor \}\)\(\{ \lnot, \land \}\), і\(\{ \lnot, \lif\}\) —thes можуть бути об'єднані з будь-яким квантором для виразно повної мови першого порядку.

Можливо, ви знайомі з двома іншими логічними операторами: інсультом Шеффер\(|\) (названий на честь Генрі Шеффер) та стрілою Пірса\(\downarrow\), також відомою як кинджал Квін. Коли дані їх звичайні показання «nand» і «nor» (відповідно), ці оператори є істинно функціонально завершеними самі по собі.