Свойство дизъюнкции - проблема классической логики?

[epros]

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

Что значит «ту же логику»? Вон в теории нету никакого $\vdash$, а в метатеории есть. Теория у нас исчисление высказываний, а метатеория, как вы признали, предикатов.

Исчисление предикатов разрешает теориям вводить бинарные предикатные символы. Да, в теориях, которые рассматривает наша мета-теория, такого символа наверняка нет. Ну и что? Логика-то всё равно одна - классическое исчисление предикатов (я на самом деле не утверждаю, что рассматриваемые теории - в чистом исчислении высказываний, я только сказал, что мы ничего специфичного из исчисления предикатов не использовали при выводе - никаких там правил обобщения и т.п.).

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

Я даже честно не знаю как на это отвечать. Это неправильно. Ниоткуда не следует, что так должно быть хоть где-нибудь.

Попробуйте сказать почему это неправильно. Я вот хочу, к примеру, чтобы в сигнатуре моей мета-теории было всё необходимое для выражения формул типа $1+1=2$, причём рассматривать она может тоже такие теории, в которых это всё есть. Поэтому когда мета-теория подставляет $1+1=2$ вместо $a$ в выражения типа $c \to a$, то она интерпретирует $1+1=2$ как формулу своего языка, а когда она подставляет его вместо $a$ в выражения типа $c \vdash a$, то она интерпретирует это как формулу рассматриваемой теории. Если хотите, то можете во втором случае $1+1=2$ заключить в кавычки, по-моему, сути это не изменит.

Посмотрите теперь на любое из моих приведенных выше доказательств, в которых фигурируют и выражения типа $c \to a$, и выражения типа $c \vdash a$. Вы видите где-нибудь незаконный переход от одних к другим? Я пока нет. Может, я, конечно, где-то туплю...

[arseniiv]

epros в сообщении #1319126 писал(а):

Да, в теориях, которые рассматривает наша мета-теория, такого символа наверняка нет. Ну и что? Логика-то всё равно одна - классическое исчисление предикатов

Но вы на неё ещё и какие-то странные соотношения надеваете — поднимаете формулы теории до формул метатеории. Ну хотя бы ставили $\vdash$ тогда перед ними. Или $\vDash$. Или ещё какую штуковину.

epros в сообщении #1319126 писал(а):

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

Ну как бы вы предлагаете, так что вам говорить, почему это правильно (разве нет?).

epros в сообщении #1319126 писал(а):

Посмотрите теперь на любое из моих приведенных выше доказательств, в которых фигурируют и выражения типа $c \to a$, и выражения типа $c \vdash a$. Вы видите где-нибудь незаконный переход от одних к другим?

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

И интерпретацию ведь вас не попросишь предъявить, раз вы против них…

[Someone]

epros в сообщении #1319126 писал(а):

Логика-то всё равно одна - классическое исчисление предикатов

Совершенно разные логики: предметная логика и металогика. Пусть даже они обе называются "классической логикой". Нельзя смешивать предметную теорию и метатеорию. "Штопор" используется для записи в метаязыке метаутверждения о выводимости в предметной теории. Формулы предметной теории не являются формулами метатеории, а формулы метатеории не являются формулами предметной теории, и их никак нельзя смешивать.

[epros]

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

Ну как бы вы предлагаете, так что вам говорить, почему это правильно (разве нет?).

Ну нет конечно. Вы сказали, что неправильно, но не объяснили что именно и почему. Как так? А я-то как раз сказал, каких возможностей с моей точки зрения мы не имеем права лишить мета-теорию:

epros в сообщении #1319126 писал(а):

Я вот хочу, к примеру, чтобы в сигнатуре моей мета-теории было всё необходимое для выражения формул типа $1+1=2$, причём рассматривать она может тоже такие теории, в которых это всё есть.

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

Совершенно разные логики: предметная логика и металогика. Пусть даже они обе называются "классической логикой".

Это как? Логика - это просто некий набор правил, общих для всех теорий (в этой логике): общие правила синтаксиса, общий набор аксиом, общие правила вывода. У логики нет признака "мета" или "предметная".

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

Нельзя смешивать предметную теорию и метатеорию.

Теории я не смешиваю, рассматриваю только мета-теорию. Даже если речь об утверждениях каких-то предметных теорий, они рассматриваются только как утверждения мета-теории об утверждениях предметных теорий.

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

Формулы предметной теории не являются формулами метатеории, а формулы метатеории не являются формулами предметной теории, и их никак нельзя смешивать.

