Логическое следование с несколькими заключениями

[kernel1983]

Известно, что в логике высказываний есть такая конструкция, как логическое следование формул с несколькими посылками.

Пусть $F_1,F_2,\ldots, F_k,G$ - формулы, которые зависят от пропозициональных переменных $P_1,P_2, \ldots, P_n$.

Определение 1. Будем говорить, что формула $G$ логически следует из формул $F_1,F_2, \ldots, F_k$, если для любых высказываний $A_1,A_2, \ldots, A_n$ если высказывания $F_1(A_1,A_2, \ldots, A_n), F_2(A_1,A_2, \ldots, A_n) , \ldots, F_k(A_1,A_2, \ldots, A_n)$ истинны, то истинно и высказывание $G(A_1,A_2, \ldots, A_n)$.

Определение 2. Будем говорить, что формула $G$ логически не следует из формул $F_1,F_2, \ldots, F_k$, если существуют такие высказывания $A_1,A_2, \ldots, A_n$, что высказывания $F_1(A_1,A_2, \ldots, A_n), F_2(A_1,A_2, \ldots, A_n) , \ldots, F_k(A_1,A_2, \ldots, A_n)$ истинны, а высказывание $G(A_1,A_2, \ldots, A_n)$ ложно.

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

Пусть $F, G_1, G_2, \ldots, G_m$ - формулы, которые зависят от пропозициональных переменных $P_1,P_2, \ldots, P_n$.

Определение 3. Будем говорить, что формулы $G_1,G_2, \ldots, G_m$ логически следуют из формулы $F$, если для любых высказываний $A_1,A_2, \ldots, A_n$ если высказывание $F(A_1,A_2, \ldots, A_n)$ истинно, то истинно хотя бы одно из высказываний $G_1(A_1,A_2, \ldots, A_n), G_2(A_1,A_2, \ldots, A_n), \ldots, G_m(A_1,A_2, \ldots, A_n)$.

Определение 4. Будем говорить, что формулы $G_1,G_2, \ldots, G_m$ логически не следуют из формулы $F$, если существуют такие высказывания $A_1,A_2, \ldots, A_n$, что высказывание $F(A_1,A_2, \ldots, A_n)$ истинно, а высказывания $G_1(A_1,A_2, \ldots, A_n), G_2(A_1,A_2, \ldots, A_n), \ldots, G_m(A_1,A_2, \ldots, A_n)$ ложны.

Понятно, что в определениях 1 и 2 есть здравый смысл (из нескольких формул следует или не следует одна формула). Есть ли какой-то смысл в определениях 3 и 4? Там из одной формулы следуют или не следуют несколько формул.

[arseniiv]

Исчисление секвенций (sequent calculus) оперирует как раз подобными штуками вида $\mathcal F \vdash \mathcal G$, выводя их друг из друга, где $\mathcal F, \mathcal G$ — конечные последовательности формул, с семантикой как у вас, то есть для классического исчисления мы имеем «$\mathcal F \vdash \mathcal G$ выводится ровно тогда, когда $\vdash (\bigwedge \mathcal F)\to(\bigvee \mathcal G)$ и также ровно тогда, когда $(\bigvee \mathcal F)\wedge\neg(\bigvee \mathcal G)\vdash$» (в первой слева от $\vdash$ пустое множество формул и справа одна комбинированная, во второй наоборот), а для интуиционистского прям так не выйдет, но семантика подобная.

-- Сб фев 20, 2021 02:25:46 --

Но вне таких симметричных исчислений (как пример ещё можно линейную логику взять, а больше я примеров и не знаю) я смысла бы в таком понятии следования одновременно нескольких формул не видел, оно точно часто будет путаться с обычным пониманием «для всех $G \in \mathcal G$ верно $\mathcal F \vDash G$».