структуры с пустым носителем в теории моделей

[beroal]

В большинстве учебников по локиге структуры с пустым носителем не рассматриваются. Насколько я понимаю, причина в том, что определение оценки (функции, задающей значения свободных индивидных переменных формулы) там выглядит так: оценка есть функция из множества всех индивидных переменных в носитель структуры. А множество всех индивидных переменных бесконечно и счётно. Если носитель структуры пустой, то никаких оценок не существует, и все формулы истинны в этой структуре. Но $\exists x(\top)$, по идее, должна быть ложна в такой структуре. Чтобы исправить это, нужно дать следующее определение оценки: оценка есть функция из некоторого множества индивидных переменных в носитель структуры. Но тогда истинность формулы при оценке, область определения которой не содержит какую-то свободную индивидную переменную этой формулы, по идее, должна быть неопределённой. Есть ли книги по логике, где рассматриваются структуры с пустым носителем? Такой подход мне кажется более правильным. Я хочу понять, как это изменит теорию.

[george66]

Зачем сюда помещаете, я сюда редко хожу. На пустой модели все формулы вида $\exists x\varphi(x)$ ложны, а все формулы вида $\forall x\varphi(x)$ истинны. Соответственно, не все формулы, выводимые в обычной логике, верны на пустой модели. Например, формула вида
$\forall x\varphi(x)\Rightarrow\exists x\varphi(x)$
ложна, хотя выводима в обычной логике. Логику можно немного ослабить, получается так называемая "свободная логика" (не берусь сказать, от чего свободная), есть много её вариантов. Один вариант - к каждой формуле приписывать "контекст" из объявлений типов переменных. Например, в обычной логике мы можем вывести формулу $\exists x (x=x)$, начав с формулы $x=x$ и навесив квантор. В свободной логике мы начинаем с такой "секвенции" $x:T\vdash x=x$ (где $T$ какой-нибудь тип) и навесить квантор можем только так $x:T \vdash \exists x:T (x=x)$ ("если элемент икс принадлежит типу $T$, то $\exists x:T (x=x)$, что правда даже для пустого $T$) На эту тему надо читать по теории типов, например "Type Theory and Formal Proof", Nederpelt & Geuvers, 2014
http://gen.lib.rus.ec/search.php?req=Ty ... column=def
Есть также совсем другой подход, где к каждому множеству формально добавляется "неопределённый элемент", а к исчислению предикатов добавляется предикат "определено". Он подробно изложен в книге Constructivism in mathematics
http://gen.lib.rus.ec/search.php?req=co ... column=def

[arseniiv]

Ещё предикат определённости $\exists!y$ может быть выразим в некоторых из них как $\exists x.\;x = y$, и неопределённых элементов можно и не добавлять. И совсем уж недавно я, пытаясь навести порядок в голове и читая стэнфордскую энциклопедию по поводу свободной логики (вот она, и не смотрите, что Encyclopedia of Philosophy, несколько статей, касающихся логики, которые я видел, там весьма хороши) и модальной логики первого порядка, наткнулся на язык с внутренними (нашими обычными) и внешними кванторами, вот это, конечно, вообще хитро. У всех вариантов свободных логик, которые там упоминались, есть проблемы, которые там же упоминались тоже, и если раньше я смотрел на неё с надеждой, теперь не знаю как смотреть. Логика беспросветна. (потому что у несвободной-то тоже есть проблемы).

-- Пт авг 23, 2019 02:06:37 --

Ещё часто свободные логики допускают незначащие термы, и можно например вводить конструкции типа $\rotatebox[c]{180}{\(\iota\)}x.\varphi$ «единственный $x$ такой, что $\varphi$» или $\varepsilon x.\varphi$ «некоторый $x$ такой, что $\varphi$» (насколько правильно помню).