Огранич. обл. определения при интерпретации ф./п. символов

[arseniiv]

На волне недавних тем насчёт логики вспомнил про эту вещь и опишу здесь возникший велосипед (практически никакой свободы выбора деталей не было, потому это наверняка уже триста раз придумывали и просто трудно найти).

Обычно для простоты изложения [предикатные и функциональные] символы языка интерпретируются как отношения и операции на всей области интерпретации. Если при этом мы имеем дело, скажем, с операцией взятия обратного элемента в кольце, она доопределяется на элементах, у которых нет обратного, как угодно, т. к. формулы с «неправильным» использованием соответствующего символа появляться не должны. Лично мне такой подход когда-то был странен, но сейчас привычен, что всё равно не мешает рассмотреть более сложную альтернативу (которая, возможно, прошлому мне понравилась бы больше [после написания уже не так уверен]).

Для этого внесём несколько изменений в определения формулы первого порядка и интерпретации. Формулой теперь будет ещё и конструкция $\mathrm{defined}(e)$ для любого терма или формулы $e$ соответствующего языка. Интерпретации коснётся куча изменений, так что определим всё с нуля. Пусть множество формул нашего видоизменённого языка — $\mathcal F$, термов — $\mathcal T$, переменных — $\mathcal V$, функциональных символов — $F$, предикатных символов — $P$; множество $B^A$ будем также обозначать $A\to B$; $A^* := \bigcup_{n=0}^\infty A^n$; множество логических значений $\mathbb B := \{0,1\}$ с обычными операциями $\wedge,\vee,\to,\neg,\ldots$ на нём.

Интерпретацией языка назовём набор из
• области интерпретации $A$;
• функции областей определения $D\colon F\cup P\to2^{A^*}$, причём должно выполняться $D(s)\subset A^{\operatorname{arity}(s)}$ (хотя можно этого — вместе с фиксированностью арности — не требовать, но тут это оффтоп);
• интерпретаций символов $I\colon F\to(A^*\to A)$, $I\colon P\to(A^*\to\mathbb B)$, причём должно выполняться $\operatorname{dom}I(s) = D(s)$;
• функции определённости термов $DI\colon\mathcal T\times(\mathcal V\to A)\to\mathbb B$ такой, что $DI(f(t_1,\ldots,t_n),w) = DI(t_1,w)\wedge\ldots\wedge DI(t_n,w)\wedge{}$ $(I(t_1,w),\ldots,I(t_n,w))\in D(f)$ и $DI(v,w) = 1$;
• функции интерпретации термов $I\colon\mathcal T\to(\mathcal V\to A)\to A$ такой, что $I(f(t_1,\ldots,t_n),w) = I(f)(I(t_1,w),\ldots,I(t_n,w))$, если правая часть равенства определена, и $I(v,w) = w(v)$ — а если не $DI(t,w)$, $I(t,w)$ может быть чем угодно;
• функции определённости формул $DI\colon\mathcal F\times(\mathcal V\to A)\to\mathbb B$ такой, что:
$DI(p(t_1,\ldots,t_n),w) = DI(t_1,w)\wedge\ldots\wedge DI(t_n,w)\wedge{}$ $(I(t_1,w),\ldots,I(t_n,w))\in D(p)$,
$DI(\neg A,w) = DI(A,w)$,
$DI(A\wedge B,w) = DI(A,w)\wedge DI(B,w)\vee DI(A,w)\wedge\neg I(A,w)\vee{}$ $DI(B,w)\wedge\neg I(B,w)$,
$DI(A\vee B,w) = DI(A,w)\wedge DI(B,w)\vee DI(A,w)\wedge I(A,w)\vee{}$ $DI(B,w)\wedge I(B,w)$,
$DI(A\to B,w) = DI(A,w)\wedge DI(B,w)\vee DI(A,w)\wedge\neg I(A,w)\vee{}$ $DI(B,w)\wedge I(B,w)$,
$DI(A\leftrightarrow B,w)$ тоже по смыслу,
$DI(\forall xA,w)$ в соответствие с тем, как у $\wedge$,
$DI(\exists xA,w)$ в соответствие с тем, как у $\vee$,
$DI(\operatorname{defined}(e),w) = 1$;
• функции интерпретации формул $I\colon\mathcal F\times(\mathcal V\to A)\to\mathbb B$ такой, что:
$I(p(t_1,\ldots,t_n),w) = I(p)(I(t_1,w),\ldots,I(t_n,w))$, если правая часть равенства определена, или что угодно вместо неё,
$I(A\wedge B,w),\ldots,I(\exists xA,w)$ как для формул первого порядка в классической логике,
$I(\operatorname{defined}(e),w) = DI(e,w)$.

