Метатеоремы

[kry]

(Оффтоп)

oleg.k в сообщении #1427169 писал(а):

Математику тогда можно будет считать эмпирической наукой, где основной критерий истинности - соответствие с опытом.

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

[kernel1983]

Дело всё в том, что, по-видимому, ни одну математическую науку нельзя изложить посдедовательно, начиная с самых азов. Всё равно придётся ссылаться на другие разделы математики, а для их построения нужна та самая математическая наука, которую мы пытаемся изложить. Даже в такой простой науке, как логика высказываний (не исчисление), потребуется, например, аксиома индукции Пеано.

[epros]

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

Разве в классическом?

Именно в классическом. Несмотря на тавтологичность $(r \to (p \vee q)) \to ((r \to p) \vee (r \to q))$ для формул полного по Тьюрингу языка из $r \vdash p \vee q$ вообще говоря не следует $r \vdash p$ или $r \vdash q$. Это говорит о том, что логическая выводимость (обозначаемая как $\vdash$) и логическое следствие (изображаемое значком импликации $\to$) для классической логики - это принципиально разные вещи.

[arseniiv]

Я бы не сказал, что дизъюнктивное свойство выводимости обязательно, чтобы различие между следствием и выводимостью было не страшным. Различие же останется и если такое свойство выполнено.

[epros]

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

[arseniiv]

А что тут нового страшного, если мы изначально принимаем заведомо классические (в смысле не конструктивные) аксиомы вроде $a\vee\neg a$? Это же из-за них проблемы. Сами такого захотели. Хотя да, теперь я не знаю, что именно я аргументирую. Но по-моему пока теорема о дедукции работает, выводимость ещё не далеко уходит от импликации.

-- Пт ноя 29, 2019 23:47:53 --

В общем это слишком абстрактно-философский вопрос; перед нами в конкретные моменты стоят конкретные задачи, вот с точки зрения их решаемости гораздо конструктивнее можно что-то охарактеризовать. А если говорить о страшном, меня пугает, какие есть подгруппы движений гиперболической плоскости.

[epros]

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

Но по-моему пока теорема о дедукции работает, выводимость ещё не далеко уходит от импликации.

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

[arseniiv]

Нет, ещё раз, а что, в промежуточных логиках, интуиционистской логике и минимальных логиках совсем никаких проблем нет?

-- Сб ноя 30, 2019 13:19:58 --

(Я-то знаю цену классической логике. Но.)

[epros]

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

Нет, ещё раз, а что, в промежуточных логиках, интуиционистской логике и минимальных логиках совсем никаких проблем нет?

В конструктивном анализе это всё трактуется совершенно иначе, начиная с того, что $(r \to (p \vee q)) \to ((r \to p) \vee (r \to q))$ - не тавтология, и заканчивая тем, что требования конструктивности не ограничиваются логикой, а распространяются и на прикладные аксиоматики (имеются в виду свойства теорий - дизъюнктивности, существования и правило Чёрча). В итоге всё вроде бы оказывается направленным на то, чтобы взаимозаменяемость выводимости и следствия сохранялась. Хотя я не уверен, что оная взаимозаменяемость в итоге гарантируется.

Зато можно быть совершенно уверенным в том, что в классическом анализе её нет.

[Lia]

Оффтоп отделен в «Метатеоремы: оффтоп»