А вот формулы предметной и мета-теорий как раз неизбежно "смешиваются". Ибо в записи формулы мета-теории $a \vdash b$, хотите Вы или нет, присутствуют формулы предметной теории $a$ и $b$. Потому что:

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

"Штопор" используется для записи в метаязыке метаутверждения о выводимости в предметной теории.

В частности, мета-утверждение $a \vdash b$ говорит о выводимости $b$ в предметной теории с одной аксиомой $a$ (помимо стандартного набора "логических" аксиом).

-- Вт июн 12, 2018 00:54:04 --

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

поднимаете формулы теории до формул метатеории

Кстати, я не понял этой претензии. Вот формула $1+1=2$ - она предметной или мета-теории? Если в сигнатурах обеих теорий есть всё необходимое для её записи? Как я могу её "поднять", если я просто в одном месте рассматриваю её как формулу предметной теории, а в другом месте - ту же буквальную строку символов рассматриваю как формулу мета-теории? Причём из синтаксиса всегда понятно где что.

[arseniiv]

epros в сообщении #1319162 писал(а):

Вы сказали, что неправильно, но не объяснили что именно и почему. Как так?

Ну, все сознательные аргументы я уже привёл, остались ощущения (как у вас).

epros в сообщении #1319162 писал(а):

А я-то как раз сказал, каких возможностей с моей точки зрения мы не имеем права лишить мета-теорию:

epros в сообщении #1319126 писал(а):

Я вот хочу, к примеру, чтобы в сигнатуре моей мета-теории было всё необходимое для выражения формул типа $1+1=2$, причём рассматривать она может тоже такие теории, в которых это всё есть.

Для этого вовсе не обязательно смешивать формулы теории и метатеории как вы это делаете. Ещё раз, что вам мешает наставить штопоры где надо? Оно хотя бы формально корректным станет, остальное потом разберём.

epros в сообщении #1319162 писал(а):

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

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

epros в сообщении #1319162 писал(а):

Вот формула $1+1=2$ - она предметной или мета-теории?

Неизвестно из-за того что в ходу слишком много сокращений и нотаций. Если делать всё аккуратно, формулы теории будут вообще значениями объектов метатеории. Правда, когда имеешь дело с алгеброй термов (такой как множество термов или формул некоторого языка первого порядка), может затереться разница между выражением и его значением, потому что тогда интерпретация инъективна.

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

UPD.

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

значениями объектов метатеории

Перестарался тут, конечно же. Или объектами, или значениями термов.

[Someone]

epros в сообщении #1319162 писал(а):

Это как? Логика - это просто некий набор правил, общих для всех теорий (в этой логике): общие правила синтаксиса, общий набор аксиом, общие правила вывода. У логики нет признака "мета" или "предметная".

Признака нет. Есть интерпретации.

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

Разумеется, предметная теория и метатеория могут быть изоморфными в том смысле, что можно установить взаимно однозначное соответствие между их алфавитами так, чтобы термы соответствовали термам, формулы — формулам, аксиомы — аксиомам и т.д. Однако это всё равно разные теории. В частности, формулы предметной теории являются объектами, но не формулами метатеории.

epros в сообщении #1319162 писал(а):

А вот формулы предметной и мета-теорий как раз неизбежно "смешиваются". Ибо в записи формулы мета-теории $a \vdash b$, хотите Вы или нет, присутствуют формулы предметной теории $a$ и $b$.

Нет. Эти самые $a$ и $b$ — это объекты метатеории, которые мы интерпретируем как формулы предметной теории. Термы в языке метатеории, изображающие эти объекты, являются именами этих объектов. И $\vdash$ — двухместный предикат, который применяется, естественно, к упорядоченным парам объектов метатеории, интерпретируемых как формулы предметной теории.

epros в сообщении #1319162 писал(а):

Вот формула $1+1=2$ - она предметной или мета-теории?

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

[epros]

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

что вам мешает наставить штопоры где надо?

А где надо? По-моему, больше нигде не надо.

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

Ничего они не смешиваются. ... Формулы теории являются как раз значениями одного из видов термов метатеории (если мы выбрали её теорией первого порядка).

Ну да, в этом смысле и смешиваются: Формулы предметной теории являются частью формул мета-теории.

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

А потом вы зачем-то используете эти термы как формулы самой метатеории.

Не "я использую эти термы как ...", а они посимвольно совпадают с формулами самой мета-теории. Какой в этом криминал?

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

На деле это будут просто одинаковые имена для разносортных выражений, не более. Вы не можете их отождествлять, а одинаковость имён только путает.

