Решён
Почему нотация Фреге в логике не прижилась?
Читаю сейчас Begriffsschrift и вот что не дает покоя. Фреге по сути придумал первую формальную систему логики предикатов, изобрел кванторы, связки, импликацию как базовый коннектив. Система мощная, выразительная, исторически первая.
Но его двумерная нотация (эти деревья с вертикальными и горизонтальными линиями) полностью вымерла. Победила линейная запись Пеано-Рассела, потом польская нотация Лукасевича, потом современная стандартная. Никто в XX веке не использовал Begriffsschrift.
Почему? Это чисто типографская проблема (сложно набирать в печати)? Или есть более глубокие когнитивные причины, по которым двумерная запись проигрывает линейной? Ведь деревья вывода мы до сих пор рисуем, секвенциальные исчисления Генцена тоже двумерные. Значит дело не только в плоскости записи.
Про разницу между двумерностью доказательства и двумерностью формулы - отличное наблюдение, спасибо. Не формулировал для себя так четко.