Много скобок

[Sinoid]

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

но кажется, что можно короче и с меньшей длиной формул.

А я и не претендую на красоту решения, наверняка вы, arseniiv, решили бы эту задачу намного красивее, просто мне пришло вот такое решение.

Munin в сообщении #1192349 писал(а):

Есть и ещё один способ записи - "программистский", в виде отступов:
$\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}$

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

Munin в сообщении #1192349 писал(а):

Ну и перестать маяться фигнёй, как вам уже говорили:
$\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}$

У меня один раз в рассуждении было $(A\supset B)$, мне нужно было получить $((B\supset C)\supset((A\supset(B\supset C))\supset(A\supset C)))$ с помощью, как потом выяснилось, аксиомы $((A\supset B)\supset((A\supset(B\supset C))\supset(A\supset C)))$, представляю, какое упрощение решения дала бы мне подстановка
$y::= (B \subset C)$.

Munin в сообщении #1192349 писал(а):

Пронумеруем уровни вложенности:

Встречаются одинаковые циферки, легко можно сбиться.

Sonic86 в сообщении #1192096 писал(а):

Даже неплохая идея,

Да это не моя идея, у Клини почти такое встречалось в доказательстве одной леммы, я и решил воспользоваться.

[Munin]

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

Встречаются одинаковые циферки, легко можно сбиться.

Вы вообще понимаете, что такое уровень вложенности?

А, так это вы начали тему? Я сразу не заметил. Всё, ухожу. Жаль, нельзя моё сообщение из темы стереть.

[arseniiv]

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

А я и не претендую на красоту решения

Да не, я, скорее, об экономии*. Не думаю, что в низкоуровневых выводах можно найти какую-то особую красоту.

Кстати, ещё в старых книжках по логике вместо скобок использовались наборы точечек. Я так и не справился с ними, но при определённой тренировке они должны приниматься не хуже скобок. В отличие от безликих скобок, эти точечки имеются в гораздо большем числе вариаций (счётном, но в любой формуле, конечно, потребуется только конечное число, и обычно довольно малое, по числу уровней или такого же порядка — повторюсь, не помню, что конкретно они обозначают). Не помню, есть ли они в тех книгах Клини, которые вы читали, но вроде должны быть. Может принести пользу, попробуйте.

P. S. * Экономии своих ресурсов, тратящихся на то, чтобы удостоверяться в точности переписываний и подстановок, и вообще на весьма монотонную писанину; это как раз даётся нелегко мозгу человеческому.

[Sinoid]

Спасибо за помощь.