5.6: Підформули
- Page ID
- 52992
Часто корисно говорити про формулах, які «складають» задану формулу. Ми називаємо ці його підформули. Будь-яка формула вважається підформулою себе; підформула,\(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\).