5.3: Терміни та формули

Last updated
Save as PDF

Page ID: 53036

\( \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

Після того, як\(\Lang L\) вказано мову першого порядку, ми можемо визначити вирази, побудовані з базового словникового запасу\(\Lang L\). До них відносяться, зокрема, терміни і формули.

Визначення\(\PageIndex{1}\): Terms

Сукупність \(\Trm[L]\)термінів\(\Lang L\) визначається індуктивно:

Кожна змінна є терміном.
Кожен постійний символ\(\Lang L\) - це термін.
Якщо\(f\) є символом функції\(n\) -place і\(t_1\),...,\(t_n\) є термінами, то\(\Atom{f}{t_1, \ldots, t_n}\) є терміном.
Ніщо інше не є терміном.

Термін, що не містить змінних, є закритим терміном.

Постійні символи з'являються в нашій специфікації мови та термінів як окрема категорія символів, але замість цього вони могли бути включені як символи функції нульового місця. Тоді ми могли б обійтися без другого пункту у визначенні термінів. Ми просто повинні розуміти,\(\Atom{f}{t_1, \ldots, t_n}\) як тільки самі\(f\) по собі, якщо\(n = 0\).

Визначення\(\PageIndex{2}\): Formula

Набір \(\Frm[L]\)формул мови\(\Lang L\) визначається індуктивно наступним чином:

\(\lfalse\) is an atomic formula.
Якщо\(R\) є символом присудка\(n\) -place\(\Lang L\) і\(t_1\),...,\(t_n\) є членами\(\Lang L\), то\(\Atom{R}{t_1,\ldots, t_n}\) є атомною формулою.
Якщо\(t_1\) і\(t_2\) є членами\(\Lang L\), то\(\Atom{\eq[][]}{t_1, t_2}\) є атомною формулою.
Якщо\(A\) is a formula, then \(\lnot A\) is formula.
Якщо\(A\) and \(B\) are formulas, then \((A \land B)\) is a formula.
Якщо\(A\) and \(B\) are formulas, then \((A \lor B)\) is a formula.
Якщо\(A\) and \(B\) are formulas, then \((A \lif B)\) is a formula.
Якщо\(A\) is a formula and \(x\) is a variable, then \(\lforall{x}{A}\) is a formula.
Якщо\(A\) is a formula and \(x\) is a variable, then \(\lexists{x}{A}\) is a formula.
Ніщо інше не є формулою.

Визначення множини термінів та формул є індуктивними визначеннями. По суті, ми будуємо набір формул в нескінченно багато етапів. На початковій стадії ми вимовляємо всі атомні формули формулами; це відповідає першим декільком випадкам визначення, тобто відмінкам для\(\lfalse\), \(\Atom{R}{t_1,\dots,t_n}\) і\(\Atom{\eq[][]}{t_1,t_2}\). «Атомна формула» таким чином означає будь-яку формулу такої форми.

Інші випадки визначення дають правила побудови нових формул з уже побудованих формул. На другому етапі ми можемо використовувати їх для побудови формул з атомних формул. На третьому етапі будуємо нові формули з атомних формул і отриманих на другому етапі і так далі. Формула - це все, що врешті-решт будується на такому етапі, і нічого іншого.

За умовністю пишемо\(\eq[][]\) між його аргументами і залишаємо в дужках:\(\eq[t_1][t_2]\) є абревіатурою для\(\Atom{\eq[][]}{t_1,t_2}\). Більш того,\(\lnot \Atom{\eq[][]}{t_1,t_2}\) скорочено позначається як\(\eqN[t_1][t_2]\). При написанні формули\(B\),\((B \ast C)\) побудованої з,\(C\) використовуючи двомісну сполучну\(\ast\), ми часто залишаємо крайню пару дужок і пишемо просто\(B \ast C\).

Деякі логічні тексти вимагають, що змінна\(x\) повинна відбуватися для\(A\) того,\(\lforall{x}{A}\) щоб\(\lexists{x}{A}\) і вважати формулами. Нічого поганого не відбувається, якщо ви цього не вимагаєте, і це полегшує ситуацію.

Визначення\(\PageIndex{3}\)

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

\(\ltrue\) abbreviates \(\lnot\lfalse\).
\(A \liff B\) abbreviates \((A \lif B) \land (B \lif A)\).

Якщо ми працюємо мовою для певної програми, ми часто пишемо двомісні присудкові символи та символи функцій між відповідними термінами, наприклад,\(t_1 < t_2\) і\((t_1 + t_2)\) мовою арифметики та\(t_1 \in t_2\) мовою теорії множин. Функція-наступник мовою арифметики навіть записується умовно після її аргументу:\(t'\). Офіційно, однак, це всього лише умовні скорочення для\(\Atom{\Obj A^2_0}{t_1, t_2}\)\(\Obj f^2_0(t_1, t_2)\),\(\Atom{\Obj A^2_0}{t_1, t_2}\) і\(f^1_0(t)\), відповідно.

Визначення\(\PageIndex{4}\): Syntactic identity

Символ\(\ident\) виражає синтаксичну ідентичність між рядками символів, тобто\(A \ident B\) iff\(A\) і\(B\) є рядками символів однакової довжини і які містять один і той же символ в кожному місці.

\(\ident\)Символ може бути обрамлений рядками, отриманими шляхом конкатенації, наприклад,\(A \ident (B \lor C)\) означає: рядок символів\(A\) - це той самий рядок, що і той, що отримується шляхом об'єднання відкриваючої дужки, рядка\(B\), \(\lor\)символ\(C\), рядок і закриваюча дужка, в такому порядку. Якщо це так, то ми знаємо, що перший символ\(A\) - це відкриваюча дужка,\(A\) містить\(B\) як підрядок (починаючи з другого символу), що підрядок слідує і\(\lor\) т.д.