Много скобок

[Sinoid]

Здравствуйте! Занимался выводом одной формулы в ИВ. Получил столько скобок, аж вывалился язык. Решил соответственные пары скобок нумеровать. Получил вот что:
$\begin{gathered}(_{27}(_{7}(_{3}(_{1}A\wedge C)_{1}\supset(_{2}B\wedge C)_{2})_{3}\supset(_{6}(_{4}A\wedge C)_{4}\supset(_{5}B\wedge C)_{5})_{6})_{7}\supset\\ (_{26}(_{14}(_{10}(_{8}A\wedge C)_{8}\supset(_{9}B\wedge C)_{9})_{10}\supset(_{13}(_{11}B\wedge C)_{11}\supset(_{12}A\wedge C)_{12})_{13})_{14}\supset(_{25}(_{17}(_{15}A\wedge C)_{15}\supset(_{16}B\wedge C)_{16})_{17}\supset\\ (_{24}(_{20}(_{18}A\wedge C)_{18}\supset(_{19}B\wedge C)_{19})_{20}\wedge(_{23}(_{21}B\wedge C)_{21}\supset(_{22}A\wedge C)_{22})_{23})_{24})_{25})_{26})_{27} \end{gathered} $
А вот, например, если на такое выражение наткнешься в контрольной или вот в книге такая запись допустима или нет? Я понимаю, что в данном случае использование скобок разных видов значительно облегчит восприятие формулы, но ведь скобок может быть больше.

[Dmitriy40]

Наверное удобнее было не нумеровать все скобки подряд, а нумеровать уровни вложенности. Тогда скобки 21 и 22 к примеру получат одинаковый номер и т.д. И уже для каждого уровня вложенности можно использовать свой вид скобок. Здесь вижу 6 уровней вложенности. Самые внутренние можно оставить как есть, а самые внешние сделать увеличенного размера, тогда хватит всего 3-х видов скобок (или даже двух если использовать три разных размера).

-- 12.02.2017, 20:48 --

(Если допустимо упростить выражение)

Ещё полезна замена переменных, у вас во всех внутренних скобках всего два варианта выражений, или $A \wedge C$ или $B \wedge C$, переобозначив их двумя новыми переменными $x, y$ снимется один уровень скобок. Если не ошибаюсь можно точно так же снять и ещё один внутренний уровень, там всего два типа выражений, или $x \supset y$ или $y \supset x$.

-- 12.02.2017, 20:58 --

(Оффтоп)

Кстати, а выражение $(a\supset a)$ разве не упрощается? Оно идёт самым первым в вашей формуле.

[Sonic86]

Sinoid в сообщении #1192034 писал(а):

А вот, например, если на такое выражение наткнешься в контрольной или вот в книге такая запись допустима или нет?

Просто дайте ее определение и она станет допустимой. Даже неплохая идея, не красить же их в разные цвета и не придавать им разную форму.
А вообще, на самом деле, формулы - это деревья, скобки - это такая техническая конструкция, позволяющая осуществить преобразование строки обратно в дерево. Попробуйте деревья - проблема исчезнет

[arseniiv]

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

Dmitriy40 в сообщении #1192078 писал(а):

Кстати, а выражение $(a\supset a)$ разве не упрощается?

Пока не доказана определённая теорема, заменять эквивалентные подформулы друг на друга в выводе нельзя.

Хотя то ли я недостаточно много руками выводил, то ли как-то эта формула большевата. Как она появилась?

[Sonic86]

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

Dmitriy40 в сообщении #1192078 писал(а):

Кстати, а выражение $(a\supset a)$ разве не упрощается?

Пока не доказана определённая теорема, заменять эквивалентные подформулы друг на друга в выводе нельзя.

Угу, причем метатеорема. В ИВ, например, если $x\vdash y$, то отсюда нифига не следует, что $F(x)\vdash F(y)$

[Sinoid]

Dmitriy40 в сообщении #1192078 писал(а):

Ещё полезна замена переменных

Не всегда удобно. Когда строишь формулу с прицелом на предстоящие выводы частей формулы, замена затрудняет ход мысли. Ладно, допишу потом: началась сварка.

[Sinoid]

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

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

Во-первых, люди могут быть дальтоники. Во-вторых, это лишний код в формуле.

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

