I have diary now. Diaries are cool!
Добрый день. Есть следующее задание:
Если известно, что секвенции `\Gamma \rightarrow\Delta_{1} A\Delta_{2}` и `\Sigma_{1} A\Sigma_{2}\rightarrow\Pi` — аксиомы, доказать, что выводима секвенция
`\Gamma\Sigma_{1}\Sigma_{2}\rightarrow\Delta_{1}\Delta_{2}\Pi`. (`\Gamma, \Delta_{1}, \Delta_{2}, \Sigma_{1}, \Sigma_{2}, \Pi` — списки формул, A — пропозициональная переменная)
Что у меня уже получилось сделать:
1 случай: Пусть B — формула, входящая в `\Gamma` и секвенция `\Gamma\rightarrow\Delta_{1} A\Delta_{2}` является аксиомой "из-за" B. Тогда если B входит в `\Gamma`, то B входит либо в `\Delta_{1}`, либо в `\Delta_{2}`, тогда интересующая нас секвенция `\Gamma\Sigma_{1}\Sigma_{2}\rightarrow\Delta_{1}\Delta_{2}\Pi` выводима. При этом секвенция `\Sigma_{1} A\Sigma{2}\rightarrow\Pi` может являться аксиомой как "из-за" A, так и "из-за" другой переменной, входящей либо в `\Sigma_{1}`, либо в `\Sigma_{2}`
2 случай: Аналогично 1-му случаю, только теперь известно, что вторая секвенция является аксиомой не "из-за" A.
Что у меня сделать не получается: Доказать выводимость `\Gamma\Sigma_{1}\Sigma_{2}\rightarrow\Delta_{1}\Delta_{2}\Pi`, если обе исходные секвенции являются аксиомами "из-за" A. Не знаю даже, с какой стороны подойти.
Заранее спасибо за помощь!
Если известно, что секвенции `\Gamma \rightarrow\Delta_{1} A\Delta_{2}` и `\Sigma_{1} A\Sigma_{2}\rightarrow\Pi` — аксиомы, доказать, что выводима секвенция
`\Gamma\Sigma_{1}\Sigma_{2}\rightarrow\Delta_{1}\Delta_{2}\Pi`. (`\Gamma, \Delta_{1}, \Delta_{2}, \Sigma_{1}, \Sigma_{2}, \Pi` — списки формул, A — пропозициональная переменная)
Что у меня уже получилось сделать:
1 случай: Пусть B — формула, входящая в `\Gamma` и секвенция `\Gamma\rightarrow\Delta_{1} A\Delta_{2}` является аксиомой "из-за" B. Тогда если B входит в `\Gamma`, то B входит либо в `\Delta_{1}`, либо в `\Delta_{2}`, тогда интересующая нас секвенция `\Gamma\Sigma_{1}\Sigma_{2}\rightarrow\Delta_{1}\Delta_{2}\Pi` выводима. При этом секвенция `\Sigma_{1} A\Sigma{2}\rightarrow\Pi` может являться аксиомой как "из-за" A, так и "из-за" другой переменной, входящей либо в `\Sigma_{1}`, либо в `\Sigma_{2}`
2 случай: Аналогично 1-му случаю, только теперь известно, что вторая секвенция является аксиомой не "из-за" A.
Что у меня сделать не получается: Доказать выводимость `\Gamma\Sigma_{1}\Sigma_{2}\rightarrow\Delta_{1}\Delta_{2}\Pi`, если обе исходные секвенции являются аксиомами "из-за" A. Не знаю даже, с какой стороны подойти.
Заранее спасибо за помощь!