Что такое определение?
Каково формальное определение определения в математической логике или других формальных системах?
Если «А» определяется как «В», каково определение «А»? Включает ли это как «А», так и «Б» (например, «А: = В») или только «В»?
Например, на стр. 126 в § 3. Расширения с помощью определений в VIII Синтаксических интерпретациях и нормальных формах в математической логике Эббингауза , предположим, что$S$ является (нелогическим) набором символов,
3.1 Определение. Позволять$\Phi$ быть набором $S$-фразы.
(а) Предположим $P \notin S$ является $n$-арное отношение и $\phi_P(v_0, ... , v_{n-1})$ ан $S$-формула. Затем мы говорим, что$$ \forall v_0, .... \forall v_{n-1} (P v_0 ... n_{n-1} \leftrightarrow \phi_P(v_0, ... , v_{n-1})) $$ является $S$-значение $P$ в $\Phi$.
Кого я назову $S$-значение $P$ в $\Phi$:
$ \forall v_0, .... \forall v_{n-1} (P v_0 ... n_{n-1} \leftrightarrow \phi_P(v_0, ... , v_{n-1})) $?
Круглое определение $P$ с точки зрения самого себя?
Является $𝑆$-значение $𝑃$ в $Φ$ интерпретация символа $P$ как $S'$-приговор? (как часть синтаксической интерпретации из$S'$ в $S'$ сам?)
Появление $P$ в собственном определении $∀ 𝑣_0,....∀ 𝑣_{𝑛−1}(𝑃𝑣_0...v_{𝑛−1}↔𝜙_𝑃(𝑣_0,...,𝑣_{𝑛−1}))$, в том же смысле, что и появление $A$ в $𝐴:=𝐵$?
$\phi_P(v_0, ... , v_{n-1})) $? (Я думаю что$P$ определяется как $\phi_P(v_0, ... , v_{n-1})) $ в $\Phi$.)
$\phi_P$? (Сравните это со вторым:$P$ сам по себе не содержит переменных)
См. Как это определение определяет символ$P$ вне набора символов $S$ как $S$-приговор?
Благодарю.
Ответы
У нас есть подпись $S$ и мы расширяем его до $S':=S\cup\{P\}$.
В $S$-значение $P$ это $S'$-формула $$\forall v_0\dots v_{n-1}: Pv_0\dots v_{n-1}\leftrightarrow \phi_P(v_0,\dots,v_{n-1})$$что формально можно рассматривать как дополнительную аксиому к данной$S$-теория, с которой мы работаем, таким образом создавая эквивалент $S'$-теория, в которой символ $P$может использоваться как сокращение для формулы$\phi_P$.
Например, приведенная ниже формула является определением обычного отношения порядка $\le$ неотрицательных целых чисел в языке $(0,+)$: $$\forall x,y:\ x\le y\,\leftrightarrow\,\exists z: x+z=y$$
Ниже я сначала попытаюсь описать процесс более интуитивно, а затем обращусь к вашим опасениям по поводу замкнутости. Я подозреваю, что последний пункт может оказаться более полезным, поэтому не стесняйтесь сначала прочитать второй раздел - и, в частности, выделенный там девиз, я думаю, будет весьма полезным.
(Re: ваш последний комментарий, определение $(1)$- вещь, которая сообщает вам, как ведет себя новый символ в терминах старых символов, которые у вас уже есть и которые вы понимаете.)
Ключевая фраза здесь - « расширение по определениям ».
Интуитивно мы имеем в виду следующий процесс:
Начиная с подписи $S$ и некоторый набор $\Phi$ из $S$-предложения, нас немного раздражает неэффективность : есть некоторые вещи, о которых мы можем поговорить, используя$S$-формулы, но только окольными путями. Подумайте, например, о языке теории множеств,$\{\in\}$: мы можем выражать такие вещи, как "$x$ декартово произведение $y$ и $z$"на этом языке, но только с помощью досадно длинных формул. (Это хорошее упражнение для обработки предыдущего примера - например, с использованием пар Куратовского.)
Итак, учитывая нашу действительно сложную формулу $\varphi(x_0,...,x_{n-1})$, мы хотим создать новую теорию, которая в основном аналогична $\Phi$ за исключением того, что он дополнительно имеет «сокращение» для $\varphi$.
Во-первых, это означает, что мы хотим расширить наш язык: вместо того, чтобы работать с $S$ мы хотим работать с $S\cup\{R\}$ для некоторых $n$символ -арное отношение $R\not\in S$ который мы намерены использовать как сокращение для $\varphi$.
Теперь нам нужно дать определение теории на этом более широком языке. Эта теория должна включать в себя то, что у нас уже есть (то есть$\Phi$), должны правильно диктовать поведение $R$ (то есть скажем, что это сокращение от $\varphi$), и больше ничего делать не должен. Это подводит нас к рассмотрению новой теории$$\Phi':=\Phi\cup\{\forall x_0,...,x_{n-1}(R(x_0,...,x_{n-1})\leftrightarrow \varphi(x_0,...,x_{n-1})\}.$$
Отрывок из $S,\Phi$, и $\varphi$ к $S\cup\{R\}$ и $\Phi'$является расширением по определениям . Здесь есть серьезная избыточность : в точном смысле,$\Phi'$ действительно не лучше чем $\Phi$. (Формально,$\Phi'$является консервативным расширением из$\Phi$ в самом сильном смысле: каждая модель $\Phi$ имеет ровно одно расширение до модели $\Phi'$.) Это не удивительно. Мы уже знали, что можем выразить то, о чем мы заботимся, через$\varphi$, мы просто хотели сделать это быстрее.
Кстати, обратите внимание, что это предполагает естественную «максимально эффективную» версию любой теории: просто добавьте новые символы для каждой формулы! Это называется морлейизацией и иногда бывает полезно (хотя обычно выглядит глупо ).
Хорошо, а что насчет округлости, о которой вы беспокоитесь?
Во-первых, обратите внимание, что "$R$"сам по себе просто символ. Новое предложение, которое мы добавляем, на самом деле не является определением $R$, а скорее определение значения $R$, или если вы предпочитаете правило, регулирующее поведение$R$.
А если серьезно, то в FOL никогда не возникает проблем с округлостью! Ключевая идея заключается в следующем, что, на мой взгляд, является важным отходом от интуиции, которую можно привнести в программирование:
Набор предложений первого порядка не создает вещи, он описывает вещи.
В частности, набор предложений первого порядка $\Phi$вырезает особый класс структур, точные описания которых есть. Например, потенциально опасные на вид наборы$$\{\forall x(P(x)\leftrightarrow P(x))\}$$ и $$\{\forall x(Q(x)\leftrightarrow \neg Q(x))\}$$совершенно без кругов; они просто пустые (= удержание любой структуры) и противоречивые (= удержание без структуры) соответственно.