Кванторы и термы

[Sinoid]

Здравствуйте! Вопрос, конечно, глупый, но развейте, пожалуйста, мои сомнения. Кванторы в термы ведь не могут входить?

[Xaositect]

Ну смотря в какой теории. Бывают теории, в которых термы могут содержать формулы, напр. $\{x | \neg\exists y\, x < y\}$. В обычном изложении теории первого порядка - не могут.

[knizhnik]

Xaositect в сообщении #1182426 писал(а):

$\{x | \neg\exists y\, x < y\}$

Но ведь эта запись - в логике первого порядка? Ведь предикат тут поставлен конкретный, а не произвольный.

[Xaositect]

Да, но обычно при изложении теории первого порядка такие термы не определяются, а потом описываются как метасокращения для конструкций формального языка, а не как элементы какого-то модифицированного формального языка. Т.е. например $z = \{x|\neg\exists y x < y\}$ это сокращение для формальной формулы $\exists u\, \forall x\, (x\in u \Leftrightarrrow \neg\exists y\, x < y) \wedge z = u$.
Это делается, как я понимаю, чтобы не доказывать одни и те же теоремы для разных модификаций, а ограничиться только базовым языком.

[Sinoid]

Xaositect в сообщении #1182426 писал(а):

Бывают теории, в которых термы...

Определение терма:
1. 0 есть терм
2. Каждая переменная есть терм
3-5. Если $\mathrm{s}$ и $\mathrm{t}-$ термы, то $(\mathrm{s})+(\mathrm{t})$, $(\mathrm{s})\cdot(\mathrm{t})$ и $(\mathrm{s})'-$ термы
6. Никаких других термов, кроме определенных согласно 1-5, нет.
А перед этим определением, в обычном тексте, написано

Цитата:

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

[Someone]

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

[Sinoid]

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

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

Так-то так, но проблема в том, что после такого определения терма, в следующем параграфе, без какой бы то ни было модификации определения терма вводится понятие свободное вхождение переменной $\mathrm{x}$ в терм $\mathrm{a}$, требующее принципиальную возможность вхождения квантора в терм. И как это все понять ума не приложу.

-- 07.01.2017, 20:24 --

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

Sinoid, Вы совершенно правы,

Это не я прав, это Клини.

[Someone]

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

проблема в том, что после такого определения терма, в следующем параграфе

Уточните место: какая книга, какой параграф и т.п. Чтобы я мог найти и посмотреть, что там.

[Sinoid]

Клини С.К. Введение в метаматематику, стр. 72, параграф 18, он называется "Свободные и связанные переменные. Книга 1957 года.

[Someone]

Ага, нашёл.

Не вижу там ничего криминального. Клини пишет:

Цитата:

Мы будем говорить также, что любое вхождение переменной $x$ в терм $t$ является свободным, как это будет следовать из приведенного определения, если заменить в нем слова «формула $A$» на «терм $t$».

Так и есть: поскольку, согласно приведённому определению терма, никаких кванторов внутри терма нет, то и связанным переменным в терме взяться неоткуда.

[Sinoid]

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

Так и есть: поскольку, согласно приведённому определению терма, никаких кванторов внутри терма нет, то и связанным переменным в терме взяться неоткуда.

А тогда зачем вообще вводить понятие свободной и связанной переменной для терма, если, по крайней мере, на данном месте книги, эти понятия неразличимы?

[Someone]

А где он вводит понятие связанной переменной специально для терма?

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

если, по крайней мере, на данном месте книги, эти понятия неразличимы?

Почему "неразличимы"? Наоборот, в одну группу попадают вообще все термы, а в другую — ни одного. А вдруг в будущем ему это понадобится?

[arseniiv]

(Оффтоп)

Жалко, у Клини, кажется, не упоминаются индексы де Брёйна. А то можно формулы со связанными переменными понимать как метасокращения для формул с индексами… Хотя бы в этом случае проблема корректности замены сменяется довольно прозрачной поддержкой этих индексов. Притом их можно приспособить и для обозначения свободных переменных.

[Sinoid]

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

Наоборот, в одну группу попадают вообще все термы, а в другую — ни одного. А вдруг в будущем ему это понадобится?

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

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

А где он вводит понятие связанной переменной специально для терма?

Там же где он вводит понятие связанного вхождения переменной в формулу: свободное вхождение в формулу является случаем, противоположным для связанного. Значит, в случае формулы для определения понятия свободного вхождения нужно определение понятия связанного вхождения. И это переносится на терм.

[Someone]

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

Так и вводил бы когда нужно, предварительно переопределив понятие терма.

Ну, это вопрос не ко мне, а к автору книги.

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

Там же где он вводит понятие связанного вхождения переменной в формулу: свободное вхождение в формулу является случаем, противоположным для связного. Значит, в случае формулы для определения понятия свободного вхождения нужно определение понятия связанного вхождения. И это переносится на терм.

Там этого не написано, это уже ваши домыслы. Я согласен, что такая интерпретация текста возможна, но не вижу ничего криминального.

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