Как логически записать, что можно и то и то?

[epros]

Dims писал(а):

Ну да, можно, конечно. Но смысл получается не тот, что мне хочется.

Я так и не понял, какой именно смысл Вы хотите получить? Разрешительную модальность можно применить к любому высказыванию, т.е. к любой логической комбинации, которая только придёт Вам в голову. Аналогично - с запретительной модальностью.

Можно(снять левый ботинок и снять правый ботинок) - это как раз та разрешительная формула, которая позволяет одновременные действия. Естествено, она ничего не запрещает, в том числе - не запрещает снимать по одному ботинку. Чтобы что-то запретить, нужна запретительная модальность: Нельзя(снять левый ботинок и не снять правый ботинок или не снять левый ботинок и снять правый ботинок) - то, что Вам записал PAV. Но это вопрос, совершенно отдельный от разрешительной модальности (исключая тот факт, что запрещение определяется через отрицание разрешения).

[Dims]

Хорошо, переформулируем задачу.

У меня есть некая структура, типа графа. Вершины графа -- это нечто, вроде возможных состояний системы. Особенность в том, что система может находиться сразу в нескольких из этих состояний.

Вершины соединены стрелочками -- это возможные переходы между состояниями. То есть, в частном случае у нас может быть просто ориентированный граф. Но в общем случае есть особенность: должна быть возможность отображения правил, которые требуют одновременного выполнения сразу нескольких переходов и не требующие при этом допустимости отдельных переходов.

То есть, некоторые стрелочки, говоря квантовомеханическим языком, запутаны между собой. Пусть на картинке такие срелочки соединены между собой зелёными линиями.

Вот как мне вот это всё записать на языке предикатов?

Если бы у меня просто был ориентированный граф, то я бы сделал просто один предикат "переход" с двумя параметрами. Его параметрами и одновременно атомами служили бы вершины графа. Если такой предикат был бы истинен, то это значило бы, что между соответствующими вершинами есть стрелочка. Если ложен -- то нет.

Поскольку эта задача является частным случаем по отношению к моей, то я хочу, чтобы предикат "переход" был и в последней. Но при этом его как-то надо обобщить на случай наличия запутанных стрелочек.

Можно было бы сделать, чтобы предикат "переход" имел бы произвольное чётное количество аргументов, и чтобы кажда пара означала один такой спутанный с другими переход, но это не отражало бы родства между предикатом с одной парой и предикатом с несколькими парами.

Фактически, используя лямбда-исчисление, мой вопрос заключается в вопросе, что из себя представляет

лямбда: (замена(а,б) , замена(в,г)) . замена(а,б,в,г)

[luitzen]

На всякий случай выложил что-то по модальной логике тут:
Фейс
Handbook of philosophical logic, vol. 2
Chagrov & Zakharyaschev
Advances in modal logic, vol. 3

Dims писал(а):

Я так понял, что модальности действуют на формулы как бы символически, не вычисляя их значения?

Имеются различные модальные исчисления со своими аксиомами и правилами вывода. Но к ним, как правило, предлагаются и некие модели, такие, что формула является выводимой в исчислении тогда и только тогда, когда она в некотором смысле общезначима в соответствующей модели.
Модальности вполне «вычисляют» значения формул, только на калькуляторе это реализовать сложно.
К примеру, «значением» $p$ может быть некое $A\subseteq\mathbb{R}$, тогда значением $\lozenge p$ («возможно, что $p$») будет (ещё раз к примеру) замыкание этого $A$.

Dims писал(а):

Вершины соединены стрелочками -- это возможные переходы между состояниями…

Это мне напомнило семантику возможных миров с её отношением достижимости

ОК, пусть «стрелочка» — (одноместный) предикат на множестве $M$ упорядоченных пар состояний. Тогда «переход» — предикат на множестве подмножеств этого $M$. Только вот «стрелочка» и «переход» будут объектами разных «типов», и придётся различать $Str(\langle a,b \rangle)$ и $Per(\{\langle a,b\rangle\})$. Это Вам подойдёт, Dims?

[epros]

Dims писал(а):

Если такой предикат был бы истинен, то это значило бы, что между соответствующими вершинами есть стрелочка. Если ложен -- то нет.

Поскольку эта задача является частным случаем по отношению к моей, то я хочу, чтобы предикат "переход" был и в последней. Но при этом его как-то надо обобщить на случай наличия запутанных стрелочек.

Ну, если Вы хотите выразить это именно предикатом, то luitzen Вам правильно указал, что это соответствует переходу от множества "стрелочек" к множеству подмножеств множества "стрелочек". Я хочу только добавить, что модальности фактически вводятся именно для того, чтобы этого не делать.

Смотрите, если у Вас, например, всего имеется $N$ "стрелочек" (т.е. вариантов действия, таких как "Вася снимает левый ботинок" или "Петя снимает правый ботинок", или любого другого типа), то предикат, который некоторые из этих стрелочек разрешает, а остальные - запрещает, является логической функцией на множестве "стрелочек". Таких функций может быть всего $2^N$ штук. А модальный оператор, как я говорил ранее, является функционалом, заданным на множестве предикатов. Т.е. Вы можете трактовать модальный оператор, разрешающий определённые наборы "стрелочек" и не разрешающий (но и не запрещающий) другие наборы "стрелочек", как логическую функцию, заданную на множестве предикатов (= на множестве разрешённых наборов стрелочек), - разрешены именно те наборы "стрелочек", соответствующие которым предикаты, будучи подставленными в качестве аргумента $X$ данной логической функции можно$(X)$, дадут значение "истина".

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

[Dims]

luitzen писал(а):

Только вот «стрелочка» и «переход» будут объектами разных «типов», и придётся различать $Str(\langle a,b \rangle)$ и $Per(\{\langle a,b\rangle\})$. Это Вам подойдёт, Dims?

Да, тогда не этом языке: что из себя представляет функция

$Per(\{\langle a,b\rangle\}) , Per(\{\langle c,d\rangle\}) \Rightarrow Per(\{\langle a,b\rangle ,\langle c,d\rangle\})$

?

[Dims]

luitzen писал(а):

Это мне напомнило семантику возможных миров с её отношением достижимости

А что это такое? Откуда это?