Меня натуральные числа по фон Нейману или по Цермело относительно устраивают. Не устраивают лишь определения в духе "мы все знаем эти числа, мы их используем для счета" и все такое.
А, ну тогда вот вам определение: натуральное число — это запись, которую можно получить лишь одним из двух следующих способов: (i) взять запись
, (ii) взять натуральное число и приписать слева
. После этого мы можем определить равенство (в данном случае просто как совпадение записей) и прочие вещи типа сложения. Наше определение натурального числа —
индуктивное, так что мы можем использовать индукцию для доказательств и рекурсию для определений.
Для этого не обязательно читать матлогику, а для установления нижней планки, как уже писал
epros, матлогики будет недостаточно — мы должны будем точно так же договориться о том, где у нас дно, используя и матлогику. В конечном счёте она сама полноценный раздел математики.
А вот это интересно. Где можно почитать матлогику с т.з. деревьев?
Точно не знаю, но пара книжек может существовать, потому что этому сто лет в обед. Везде, где упоминается абстрактный синтаксис (abstract syntax), речь должна быть о деревьях, но я видел это в основном в книжках и статьях, касающихся языков программирования и теории типов. Они, разумеется, и не на ту тему, что вам нужна, и подразумевают какую-то немаленькую и специфическую базу, так что не подходят.
Идея тут настолько же проста, что выше: мы индуктивно определяем интересующие выражения, но с большим числом
альтернатив и возможных способов вхождения подвыражений, и удобно думать о них как о деревьях с
типами вершин, у каждой из которых какое-то конечное число поддеревьев, зависящее лишь от типа вершины, и поддеревья идут в некотором порядке, так что можно говорить о первом, втором и т. д.. Такие «хорошие» деревья легко выделяются из всех упорядоченных деревьев с
типами вершин, которые сами довольно ясно определены, не противны наивным взглядам и не несут противоречий при формализации. Для более реальных по сложности выражений деревья и требования к поддеревьям вершин могут быть ограничены
типами из некоторого обозримого множества, так что виды вершин получают типы
, где
— требуемые типы поддеревьев вершины, а
— тип дерева, которое получается с такой вершиной в корне. (Возможны и другие усложнения.)
А я даже не знаю толком, что такое символ
Символ, который реально написан на бумаге? Или "абстрактный" символ? А может и то и другое? Можно так: "абстрактный" символ - это "класс" "похожих" символов (одной формы)? (И что такое тогда "класс"?)
Как уже написали, тут можно падать бесконечно, так что стоит предъявить к таким понятиям другие требования: во-первых, не очень формальные, потому что при формализации мы провалимся на уровень ниже; во-вторых, операционные: что мы должны уметь делать с этими вещами. Для символов мы должны уметь проверять их равенство, во-первых всегда результативно (не зависать для каких-то пар символов), и во-вторых желательно побыстрее (это более неформальное требование). Кроме того мы должны уметь перечислить все символы и так же, если мы рассматриваем что-то кроме них, уметь (результативно) определить, символ перед нами или что-то ещё.
Это всё. Считать ли буквы разного цвета разными или одинаковыми, определяется уже уровнем рассмотрения, который — пока мы биологические существа вида Homo sapiens — можно задать только неформально в процессе коммуникации с другими сторонами, с которыми мы хотим взаимопонимания.
С именами вообще беда. Есть ли "взаимно однозначное соответствие" между именами и их "смыслами"? А между именами и их "объектами"? А между "смыслами" и "объектами"?
В общем случае значение имени зависит от контекста и действительно может быть не единственным и не существовать. Последние два часто можно «вынести за скобки», но зависимость от контекста обычно полезна. Например, что такое 2? Для довольно большого числа случаев можно сказать, что
определяется как
, где
и
— это единица и сложение
рассматриваемого полукольца. Таким образом мы можем говорить о натуральном числе 2, целом числе 2, комплексном числе 2 и даже о том, что
в поле характеристики 2 или булевом кольце.
Как быть, когда имя само является объектом?
Обычно когда об этом надо говорить, есть (как минимум?) две альтернативы:
(1) Явно разделают уровни имён и того, что может быть их значениями, и вводят операцию «цитирования», превращающую первое во второе. В таком случае всё просто — имя никогда само по себе не является объектом, но может быть «поднято» (или «спущено», как смотреть) туда, и это уже не будет имя, это будет выражение, содержащее такое имя, и у этого выражения у самого будет имя.
(2) Имена — это значения «имён выше уровнем», уже третьим, и эту башню можно строить и далее ввысь (но редко нужно). Так, иногда говорят о
метапеременных, но это может быть полезно как раз для целей матлогики или теорий о языках, но не везде подряд.
Такая эзотерика вам скорее всего не пригодится, она именно что возникает в основном для нужд таких хитрых разделов, а не какого-нибудь там матанализа.
Ну мне кажется сомнительным modus pones. Кто вообще сказал, что я должен верить, что он работает?
А он работает и не всегда, но для этого рассматриваемая логика должна быть или слишком простой и бесполезной, или такой сложной, что там можно сказать MP разными способами и не все из них хороши.
MP идёт всегда в связке с импликацией и выражает часть её смысла: мы не можем принять выводимой импликацию
, когда при этом не можем вывести
, имея
. Аксиоматически мы можем гарантировать обратную сторону монеты: мы обязаны принять выводимой
, если из
можем вывести
. Но хотя бы одно правило вывода нам понадобится.
-- Пт окт 04, 2019 00:32:13 --(Я вдался в мелкие подробности и ответил на некоторые довольно отвлечённые вопросы просто для иллюстрации. На общем уровне там особо нечего говорить, конкретный выбор деталей зависит от конкретных же целей.)