5.6: Підформули

Last updated
Save as PDF

Page ID: 52992

\( \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\) себе, є належною підформулою.

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

Якщо\(A\) є формулою, безпосередні підформули\(A\) визначаються індуктивно наступним чином:

Атомні формули не мають безпосередніх підформул.
\(\indcase{A}{\lnot B}\)Єдина безпосередня підформула\(\indfrm\) є\(B\).
\(\indcase{A}{(B \ast C)}\)Безпосередні підформули\(\indfrm\) є\(B\) і\(C\) (\(\ast\)є будь-яким з двомісних з'єднань).
\(\indcase{A}{\lforall{x}{B}}\)Єдина безпосередня підформула\(\indfrm\) є\(B\).
\(\indcase{A}{\lexists{x}{B}}\)Єдина безпосередня підформула\(\indfrm\) є\(B\).

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

Якщо\(A\) є формулою, правильні підформули\(A\) рекурсивно виглядають наступним чином:

Атомні формули не мають належних підформул.
\(\indcase{A}{\lnot B}\)Правильні підформули\(\indfrm\) знаходяться\(B\) разом з усіма власними підформулами\(B\).
\(\indcase{A}{(B \ast C)}\)Правильні підформули\(\indfrm\) є\(B\)\(C\), разом з усіма власними підформулами\(B\) і тими з\(C\).
\(\indcase{A}{\lforall{x}{B}}\)Правильні підформули\(\indfrm\) знаходяться\(B\) разом з усіма власними підформулами\(B\).
\(\indcase{A}{\lexists{x}{B}}\)Правильні підформули\(\indfrm\) знаходяться\(B\) разом з усіма власними підформулами\(B\).

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

Підформули\(A\) є\(A\) самі собою разом з усіма власними підформулами.

Зверніть увагу на тонку різницю в тому, як ми визначили негайні підформули та відповідні підформули. У першому випадку ми безпосередньо визначили безпосередні підформули формули\(A\) для кожної можливої форми\(A\). Це явне визначення за відмінками, а відмінки відображають індуктивне визначення набору формул. У другому випадку ми також віддзеркалили спосіб визначення набору всіх формул, але в кожному випадку ми також включили правильні підформули менших формул\(B\),\(C\) крім самих цих формул. Це робить визначення рекурсивним. Загалом, визначення функції на індуктивно визначеному множині (у нашому випадку формули) є рекурсивним, якщо випадки у визначенні функції використовують саму функцію. Щоб бути чітко визначеними, ми повинні переконатися, що ми коли-небудь використовуємо значення функції лише для аргументів, які приходять «перед» тим, який ми визначаємо - у нашому випадку, при визначенні «правильної підформули», оскільки\((B \ast C)\) ми використовуємо лише відповідні підформули «більш ранніх» формул \(B\)і\(C\).