Посоветуйте книгу по матлогике/основаниям

[arseniiv]

Про типы можно пояснить на том же примере натуральных чисел. Будем рассматривать выражения из них с плюсами и умножениями, тогда всё это можно задать как-нибудь покороче так:

Индуктивный тип $\mathbb N$:

• $0 : \mathbb N$,
• $S : \mathbb N\to\mathbb N$.

Индуктивный тип $A$:

• $\langle\text{без явного обозначения}\rangle : \mathbb N\to A$,
• ${+} : A\times A\to A$,
• ${\times} : A\times A\to A$.

В местах, где используют абстрактный синтаксис, это бы описали более человечно, каждый тип обозначив набором переменных, которые будут иметь такой тип ниже в тексте, и используя эти переменные в примерах выражений в определении других типов (или того же), и справа будет ещё удобно комментировать неформальный смысл обозначений — как-то так:

$\begin{array}{lclr} m, n, k & ::= & &\qquad\textit{натуральные числа:} \\ & & 0 &\qquad\textit{ноль} \\ & \mid & Sn &\qquad\textit{следующее за }n\textit{ число} \end{array}

$\begin{array}{lclr} a, b & ::= & &\qquad\textit{выражения:} \\ & & n &\qquad\textit{число} \\ & \mid & a + b &\qquad\textit{сумма} \\ & \mid & a\times b &\qquad\textit{произведение} \\ \end{array}$

и в дальнейшем тексте, как и прям в этих определениях, $m, n, k$ (а также, к примеру, некие $m_1,m_2, n', k^*$) будут обозначать натуральные числа и $a, b$ будут обозначать арифметические выражения. Тут плюс, что мы определяем сам синтаксис, которым будем пользоваться, говоря про вещи, потому что первое определение даёт нам само по себе никакого языка нам не даёт.

Мы сможем говорить, что $0 + (SSS0\times SS0)$ — выражение, а если примем соглашения о приоритете, можем некоторые скобки опускать. Абстрактность синтаксиса означает, что нам нет дела о вопросах корректности записей типа ${\times}{\times}0{\times}S){+}()(($ — мы уже должны воспринимать их как не означающие никакое выражение; мы говорим о выражениях, а их запись — дело десятое, и если мы например записали какое-то выражение двусмысленно или там у нас мигрень и мы не можем читать, это не интересует теорию о выражениях.

-- Пт окт 04, 2019 01:15:57 --

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

Между прочим, это довольно глубокий вопрос, от которого не стоит так отмахиваться. Именно на расположении деревьев в виде строк основано фундаментальнейшее свойство алгебры - ассоциативность.

Тут недавно в одной теме beroal писал насчёт этого. Коротко, раз дерево упорядоченное, мы можем собрать его листья в одном из естественных порядков и получить строку. Тут важно, что нам плевать на всякие скобочки и прочую презентацию, на которые традиционное рассмотрение формул как строк внимание обращает, потому что им ведь пользоваться надо, так что ассоциативность зиждется совсем не на тех строках, которые подвергаются сомнению.

Ссылку щас найду и вставлю.

-- Пт окт 04, 2019 01:17:14 --

post1412572.html#p1412572

-- Пт окт 04, 2019 01:19:05 --

Кстати ровно тот же самый beroal недавно показывал свой список книг по логике, уже в другом месте. Он тут тоже бы пригодился(?) Вообще его надо куда-нибудь сохранить, не у всех есть свой список (у меня нету, я не очень организован на этот счёт).

[Munin]

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

Коротко, раз дерево упорядоченное, мы можем собрать его листья в одном из естественных порядков и получить строку.

В этом действии нет ничего от той "строчности", в которой мы обычно пишем математические выражения. И которую обсуждаемо можно попробовать заменить на двумерность или что-то ещё.

Ну, если вас это не заинтересовало, я умолкаю.

[arseniiv]

Munin
Нет, почему не заинтересовало? (Хотя смотря что.) (Но тут это чуть оффтоп в любом случае.)

-- Пт окт 04, 2019 01:45:05 --

(Оффтоп)

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

(Например, взять алгебраическую операцию $f(x,y,z),$ и расположив аргументы треугольником, попробовать для неё придумать содержательный аналог ассоциативности.)

Кстати если вы видели упоминания груд (heaps), там операция тернарная, но для её смысла ассоциативность получается специфической: $f(f(x, y, z), t, w) = f(x, y, f(z, t, w))$, всё из-за того, что крайние аргументы там «с плюсом», а средний «с минусом», и аналог коммутативности там даёт нам в списке переставлять нечётные элементы друг с другом и отдельно чётные друг с другом, но не смешивая те и те.

[Munin]

Тернарные операции в строчку - это всё равно в строчку :-) Там придумать чего-то осмысленное намного проще.

-- 04.10.2019 00:06:00 --

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

[arseniiv]

Надеюсь, это не столь ограничительно, всё же в большей части наших обозначений линейность особо не важна.

[Munin]

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

всё же в большей части наших обозначений линейность особо не важна.

У меня обратное впечатление: что она настолько повсеместна, что мы этого не замечаем, как рыбы воды́.

[epros]

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

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

Это вряд ли. Скорее из-за нашей человеческой неспособности вырваться за пределы алгоритмов (тезис Чёрча). А алгоритмы формализуются не только строками.

[arseniiv]

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

[george66]

Вот два архива, где собраны все или почти все книги по матлогике, изданные в советское время
http://www.mediafire.com/download/cn7hs ... o/djvu.rar
http://www.mediafire.com/download/4g54u ... u8/pdf.rar
Собиралось давно, сейчас многое есть в лучшем качестве на libgen
http://gen.lib.rus.ec/