Уф, всё. Будем теперь говорить, что формула/терм $e$ имеет значение $I(e,w)$ в данной интерпретации при значениях переменных $w$, если $DI(e,w)=1$, а в противном случае говорить, что $e$ бессмысленно. Будем называть формулу $e$ общезначимой, если она имеет значение $1$ во всех интерпретациях, etc.. Сразу натыкаемся на особенность этой системы: если взять любую формулу $A$, $A\vee\neg A$ получится не всегда общезначимой (а мы не пытались вылезать за пределы классической логики — см. определение $I$ для формул), т. к. любые входящие туда символы могут интерпретироваться нигде не определённой функцией. Что и чем можно заменять, нуждается в уточнении. Если рассмотреть язык с равенством, аналогичная ситуация будет с получением «тавтологий» вида $\sqrt{-2}=\sqrt{-2}$.

Выход, впрочем, тоже виден — раз мы ввели в язык определённость, надо её учитывать; нельзя просто заменить в формуле $A$ свободные вхождения какой-то переменной $v$ на терм $t$, нужно взять в качестве результата «замены» сразу $\operatorname{defined}(t)\to A[t/v]$; аналогично с заменой пропозициональных переменных в схемах аксиом или ещё где.

Перевод из таких языков в обычные языки первого порядка с тем же набором символов + по символу для всех $\operatorname{defined}(f(\ldots))$, прозрачен. В обратную сторону тоже. Вопрос о расширениях теории определением нового символа тоже, кажется, прозрачен (в определяющую $f$ аксиому будет входить ещё и предложение $\forall\vec v(\operatorname{defined}(f(\ldots))\leftrightarrow\ldots)$) и т. п.).