Хотя то ли я недостаточно много руками выводил, то ли как-то эта формула большевата. Как она появилась?

Вам выложить весь вывод?

[arseniiv]

Не, весь не нужно — просто что из чего выводилось.

[Sinoid]

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

Не, весь не нужно — просто что из чего выводилось.

Я ее не выводил, это схема аксиом $((P\supset Q)\supset((P\supset R)\supset(P\supset(Q\wedge R))))$

[Dmitriy40]

Sinoid в сообщении #1192280 писал(а):

Я ее не выводил, это схема аксиом $((P\supset Q)\supset((P\supset R)\supset(P\supset(Q\wedge R))))$

По моему у Вас где-то ошибка, это выражение не совпадает с $((P \supset P) \supset ((P \supset R) \supset (P \supset (P \wedge R))))$, к которому упрощается изначальное заменами переменных.

[arseniiv]

Sinoid в сообщении #1192280 писал(а):

Я ее не выводил

Я про то, в выводе чего из чего она встречается.

[Sinoid]

Dmitriy40 в сообщении #1192290 писал(а):

Sinoid в сообщении #1192280

писал(а):
Я ее не выводил, это схема аксиом $((P\supset Q)\supset((P\supset R)\supset(P\supset(Q\wedge R))))$ По моему у Вас где-то ошибка, это выражение не совпадает с $((P \supset P) \supset ((P \supset R) \supset (P \supset (P \wedge R))))$, к которому упрощается изначальное заменами переменных.

$Q=P$

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

Я про то, в выводе чего из чего она встречается.

Там связка $A \equiv B$ определяется как $((A\supset B)\wedge(B\supset A))$. Надо было построить вывод $(A\equiv B)\vdash((A\wedge C)\equiv(B\wedge C))$. Ну я и построил из 44 пунктов. Правда, конъюнкцию нужных множителей я вывел в самой задаче. Ну, допустим, тут можно было вспомогательной леммой обойтись. Но вот сейчас я строю вывод $(A\equiv B)\vdash((C\supset A)\equiv(C\supset B))$ (подсказывать, как решить эту задачу пока не нужно: мне кажется, я ее одолею) и для ее решения я пришел к выводу, что мне нужно вывести формулу $((A\supset B)\supset((B\supset C)\supset(A\supset C)))$, которая сама по себе представляет интерес, доказываю, как в доказательстве теоремы о дедукции (чтоб вслепую не блуждать), так опять в скобках утонул.

[Dmitriy40]

(Оффтоп)

Sinoid в сообщении #1192313 писал(а):

$Q=P$

Да, это я стормозил, прошу прощения.

[Munin]

Пронумеруем уровни вложенности:
$\begin{gathered}(_{6}(_{3}(_{2}(_{1}A\wedge C)_{1}\supset(_{1}B\wedge C)_{1})_{2}\supset(_{2}(_{1}A\wedge C)_{1}\supset(_{1}B\wedge C)_{1})_{2})_{3}\supset \\ (_{5}(_{3}(_{2}(_{1}A\wedge C)_{1}\supset(_{1}B\wedge C)_{1})_{2}\supset(_{2}(_{1}B\wedge C)_{1}\supset(_{1}A\wedge C)_{1})_{2})_{3}\supset \\ (_{4}(_{2}(_{1}A\wedge C)_{1}\supset(_{1}B\wedge C)_{1})_{2}\supset(_{3}(_{2}(_{1}A\wedge C)_{1}\supset(_{1}B\wedge C)_{1})_{2}\wedge(_{2}(_{1}B\wedge C)_{1}\supset(_{1}A\wedge C)_{1})_{2})_{3})_{4})_{5})_{6}\end{gathered}$

Расставим скобки разных типов:
$\begin{gathered}\biggl\{\,\,\bigl\{[(A\wedge C)\supset(B\wedge C)]\supset[(A\wedge C)\supset(B\wedge C)]\bigr\}\supset \\ \,\,\Bigl[\bigl\{[(A\wedge C)\supset(B\wedge C)]\supset[(B\wedge C)\supset(A\wedge C)]\bigr\}\supset \\ \Bigl([(A\wedge C)\supset(B\wedge C)]\supset\bigl\{[(A\wedge C)\supset(B\wedge C)]\wedge[(B\wedge C)\supset(A\wedge C)]\bigr\}\Bigr)\Bigr]\biggr\}\end{gathered}$