Теории вообще "только именами" и манипулируют. "Самими объектами" могут манипулировать только те, кто работают руками, а не головой. И почему это должно "путать"? Вот формула языка арифметики $S0+S0=SS0$ выводима из аксиом арифметики. Мета-теория об этом может сказать так: $A \vdash S0+S0=SS0$. В силу теоремы дедукции отсюда следует $\vdash A \to S0+S0=SS0$ (где $A$ - объединенные по конъюнкции все те аксиомы арифметики, из которых сделан этот вывод). Если мета-теория имеет все те же символы в своей сигнатуре, т.е. способна записывать формулы арифметики как свои, то что ей мешает записать этот же вывод от своего имени, т.е. без штопора вначале строки?

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

чтобы определить формальную теорию (назовём её предметной теорией), мы должны определить её алфавит, термы, формулы и т.д.

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

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

В частности, формулы предметной теории являются объектами, но не формулами метатеории.

Так я ж сам об этом говорил.

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

Эти самые $a$ и $b$ — это объекты метатеории, которые мы интерпретируем как формулы предметной теории.

Хм. Объекты метатеории нет смысла интерпретировать как формулы предметной теории. Это термы мета-теории интепретируются как её объекты, каковые и есть формулы предметной теории. Точно так же, как термы арифметики интерпретируются как её объекты - натуральные числа. Нет смысла "интерпретировать" объекты арифметики как натуральные числа, ибо они и есть натуральные числа.

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

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

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

[Someone]

epros в сообщении #1319179 писал(а):

Хм. Объекты метатеории нет смысла интерпретировать как формулы предметной теории. Это термы мета-теории интепретируются как её объекты, каковые и есть формулы предметной теории.

Нет. Изначально у нас есть метатеория со своими объектами и нет никакой предметной теории. Мы некоторые объекты метатеории объявляем символами алфавита предметной теории, некоторые другие — строками символов, некоторые строки мы считаем термами, некоторые — формулами предметной теории, далее определяем аксиомы и правила вывода.

[epros]

Ну да, всё так. Некоторые объекты мета-теории объявляются формулами предметной теории. А в чём проблема?

Вот мы записываем в мета-теории: $\vdash A \to S0+S0=SS0$, где $A$ - объединённые конъюнкцией несколько аксиом арифметики, из которых выводится указанное арифметическое выражение. Из синтаксиса, а именно - из того, что $A \to S0+S0=SS0$ записано справа от штопора, мы понимаем, что речь идёт о формуле в языке рассматриваемой предметной теории - арифметики. Если все эти $S$, $0$, $+$ и $=$ есть также в сигнатуре мета-теории, то что мешает нам убрать штопор, т.е. сформулировать это утверждение от имени самой мета-теории?

[Someone]

epros в сообщении #1319234 писал(а):

А в чём проблема?

А в том, что объекты — это не формулы метатеории. А в предметной теории нет "штопора", и потому его нельзя писать в формулах.

[arseniiv]

epros в сообщении #1319179 писал(а):

А где надо? По-моему, больше нигде не надо.

Ну вот в таком, например, безобразии: $(c \to a) \to (c \vdash a)$. Его можно сделать корректным так: $\vdash(c \to a) \to (c \vdash a)$ или, например, так: $(\vdash c \to {\vdash a}) \to (c \vdash a)$. Здесь $c\to a,c,a$ — термы [метатеории], обозначающие формулы теории. Так как термы — не формулы, чтобы наставить вокруг них связки, их надо сначала засунуть в штопоры.

epros в сообщении #1319179 писал(а):

Ну да, в этом смысле и смешиваются: Формулы предметной теории являются частью формул мета-теории.

Но не являются же!

epros в сообщении #1319179 писал(а):

Не "я использую эти термы как ...", а они посимвольно совпадают с формулами самой мета-теории. Какой в этом криминал?

Они могут посимвольно совпадать только в разных никак не связанных мирах. Мы не можем соотносить имена из языка метатеории и языка рассматриваемой в ней теории. Это бессмысленно. Это так же бессмысленно как считать в формуле $Ax\wedge\exists x.Bx$ два вхождения икса чем-то связанными (потому что $\alpha$-конверсия легко превращает формулу в $Ax\wedge\exists y.By$).

epros в сообщении #1319179 писал(а):

Теории вообще "только именами" и манипулируют.

Я с этим не спорил.

epros в сообщении #1319179 писал(а):

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

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

[epros]

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

Ну вот в таком, например, безобразии: $(c \to a) \to (c \vdash a)$

