5.5: Головний оператор формули

Last updated
Save as PDF

Page ID: 53067

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

Часто корисно говорити про останній операторі, який використовується при побудові формули\(A\). Цей оператор називається головним оператором\(A\). Інтуїтивно, це «зовнішній» оператор\(A\). Наприклад, головний оператор\(\lnot A\) is\(\lnot\), основний оператор\((A \lor B)\) is і\(\lor\) т.д.

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

Основний оператор формули\(A\) визначається наступним чином:

\(\indcaseA{A}{A}\)\(\indfrm\)не має головного оператора.
\(\indcase{A}{\lnot B}\)головний оператор\(\indfrm\) is\(\lnot\).
\(\indcase{A}{(B \land C)}\)головний оператор\(\indfrm\) is\(\land\).
\(\indcase{A}{(B \lor C)}\)головний оператор\(\indfrm\) is\(\lor\).
\(\indcase{A}{(B \lif C)}\)головний оператор\(\indfrm\) is\(\lif\).
\(\indcase{A}{\lforall{x}{B}}\)головний оператор\(\indfrm\) is\(\lforall{}{}\).
\(\indcase{A}{\lexists{x}{B}}\)головний оператор\(\indfrm\) is\(\lexists{}{}\).

У кожному конкретному випадку ми маємо намір конкретне зазначене виникнення основного оператора у формулі. Наприклад, оскільки формула\(((D \lif E) \lif (E \lif D))\) має вигляд,\((B \lif C)\) де\(B\) є\((D \lif E)\) і\(C\) є\((E \lif D)\), друге входження\(\lif\) є основним оператором.

Це рекурсивне визначення функції, яка зіставляє всі неатомні формули з їх основним оператором. Через те, як формули визначаються індуктивно, кожна формула\(A\) задовольняє одному з випадків у Визначенні\(\PageIndex{1}\). Це гарантує, що для кожної\(A\) неатомної формули існує основний оператор. Оскільки кожна формула задовольняє лише одному з цих умов, і оскільки менші формули, з яких\(A\) будується, однозначно визначаються в кожному випадку, основний оператор виникнення\(A\) є унікальним, і тому ми визначили функцію.

Ми називаємо формули наступними назвами в залежності від того, який символ є їх основним оператором:

Головний оператор	Тип формули	Приклад
жоден	атомний (формула)	\(\lfalse\),\(\Atom{R}{t_1, \dots, t_n}\),\(\eq[t_1][t_2]\)
\(\lnot\)	заперечення	\(\lnot A\)
\(\land\)	сполучник	\((A \land B\))
\(\lor\)	диз'юнкція	\((A \lor B\))
\(\lif\)	умовний	\((A \lif B\))
\(\lforall{}{}\)	універсальний (формула)	\(\lforall{x}{A}\)
\(\lexists{}{}\)	екзистенціальний (формула)	\(\lexists{x}{A}\)