Совпадение теорем

[Someone]

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

И что?

Ложное высказывание $X$ Вы будете интерпретировать как синоним высказывания

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

"$X$ истинно"

[Sinoid]

Someone в сообщении #1150392 писал(а):

выводимость формулы $\forall a(6\mid a\rightarrow 3\mid a)$.

Внутри теории, определяемой некоторой совокупностью аксиом. Верно?

[arseniiv]

Угу.

[Sinoid]

Someone в сообщении #1150392 писал(а):

выводимость формулы $\forall a(6\mid a\rightarrow 3\mid a)$. Sinoid в сообщении #1150388

писал(а):
употребляемая здесь импликация принадлежит метатеории и не принадлежит предметной теории. Правильно? Неправильно. Написанная формула принадлежит языку предметной теории.

А в предметной теории импликация сама по себе как-то определяется?

[arseniiv]

Логическими аксиомами.

[Sinoid]

Sinoid в сообщении #1150469 писал(а):

А в предметной теории импликация сама по себе как-то определяется?

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

Логическими аксиомами.

А это определение зависит от самой предметной теории, внутри которой определяется импликация?

[arseniiv]

Смотря что называть зависимостью. Аксиомы теории — это практически всегда объединение аксиом какой-то «чистой» логической системы (исчисление высказываний, предикатов, предикатов второго порядка, модальные, интуиционистские варианты etc.) с аксиомами, обязательно включающими в себя внелогические символы, и их потому можно понимать как «содержательные», определяющие что-то не относящееся к логике (собственные аксиомы). Определением импликации можно будет считать некоторое подмножество несобственных логических аксиом. Хотя тут можно пуститься в ненужную философию насчёт того, включать ли туда Modus ponens и не считать ли вообще все аксиомы вместо этого правилами вывода. Боюсь, зря я сказал последнее.

-- Сб сен 10, 2016 22:07:06 --

Честно говоря, это же всё основы, я ничего нового сейчас не написал.

[Someone]

Все логические связки определяются своими аксиомами в математической логике.

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

[Sinoid]

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

Честно говоря, это же всё основы, я ничего нового сейчас не написал.

Сейчас, еще пару вопросов и вопросы закончатся. Просто у, например, того же Клини непривычное для меня построение. И я хочу понимать, так сказать, краеугольные моменты, к которым должен прийти, понятными для меня сейчас словами. Значит, вот у нас была некоторая предметная теория, в которой были определены, скажем, дизъюнкция и импликация, для которых в исходной предметной теории не существует никаких таблиц истинности. Вот я эту предметную теорию каким-то образом интерпретировал, получил определенную модель и в этой модели для дизъюнкции и импликации уже существуют таблицы истинности. Верно?

[arseniiv]

Sinoid в сообщении #1150482 писал(а):

Сейчас, еще пару вопросов и вопросы закончатся.

Это был указатель не на неуместность вопросов, а на то, чтобы вы потом перепроверили, что там с литературой.

Всё-таки тут стоит остановиться и найти определение интерпретации хотя бы для языков первого порядка.

[Sinoid]

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

Всё-таки тут стоит остановиться и найти определение интерпретации хотя бы для языков первого порядка.

А это означает и полную остановку в этом направлении: я даже не знаю, что такое порядок языка.
Слушайте, а может, вот тут

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

Ещё можно добавить, что «теорема $A$» значит, что $A$ выводима (где-то там),

точнее было бы сказать, что «теорема $A$» означает истинность выводимости теоремы $A$, причем слова теоремы $A$ я не беру в кавычки, потому что они относятся к метаязыку?

[arseniiv]

Sinoid в сообщении #1150601 писал(а):

А это означает и полную остановку в этом направлении: я даже не знаю, что такое порядок языка.

Язык первого порядка состоит из формул логики предикатов.

Sinoid в сообщении #1150601 писал(а):

Слушайте, а может, вот тут точнее было бы сказать, что «теорема $A$» означает истинность выводимости теоремы $A$, причем слова теоремы $A$ я не беру в кавычки, потому что они относятся к метаязыку?

Не надо умножать сущности без причины.

[Sinoid]

А вот Введение в метаматику Клини хорошая книга? Может, ее почитать перед его Математической логикой?

[Sinoid]

Someone в сообщении #1150392 писал(а):

А метатеории принадлежит утверждение о выводимости этой формулы, то есть, другая формула: $\vdash\forall a(6\mid a\rightarrow 3\mid a)$

А словами это сказать так: Выводимость из выводимости деления числа на 6 выводимости его деления на 3. Верно?

[arseniiv]

Просто «выводится $\forall a(6\mid a\rightarrow 3\mid a)$». Формула внутри — не формула метатеории, там нет никаких выводимостей. Она читается «для всех $a$ если 6 делит $a$, то 3 делит $a$». Всё вместе в итоге читается (например) «выводится формула «для всех $a$ если 6 делит $a$, то 3 делит $a$»».