Да, здесь есть какой-то подвох. Но не потому, что формулы мета-теории и предметной теории якобы "нельзя смешивать", а потому, что $c \to a$ сильнее, чем $\vdash c \to a$: Первое можно доказать с использованием аксиом мета-теории, а второе мы должны доказывать в чистом исчислении предикатов.

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

Его можно сделать корректным так: $\vdash(c \to a) \to (c \vdash a)$ или, например, так: $(\vdash c \to {\vdash a}) \to (c \vdash a)$.

Полагаю, что корректно так: $(\vdash c \to a) \to (c \vdash a)$. Только не пойму, откуда в приведённом доказательстве возьмётся первый штопор: Там ведь в качестве гипотезы первого уровня взято $c \to a$, а не $\vdash c \to a$.

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

Они могут посимвольно совпадать только в разных никак не связанных мирах. Мы не можем соотносить имена из языка метатеории и языка рассматриваемой в ней теории. Это бессмысленно

Да ладно, с чего бы это? Вот есть две разные теории - арифметика Пеано и арифметика Пресбургера. В обеих есть "имя" (замкнутый терм) $SS0$, обозначающее число два. С чего бы это мы не могли эти имена из двух разных теорий соотнести? Арифметика Пресбургера, конечно, может сказать о числах не всё, что о них может сказать арифметика Пеано, но всё же это те же самые числа.

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

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

Какие описания я должен сделать? Что из аксиомы $x+S0=Sx$ подстановкой замкнутого терма $S0$ вместо переменной $x$ можно получить то самое $S0+S0=SS0$? И что этот вывод можно сделать в любой теории первого порядка, имеющей соответствующие символы в сигнатуре, а значит и в мета-теории тоже?

[arseniiv]

epros в сообщении #1319325 писал(а):

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

Сколько раз ни говори «халва»…

epros в сообщении #1319325 писал(а):

Только не пойму, откуда в приведённом доказательстве возьмётся первый штопор: Там ведь в качестве гипотезы первого уровня взято $c \to a$, а не $\vdash c \to a$.

Могу только развести руками. Это же у вас unsound теория получается, не у меня.

epros в сообщении #1319325 писал(а):

Да ладно, с чего бы это? Вот есть две разные теории - арифметика Пеано и арифметика Пресбургера. В обеих есть "имя" (замкнутый терм) $SS0$, обозначающее число два. С чего бы это мы не могли эти имена из двух разных теорий соотнести?

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

epros в сообщении #1319325 писал(а):

Какие описания я должен сделать? Что из аксиомы $x+S0=Sx$ подстановкой замкнутого терма $S0$ вместо переменной $x$ можно получить то самое $S0+S0=SS0$? И что этот вывод можно сделать в любой теории первого порядка, имеющей соответствующие символы в сигнатуре, а значит и в мета-теории тоже?

Да нет, совсем не эти. Просто опишите выбранное вами изначально исчисление высказываний в выбранной вами арифметике первого порядка. И посмотрите, будут ли там получаться штуки вида $(c \to a) \to (c \vdash a)$.

Всё, ушёл, покуда ничего заведомо более интересного здесь не будет построено.

[epros]

В общем, мой вывод на данный момент такой: $(c \to a) \to (c \vdash a)$ - конечно же неверно, но не потому, что одни и те же $c$ и $a$ использованы в разных смыслах в одном и том же выражении в левой и правой его части, а потому, что есть неверный шаг вот в этом доказательстве:

epros в сообщении #1318877 писал(а):

1) Гипотеза первого уровня: $c \to a$,
2) Гипотеза второго уровня: $c$.
3) Модус поненс из 2 и 1: $a$.
4) Констатируем вывод от 2 до 3: $c \vdash a$ (это даже не дедукция, поскольку нам импликация не нужна).
5) Дедукция от 1 до 4: $(c \to a) \to (c \vdash a)$.

Думаю, что неверный шаг - 4. Потому что мы констатируем вывод $a$ из $c$ в исчислении предикатов, а на самом деле нужно указывать весь список аксиом и гипотез, из которых он сделан. Т.е. правильная констатация вывода будет: $c \to a, c \vdash a$, что ничего нам не даст.

В переходе же от $a$ и $c$, интерпретируемых как формулы, к $a$ и $c$, интерпретируемым как объекты, я проблемы не вижу, ибо формулы языка могут интерпретироваться как объекты и мета-теория должна это понимать.

[george66]

А если в качестве формулы $c$ взять истину, получится $a\to\,\vdash a$