Есть и ещё один способ записи - "программистский", в виде отступов:
$\begin{aligned} &\biggl\{ \\ &\quad\bigl\{ \\ &\quad\quad[(A\wedge C)\supset(B\wedge C)] \\ &\quad\quad\quad\supset \\ &\quad\quad[(A\wedge C)\supset(B\wedge C)] \\ &\quad\bigr\} \\ &\quad\quad\supset \\ &\quad\Bigl[ \\ &\quad\quad\bigl\{ \\ &\quad\quad\quad[(A\wedge C)\supset(B\wedge C)] \\ &\quad\quad\quad\quad\supset \\ &\quad\quad\quad[(B\wedge C)\supset(A\wedge C)] \\ &\quad\quad\bigr\} \\ &\quad\quad\quad\supset \\ &\quad\quad\Bigl( \\ &\quad\quad\quad[(A\wedge C)\supset(B\wedge C)] \\ &\quad\quad\quad\quad\supset \\ &\quad\quad\quad\bigl\{ \\ &\quad\quad\quad\quad[(A\wedge C)\supset(B\wedge C)] \\ &\quad\quad\quad\quad\quad\wedge \\ &\quad\quad\quad\quad[(B\wedge C)\supset(A\wedge C)] \\ &\quad\quad\quad\bigr\} \\ &\quad\quad\Bigr) \\ &\quad\Bigr] \\ &\biggr\} \end{aligned}$

или более компактно:
$\begin{aligned} &\smash[b]{\biggl\{}\bigl\{\,\,[(A\wedge C)\supset(B\wedge C)] \\ &\quad\quad\,\,\supset \\ &\quad\hphantom{\bigl\{\,\,}[(A\wedge C)\supset(B\wedge C)]\,\,\bigr\} \\ &\quad\supset \\ &\quad\smash[b]{\Bigl[}\,\,\bigl\{\,\,[(A\wedge C)\supset(B\wedge C)] \\ &\quad\quad\quad\,\,\supset \\ &\quad\quad\hphantom{\bigl\{\,\,}[(B\wedge C)\supset(A\wedge C)]\,\,\bigr\} \\ &\quad\quad\supset \\ &\quad\quad\smash[b]{\Bigl(}\,\,[(A\wedge C)\supset(B\wedge C)] \\ &\quad\quad\quad\supset \\ &\quad\quad\quad\bigl\{\,\,[(A\wedge C)\supset(B\wedge C)] \\ &\quad\quad\quad\quad\,\,\,\wedge \\ &\quad\quad\quad\hphantom{\bigl\{\,\,}[(B\wedge C)\supset(A\wedge C)]\,\,\bigr\}\,\,\smash[t]{\Bigr)\,\,\Bigr]\,\,\biggr\}} \end{aligned}$

Ну и перестать маяться фигнёй, как вам уже говорили:
$\begin{aligned} & x ::= A \wedge C \\ & y ::= B \wedge C \\ & f ::= x \supset y \\ & g ::= y \supset x \\ & (f\supset f)\supset\bigl\{(f\supset g)\supset[f\supset(f\wedge g)]\bigr\} \end{aligned}$

[arseniiv]

Sinoid в сообщении #1192313 писал(а):

Там связка $A \equiv B$ определяется как $((A\supset B)\wedge(B\supset A))$. Надо было построить вывод $(A\equiv B)\vdash((A\wedge C)\equiv(B\wedge C))$. Ну я и построил из 44 пунктов. Правда, конъюнкцию нужных множителей я вывел в самой задаче. Ну, допустим, тут можно было вспомогательной леммой обойтись. Но вот сейчас я строю вывод $(A\equiv B)\vdash((C\supset A)\equiv(C\supset B))$ (подсказывать, как решить эту задачу пока не нужно: мне кажется, я ее одолею) и для ее решения я пришел к выводу, что мне нужно вывести формулу $((A\supset B)\supset((B\supset C)\supset(A\supset C)))$, которая сама по себе представляет интерес, доказываю, как в доказательстве теоремы о дедукции (чтоб вслепую не блуждать), так опять в скобках утонул.

Хм, мне пока немного лень самому строить выводы, но кажется, что можно короче и с меньшей длиной формул. Только кажется, ваши выводы могут быть и минимальными, но кажется.