Штука кажется всё же неудобной (но, по идее, подобные вещи мы будем делать и в обычной обстановке, где в свободной записи попадаются даже штуки вида $\exists f'(a)$ или $\exists\lim\ldots$ — по смыслу это $\mathrm{defined}$). Может быть, кто-то знает лучшие описания подобного? И не забыл ли я чего-то в этом описании (кроме лени дописать про $DI$ и $I$)?

(Никого не склоняю этим пользоваться, и сам тоже, повторюсь, не в восторге.)

-- Пн июл 18, 2016 04:20:27 --

P. S. Можно было бы слить $DI$ и $I$ вместе, используя специальное значение для неопределённости. Тогда это станет напоминать трёхзначную логику (ту, в которой $a\to b=\neg a\vee b$) (и у которой довольно неудобные свойства), но только напоминать из-за того, что есть $\mathrm{defined}$. Кажется.

P. P. S. Предлагаю вместо $\operatorname{defined(e)}$ набирать менее длинное $\Delta(e)$. Если кому-то это вообще придётся набирать.

[Свободный Художник]

arseniiv в сообщении #1138552 писал(а):

На волне недавних тем насчёт логики вспомнил про эту вещь и опишу здесь возникший велосипед (практически никакой свободы выбора деталей не было, потому это наверняка уже триста раз придумывали и просто трудно найти).

Обычно для простоты изложения [предикатные и функциональные] символы языка интерпретируются как отношения и операции на всей области интерпретации. Если при этом мы имеем дело, скажем, с операцией взятия обратного элемента в кольце, она доопределяется на элементах, у которых нет обратного, как угодно, т. к. формулы с «неправильным» использованием соответствующего символа появляться не должны. Лично мне такой подход когда-то был странен, но сейчас привычен, что всё равно не мешает рассмотреть более сложную альтернативу (которая, возможно, прошлому мне понравилась бы больше [после написания уже не так уверен]).

Если говорить о работе с функциональными символами некоторой первопорядковой теории, предполагаемой интерпретацией которых являются частично определенные функции, то можно воспользоваться механизмом "пресуппозиций". Здесь я неформально продемонстрировал работу этого механизма на интересующем меня примере:
http://www.px-pict.com/9/6/4/5/1/2.html

Но почти что стороцентно уверен, что такой механизм уже где-то формализован. Можно, конечно, и самому попробовать формализовать. При этом лучше опираться на стандартную терминологию из замечательной книги:
Кейслер Г. Дж., Чэн Ч.Ч.
Теория моделей. Пер. с англ., М.: Мир, 1977
Ее оглавление и предисловие к ней приведены по ссылке ниже:
http://www.px-pict.com/9/6/2/8/4.html

[arseniiv]

У меня в качестве ваших пресуппозиций выступает $\Delta(\ldots)$. Если формула $A$ в некоторых интерпретациях бессмысленна, формулы $\Delta(A)\to A$ или $\Delta(A)\wedge A$ будут лишены этого недостатка и будут соответственно истинной и ложной в тех интерпретациях, в которых $A$ бессмысленна.

[Свободный Художник]

Давайте на конкретном примере первопорядковой теории полугрупп. Я позволю себе воспользоваться определением первопорядкового языка по Кейслеру - Чэну:
http://www.px-pict.com/9/6/2/4/1/1.html
Сначала рассмотрим немодифицированную первопорядковую теорию полугрупп. Пусть $\bullet$ будет единственным бинарным функциональным символом ее первопорядкового языка $L$. Таким образом, $L$ является одноэлементным множеством $L = \{\bullet \}$.
Интерпретацией нашего языка будет произвольное отображение из этого одноэлементного множества в бесконечное семейство упорядоченных пар вида: $< D, f >$, где $D$ есть некоторое непустое множество, а $f$ есть некоторая всюду определенная бинарная функция на множестве $D$.
Единственной аксиомой нашей немодифицированой пока первопорядковой теории полугрупп будет универсальное предложение
$\forall x \forall y \forall z [(x \bullet y) \bullet z = x\bullet (y \bullet z)]$.

-- Пн июл 18, 2016 23:54:32 --

Мое предложение по модификации первопорядковых теорий с целью возможности работы с пресуппозициями включает в себя, прежде всего, модификацию приведенного выше определения языка первопорядковой теории по Кейслеру-Чэну. Если такой язык содержит непустое множество $F$ функциональных символов, то он теперь в обязательном порядке должен будет содержать и равномощное ему множество предикатных символов $P_1$ вместе с некоторой фиксированной биекцией $\pi: F \to P_1$, такой что для любого $n$ - арного символа $\varphi$ из $F$, $\pi(\varphi)$ есть некоторый $n+1$ - арный предикатный символ из $P_1$, содержательно интерпретируемый как пресуппозиция для соответствующего функционального символа.
Подробности несколько позже.

[arseniiv]

Ну, вообще-то, не единственной, а единственной собственной. В любом случае, из обычной аксиомы $A$ легко делается «исправленная»

arseniiv в сообщении #1138633 писал(а):

$\Delta(A)\to A$

Вопрос, если он вообще есть, тут в другом. Например, какие аксиомы, содержащие $\Delta$, нужно добавить к логическим, чтобы аксиоматизировать поведение функции $DI$ интерпретации. Например, если $x$ — переменная, $f,c$ — предикатные символы арностей 1 и 0 соотв., то $\vDash\forall x(\Delta(f(x)))\wedge\Delta(c)\to\Delta(f(c))$, но из аксиом логики первого порядка не вывести, а хотелось бы манипулировать формулами с $\Delta$ в выводах свободно. Впрочем, я уверен, что всё нужное можно получить весьма механически, а мне делать это просто лень, и меня интересовало не то, как я могу сделать текущее описание более полным, а то, встречал ли кто-то что-нибудь подобное и где, и что вообще может сказать по поводу написанного без комментариев с моей стороны.

[Свободный Художник]

arseniiv в сообщении #1138633 писал(а):

У меня в качестве ваших пресуппозиций выступает $\Delta(\ldots)$.

Хотелось бы оформить это гораздо проще. У меня появилось желание и возможность продолжить одну свою старую работу, в которой фигурировала частичная бинарная операция "действия":
http://www.px-pict.com/9/6/7/4.html
и удобная формализация механизма работы с пресуппозициями мне очень нужна.

arseniiv в сообщении #1138727 писал(а):

... из аксиом логики первого порядка не вывести, а хотелось бы манипулировать формулами с $\Delta$ в выводах свободно.

И конечно, все должно как можно проще выводиться из аксиом логики первого порядка.

Свободный Художник в сообщении #1138712 писал(а):

Если такой язык содержит непустое множество $F$ функциональных символов, то он теперь в обязательном порядке должен будет содержать и равномощное ему множество предикатных символов $P_1$ вместе с некоторой фиксированной биекцией $\pi: F \to P_1$, такой что для любого $n$ - арного символа $\varphi$ из $F$, $\pi(\varphi)$ есть некоторый $n + 1$ - арный предикатный символ из $P_1$, содержательно интерпретируемый как пресуппозиция для соответствующего функционального символа.

Здесь у меня опечатка. Должно быть:
Если такой язык содержит непустое множество $F$ функциональных символов, то он теперь в обязательном порядке должен будет содержать и равномощное ему множество предикатных символов $P_1$ вместе с некоторой фиксированной биекцией $\pi: F \to P_1$, такой что для любого $n$ - арного символа $\varphi$ из $F$, $\pi(\varphi)$ есть некоторый $n$ - арный предикатный символ из $P_1$, содержательно интерпретируемый как пресуппозиция для соответствующего функционального символа.

[arseniiv]

Свободный Художник в сообщении #1138905 писал(а):

Хотелось бы оформить это гораздо проще.

Ну куда тут проще. Вместо того чтобы вводить по специальному предикатному символу определённости для каждого «частичному» предикатного и функционального символа, здесь единственная конструкция — $\Delta(e)$, где $e$ — любой терм или формула.

Свободный Художник в сообщении #1138905 писал(а):

И конечно, все должно как можно проще выводиться из аксиом логики первого порядка.

Всё не получится просто по смыслу того, что тут наделано. В модальных логиках множества аксиом дополняются по сравнению с «основной», тут аналогично. Нужны аксиомы типа $\Delta(\Delta(t))$, $\Delta(\Delta(A))$, $\Delta(A)\leftrightarrow\Delta(\neg A)$ и т. д. ($t$ — терм, $A$ — формула).

[arseniiv]

Давайте вот для сравнения то, что делается классически. Я упоминал выше кольцо и обратные элементы, но сойдёт и моноид.

1. Сначала у нас есть теория $\mathcal M^-$ в языке $(*)$ с собственными аксиомами $(x*y)*z = x*(y*z)$, $\exists a(a*x=x\wedge x*a=x)$.

2. Мы хотим расширить эту теорию определением нейтрального элемента $e:\forall x(e*x=x\wedge x*e=x)$ и получить теорию $\mathcal M$ в языке $(*,e)$. Это возможно, потому что $\mathcal M^-\vdash\exists!a(a*x=x\wedge x*a=x)$ ($\exists!\ldots$ воспринимаем как сокращение). Имеем теорию $\mathcal M$, аксиомы которой — аксиомы $\mathcal M^-$ плюс $e*x=x\wedge x*e=x$, и она является консервативным расширением $\mathcal M^-$. Также им была бы теория $\mathcal M$, из аксиом которой $\exists a(a*x=x\wedge x*a=x)$ удалена, но это тут ни при чём.

3. Мы хотим расширить $\mathcal M$ определением правого обратного элемента $x':x*x'=e$ и получить теорию $\mathcal{MI}$ в языке $(*,e,')$, но не можем этого сделать, потому что $\mathcal M\not\vdash\exists!y(x*y=e)$ (и обозначим $I(x):=\exists y(x*y=e)$ — «$x$ обратим справа»). Уменьшим требования — пускай, например, нам теперь нужен $x':I(x)\to x*x'=e\wedge\neg I(x)\to x'=e$. Это должно прокатить и быть $\mathcal M\vdash\exists!y(I(x)\to x*y=e\wedge\neg I(x)\to y=e)$ (в точности вывод не строил, но по смыслу должен быть), так что теория $\mathcal{MI}$ с дополнительной аксиомой $I(x)\to x*x'=e\wedge\neg I(x)\to x'=e$ будет консервативным расширением $\mathcal M$.

Теперь мы можем что-нибудь говорить о формулах, скажем, $I(x)\to x''=x$, которую должно быть можно доказать, и истинной в моделях $\mathcal{MI}$ она будет. (Однако при нашем определении $x'$ в них будет истинной и $x''=x$.) Если в наших формулах со штрихом не будет в нужных местах стоять подформула $I(x)$ (можно для удобства расширить теорию определением соответствующего предикатного символа), можно будет справедливо сомневаться в их осмысленности, если мы хотим понимать $x'$ как ровно обратный элемент (когда он есть), а не, как это записано в определяющей аксиоме, обратный элемент (когда он есть) или $e$ когда его нет.

В текущих условиях можно будет на основании $\vdash A\to\exists!yB$, где $B$ содержит свободные переменные $x_1,\ldots,x_n$ и $A$ содержит какое-то их подмножество, расширить теорию определением нового $n$-арного функционального символа $f$ с опр. аксиомой $\Delta(f(x_1,\ldots,x_n))\to B[f(x_1,\ldots,x_n)/y]$ и ещё одной аксиомой $\Delta(f(x_1,\ldots,x_n))\leftrightarrow A$. Таким образом, аналог $\mathcal{MI}$ должен будет иметь собственные аксиомы

$\begin{array}{ll} 1.1 & (x*y)*z = x*(y*z), \\ 1.2 & \Delta(x*y), \\ 1.3 & \exists a(a*x=x\wedge x*a=x), \\ 2.1 & e*x=x\wedge x*e=x, \\ 2.2 & \Delta(e), \\ 3.1 & \Delta(x')\to x*x'=e, \\ 3.2 & \Delta(x')\leftrightarrow\exists y(x*y=e). \end{array}$

Строго говоря, не совсем такие, но равносильные.

Ох, от этой системы одни убытки — давно бы уже мог уйти спать, если бы не отвечал.

[Xaositect]

Тред на FOM, где обсуждают что-то похожее: https://www.cs.nyu.edu/pipermail/fom/20 ... 19267.html

[arseniiv]

Ой, вот за это огромное спасибо!

-- Ср июл 20, 2016 23:49:58 --

По начальным постам можно решить, что обсуждают как раз то, что интересовало — как можно обращаться с неопределённостью. Жалко, пока со стороны интерпретаций ничего не вычитал. Надеюсь, там ещё много постов и длинных.

[epros]

arseniiv в сообщении #1139050 писал(а):

интересовало — как можно обращаться с неопределённостью

Мне вот что интересно. Какой смысл в построении интерпретаций "с неопределённостью", если интерпретация, имхо, нужна только чтобы удовлетворить тех, кто хочет иметь определённость и полноту (или по крайней мере её видимость) и по этой причине не удовлетворяется одной выводимостью?

[arseniiv]

Я уж точно на этот вопрос не отвечу, потому что тут дело не просто в интерпретациях, а в другом наборе аксиом и правил вывода, если язык вообще остаётся неизменным (мою ерунду можно уже не рассматривать, я увидел кое-что более логичное).

[arseniiv]

Есть что дополнить насчёт вашего вопроса. Такой язык, предполагающий «неопределённые» интерпретации, можно дополнить термами вида $\rotatebox[c]{180}{\iota}x\varphi$, и при этом не вызвать к жизни парадокс Рассела (правила вывода корректируются, как я уже упоминал). Насколько я сейчас в курсе, обычно при добавлении таких термов не в теорию множеств, где можно использовать трюк с объединением, правила построения термов приходится делать разными в зависимости от теории $\mathcal T$. Если $\mathcal T\vdash \exists!x\varphi$, тогда $\rotatebox[c]{180}{\iota}x\varphi$ будет термом, и других термов такого вида нет. По-моему, это неудобное смешение языка и теорий.

-- Сб июл 23, 2016 19:50:37 --

То, что можно ввести $\rotatebox[c]{180}{\iota}x\varphi$ — по-моему, достаточно большая польза. Можно будет больше определений воспринимать как просто синтаксические замены.