Что дает нам право доказывать теоремы?

[OcarinGate]

Всем привет. Я в мат. логике новичек, и до меня не доходит одна вещь. Допустим есть у нас такая логическая теория как исчисление высказываний. Вещь формализованная, и при ее создании мы выбираем набор аксиом и правила вывода(ну и язык и все остальное, важны сейчас первые два пункта). Так вот в этом исчислении при помощи MP и только при помощи него можно выводить. Однако же есть у нас и арифметика, где так же задаются аксиомы, но доказывать теоремы из нее можем с помощью чего угодно, любых правил вывода, в частности в любом учебнике по математике, при док-ве теорем автор(любой) использует и приведение к абсурду, и исключающее третье. То есть создавая арифметику как аксиоматическую теорию, не закладываются правила вывода? Или арифметика не является формальной? А может я вообще бред несу? Опять же в первых главах учебника по мат логике которые я сейчас читаю (Игошин В.И. - Математическая логика и теория алгоритмов) , в алгебре высказываний(не исчислении), автор доказывает теоремы используя любые правила вывода. И чтобы отдельно тему не создавать можете пояснить - правила вывода же, это тавтологии логической теории,верно? Почему тогда так часто в математике доказывают с помощью именно например MP и исключающего третьего, и некоторых других. В чем например особенность MP? Очень хорошо показывает себя на практике, или есть другие глубокие причины?

[iifat]

OcarinGate в сообщении #1376050 писал(а):

правила вывода же, это тавтологии логической теории,верно?

Нет. Правила вывода — это правила перехода от одной тавтологии к другой.
А вообще... Ну, одно из любимых занятий математиков — анализ. Возьмём хорошо всем знакомую арифметику, обрубим всё что можно и посмотрим, что от неё останется. Например, оставим только одну операцию из двух, единицу, да возможность деления — получим группы, изучая которые можно получить немало интересного, что можно с успехом применить уже к арифметике.
Примерно так же соотносится формальная логика с обычной.
Кроме того, касательно MP — ну, к примеру, известно, что все логические операции можно выразить через какой-нить штрих Шеффера; однако, пользоваться только им просто неудобно — простейшие выражения будут выглядеть трёхэтажными каббалистическими знаками. Да, для доказательства теорем достаточно MP; все остальное — чисто для удобства. Как и в любой области ­— понадокажем теорем, потом только ссылаемся на них, не повторяя доказательства.

[mihaild]

Есть разные исчисления. Классическое исчисление высказываний формализует средства, которые мы используем для работы с утверждениями без учета их "внутренней структуры".
Есть исчисление предикатов, которое формализует "обычные" рассуждения в математике. Оно формализовано (в нем уже три правила вывода - modus ponens и правила Бернайса). И арифметика (Пеано) формализуется именно в исчислении предикатов.

Но писать всё абсолютно формально очень неудобно (например сравнительно простое утверждение $2 + 2 = 4$ требует 26323 шагов для доказательства), и не особо нужно. Для упрощения жизни используются два основных подхода.
Во-первых, мы доказываем, что если что-то выводимо, то что-то другое тоже выводимо - и тем самым получаем правила вывода. Правда само по себе это утверждение про выводимость доказывается уже не в том исчислении, о которым мы говорим, а в каком-то другом (обычно не формализованном). Например, есть специальная теорема об исчислении высказываний (не теорема исчисления высказываний): если $\Gamma \cup \{X\} \vdash \bot$, то $\Gamma \bot X$. Это позволяет нам попробовать добавить $X$ к аксиомам, и, формально выведя противоречие, сказать, что можно вывести $\neg X$.
Во-вторых, мы можем писать рассуждения на приближенном к естественному языку, надеясь, что все заинтересованные лица при необходимости смогут формализовать нужные куски, и сделают это скорее всего примерно одним и тем же способом.

[arseniiv]

mihaild в сообщении #1376084 писал(а):

например сравнительно простое утверждение $2 + 2 = 4$ требует 26323 шагов для доказательства

Для справедливости и уменьшения возможного испуга ТС надо заметить, что для арифметики Пеано шагов сильно меньше (должно быть всего пару десятков, ну и конечно немного зависит от того, определяем ли мы 2 как $S1$, $SS0$ или $1+1$), а в Metamath говорится сразу о комплексных числах (и вообще там ради удобства строятся сначала «примитивные» $N, Z, Q, R$, использующиеся только для построения $\mathbb C$, а вот уже в нём выделяются $\mathbb{N, Z, Q, R}$ как настоящие подмножества, и 1 является единицей именно $\mathbb C$ [df-1], ну а 2 и 4 определяются уже сложением этой 1 с собой).

-- Пт фев 15, 2019 06:19:18 --

(Подобным же образом у Бурбаки где-то была наводящая ужас «формула единицы», с которой тоже должно быть не всё так просто.)

[mihaild]

(Оффтоп)

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

Подобным же образом у Бурбаки где-то была наводящая ужас «формула единицы»

И там настолько простое определение, что у Бурбаки даже неправильно оценена его длина: оценка была "несколько десятков тысяч", а на самом деле 4,523,659,424,929. А в издании 1970 года - 2409875496393137472149767527877436912979508338752092897 $\approx 2.4 \cdot 10^{54}$.

[Qlin]

OcarinGate в сообщении #1376050 писал(а):

Допустим есть у нас такая логическая теория как исчисление высказываний.

Такой теории нет и быть не может. Вы путаете теории (в частности арифметику) с логическими исчислениями, которые не являются теориями.

OcarinGate в сообщении #1376050 писал(а):

Так вот в этом исчислении при помощи MP и только при помощи него можно выводить.

В этом исчислении только с помощью МР вывести ничего нельзя. Минимальный набор должен включать в себя помимо МР ещё правила подстановки. То есть как минимум нужно уметь подставлять одни высказывательные формы в другие.

OcarinGate в сообщении #1376050 писал(а):

правила вывода же, это тавтологии логической теории,верно?

Нет. Но в арифметике у вас должно быть правило вывода, позволяющее выполнять подстановку формул арифметики в тавтологии.

[george66]

Несёте такой бред, что в двух словах не прояснить. Некоторые комментаторы ещё усугубляют. Советую учиться по книжке Верещагина и Шеня
http://gen.lib.rus.ec/search.php?req=+% ... column=def
(главу "Схемы из функциональных элементов" можно пропустить)

[arseniiv]

mihaild
Спасибо за статью, особенно мне понравилась последняя часть, Discussion.