Оцените «мощь» логики второго порядка на примере

[epros]

migmit в сообщении #608128 писал(а):

А одно из правил языка - "использовать только известные слова".

О! И тут мы приходим к разнице между логикой первого и второго порядков. В логике первого порядка можно сказать: "Всемогущий существует", и это будет именно "использование неизвестного слова" - Вы тут же начнёте задавать мне каверзные вопросы о том, что это за теория такая, в сигнатуре которой определён предикатный символ "Всемогущий". А готового ответа у меня и нет... Но в логике второго порядка - и не надо! Берём тавтологию:
$\forall X ~ [\exists x ~ X(x) \vee \nexists x ~ X(x)]$,
внимательно её читаем и видим, что "для любого свойства можно утверждать...". Понимаете, об этом буквально сказано. Вы видите, что никаких ограничений на квантор всеобщности нет?

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

migmit в сообщении #608128 писал(а):

Вы правда считаете, что "формула" и "математический текст" - это одно и то же?

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

migmit в сообщении #608128 писал(а):

Это вообще какой-то бессмысленный набор слов.

$[\mathbb{N}(0) \wedge \forall x ~ \mathbb{N}(x) \to \mathbb{N}(S(x))] \to \forall y ~ \mathbb{N}(y)$ - формула второго порядка с одной свободной переменной $\mathbb{N}$, которая определяет свойство "являться стандартным натуральным числом" - ровно в том же смысле, в котором их определяет теория множеств. Что тут непонятного?

Поставьте квантор всеобщности - и получите аксиому индукции, коя имеет место быть в арифметике второго порядка. Это - не пример "определения понятия натурального числа"?

migmit в сообщении #608128 писал(а):

Это мы должны его предоставить. Иначе формула не является синтаксически корректной.

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

[Xaositect]

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

migmit в сообщении #608128 писал(а):

А одно из правил языка - "использовать только известные слова".

О! И тут мы приходим к разнице между логикой первого и второго порядков. В логике первого порядка можно сказать: "Всемогущий существует", и это будет именно "использование неизвестного слова" - Вы тут же начнёте задавать мне каверзные вопросы о том, что это за теория такая, в сигнатуре которой определён предикатный символ "Всемогущий". А готового ответа у меня и нет... Но в логике второго порядка - и не надо! Берём тавтологию:
$\forall X ~ [\exists x ~ X(x) \vee \nexists x ~ X(x)]$,
внимательно её читаем и видим, что "для любого свойства можно утверждать...". Понимаете, об этом буквально сказано. Вы видите, что никаких ограничений на квантор всеобщности нет?

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

[epros]

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

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

«Особой» разницы может и нет. Кроме того, что есть явное утверждение о том, что можно подставлять ЛЮБОЕ свойство. В логике первого порядка такого явного утверждения нет, отсюда и всевозможные спекуляции на тему, что якобы нужно иметь хоть какое-то определение свойства.

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

[migmit]

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

внимательно её читаем и видим, что "для любого свойства можно утверждать...". Понимаете, об этом буквально сказано. Вы видите, что никаких ограничений на квантор всеобщности нет?

Естественно. Но чтобы что-то подставлять, нужно, чтобы это что-то было. А у вас нет.

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

Так что Ваши попытки ограничить область действия тавтологии какими-то "определёнными" или "известными" свойствами - совершенно неадекватны логике второго порядка.

Я ничего не ограничиваю. Я лишь требую синтаксической корректности.

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

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

Да. Как только у вас ЕСТЬ эта константа. А у вас есть только символ.

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

$[\mathbb{N}(0) \wedge \forall x ~ \mathbb{N}(x) \to \mathbb{N}(S(x))] \to \forall y ~ \mathbb{N}(y)$ - формула второго порядка с одной свободной переменной $\mathbb{N}$, которая определяет свойство "являться стандартным натуральным числом" - ровно в том же смысле, в котором их определяет теория множеств. Что тут непонятного?

Э... ничего. Во-первых, теория множеств определяет натуральные числа не при помощи аксиом Пеано, а конструктивно, как кардиналы конечных множеств. Впрочем, об определениях договариваются, так что это непринципиально. Во-вторых, формула будет корректной только после того, как вы определите, что такое $S$. В третьих, возьмите всегда истинный предикат, подставьте его в эту формулу, и получите тавтологию. Мне не кажется, что всегда истинный предикат есть свойство "являться натуральным числом".

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

В данном случае, всё, что ему нужно - это уметь отличать символы констант от символов переменных.

"Символы констант" появляются только когда у вас есть сигнатура теории. Пока у вас сферическая логика в вакууме, никаких "символов констант" нет.

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

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

Запас символов — ради бога. А вот самих констант у нас нет.

[epros]

migmit в сообщении #608328 писал(а):

Запас символов — ради бога. А вот самих констант у нас нет.

Ба, а что это такое «сама константа»? Я как-то привык думать, что константа - это функциональный символ нулевой арности. У меня такое чувство, что Вы пытаетесь втащить в синтаксис какую-то семантику. Синтаксическая корректность - это только про символы (разных видов) и про то, как они могут быть расставлены друг относительно друга.

migmit в сообщении #608328 писал(а):

Во-первых, теория множеств определяет натуральные числа не при помощи аксиом Пеано, а конструктивно, как кардиналы конечных множеств

Если взглянуть на эту формулу внимательнее, то можно заметить, что она утверждает, что $\mathbb{N}$ является минимальным из индуктивных множеств (при надлежащей интерпретации нуля и операции инкремента).

P.S. Тьфу, я конечно же там поспешил с выписыванием формулы. Правильно так:

$\forall X ~ [X(0) \wedge \forall x ~ X(x) \to X(S(x))] \to [\forall y ~ \mathbb{N}(y) \to X(y)]$

migmit в сообщении #608328 писал(а):

Во-вторых, формула будет корректной только после того, как вы определите, что такое $S$.

И опять та же неправильность. Определение $S$ влияет на определение натурального числа (делает его более содержательным), но не влияет на синтаксическую корректность формулы.

migmit в сообщении #608328 писал(а):

В третьих, возьмите всегда истинный предикат, подставьте его в эту формулу, и получите тавтологию. Мне не кажется, что всегда истинный предикат есть свойство "являться натуральным числом".

Правильно подмечено. Потому что такое определение - недостаточно содержательно. В арифметике оно обычно сопровождается как минимум ещё двумя аксиомами:

$\forall x ~ S(x) \ne 0$ и
$\forall x,y ~ S(x)=S(y) \to x=y$.

Ограничив кванторы только натуральными числами, получим:

$\forall x ~ \mathbb{N}(x) \to S(x) \ne 0$ и
$\forall x,y ~ \mathbb{N}(x) \wedge \mathbb{N}(y) \to [S(x)=S(y) \to x=y]$.

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

P.S. И всё равно недостаточно содержательное. Строго говоря, есть ещё что добавить.

migmit в сообщении #608328 писал(а):

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

Так что Ваши попытки ограничить область действия тавтологии какими-то "определёнными" или "известными" свойствами - совершенно неадекватны логике второго порядка.

Я ничего не ограничиваю. Я лишь требую синтаксической корректности.

Неужели? А говорили о каком-то наличии определения. Вот арифметика первого порядка чем отличается от арифметики второго порядка? Только формулировкой индукции. В арифметике первого порядка индукция распространяется только на формулы. Т.е. в Вашей формулировке - только на те свойства, которые «определены». А в арифметике второго порядка индукция распространяется на ЛЮБЫЕ свойства - именно это буквально и утверждает аксиома индукции второго порядка. Какие-такие «любые» свойства кроме тех, что определены формулами? Правильно: те свойства, которые НИКАК не определены. И эта добавка про никак не определённые свойства существенным образом усиливает теорию.

[migmit]

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

Синтаксическая корректность - это только про символы (разных видов) и про то, как они могут быть расставлены друг относительно друга.

Именно. Ну блин, посмотрите, как именно строятся логические формулы.

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

P.S. Тьфу, я конечно же там поспешил с выписыванием формулы. Правильно так:

$\forall X ~ [X(0) \wedge \forall x ~ X(x) \to X(S(x))] \to [\forall y ~ \mathbb{N}(y) \to X(y)]$

Чудно. Теперь возьмите в качестве $\mathbb{N}$ предикат, который всегда ложен. Вы при этом тоже получите тавтологию.

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

И опять та же неправильность. Определение $S$ влияет на определение натурального числа (делает его более содержательным), но не влияет на синтаксическую корректность формулы.

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

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

P.S. И всё равно недостаточно содержательное. Строго говоря, есть ещё что добавить.

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

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

migmit в сообщении #608328 писал(а):

Я ничего не ограничиваю. Я лишь требую синтаксической корректности.

Неужели? А говорили о каком-то наличии определения.

Именно. Более того, наличия определения непосредственно в формуле. Иначе она некорректна.

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

В арифметике первого порядка индукция распространяется только на формулы.

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

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

А в арифметике второго порядка индукция распространяется на ЛЮБЫЕ свойства

Но если свойства НЕТ, то на него ничего распространяться не может.

[epros]

migmit в сообщении #608486 писал(а):

Ну блин, посмотрите, как именно строятся логические формулы.

Куды смотреть? Давайте я Вам подскажу: гуглите словосочетание "порождающая грамматика", изучаете сие понятие, и оно Вам рассказывает всё о том, "как строятся формулы".

migmit в сообщении #608486 писал(а):

Во-первых, "более содержательным" - это осетрина второй свежести.

Вот не надо этого. Исключив из теории часть аксиом, мы получим менее содержательную теорию. Вернув их, соответственно, поучим более содержательную теорию. Причём тут свежесть?

migmit в сообщении #608486 писал(а):

Во-вторых, синтаксически формула, содержащая неопределённые символы, некорректна.

"Неопределённые символы" - это что за зверь такой?

migmit в сообщении #608486 писал(а):

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

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

migmit в сообщении #608486 писал(а):

наличия определения непосредственно в формуле. Иначе она некорректна.

Бред какой-то. Приведите пример определения "непосредственно в формуле".

migmit в сообщении #608486 писал(а):

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

Ха-ха-ха. Это так Вы понимаете разницу между арифметиками первого и второго порядков? Т.е. аксиома индукции второго порядка просто "сводит в одно" всю схему аксиом индукции первого порядка, ничего нового не добавляется? Объясните же мне пожалуйста, каким же тогда удивительным образом в арифметике второго порядка становится доказуемой теорема Гудстейна, которая была недоказуема в арифметике первого порядка?

migmit в сообщении #608486 писал(а):

Но если свойства НЕТ, то на него ничего распространяться не может

А Вы доказали, что "свойства нет"? Вы понимаете, что в классической логике утверждение о НЕ существовании - это тоже утверждение, и его нельзя провозглашать только потому, что Вы соответствующего определения "пока не видели"?

[migmit]

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

Давайте я Вам подскажу: гуглите словосочетание "порождающая грамматика", изучаете сие понятие, и оно Вам рассказывает всё о том, "как строятся формулы".

Ну, можно. Где вы там увидели утверждение "любую последовательность символов можно подставить в формулу"?

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

Причём тут свежесть?

Уговорили, снимается.

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

migmit в сообщении #608486 писал(а):

Во-вторых, синтаксически формула, содержащая неопределённые символы, некорректна.

"Неопределённые символы" - это что за зверь такой?

Это которые не определённые.

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

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

Ни в коей мере, но вы-то говорите о натуральных числах, не?

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

migmit в сообщении #608486 писал(а):

наличия определения непосредственно в формуле. Иначе она некорректна.

Бред какой-то. Приведите пример определения "непосредственно в формуле".

"Если $G$ - множество, а $\cdot$ - бинарная операция на $G$, удовлетворяющая аксиомам (здесь перечисление аксиом группы), то..."

Разумеется, в математическом тексте никто так не пишет, на то и придуманы определения, чтобы подобное сокращать до "Если $G$ - группа..."

Но в формуле это должно быть. Либо - не должно быть понятия "группа".

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

Это так Вы понимаете разницу между арифметиками первого и второго порядков?

В том, что касается аксиомы индукции - это так.

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

Т.е. аксиома индукции второго порядка просто "сводит в одно" всю схему аксиом индукции первого порядка, ничего нового не добавляется?

Не совсем так. Аксиома индукции второго порядка вводит свободную переменную.

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

А Вы доказали, что "свойства нет"? Вы понимаете, что в классической логике утверждение о НЕ существовании - это тоже утверждение, и его нельзя провозглашать только потому, что Вы соответствующего определения "пока не видели"?

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

[epros]

migmit в сообщении #608521 писал(а):

Где вы там увидели утверждение "любую последовательность символов можно подставить в формулу"?

А я разве такое утверждал? Разумеется, не любую последовательность символов и не в любое место можно подставить. Но любые символы констант (первого или второго рода) в определённые для них места можно подставлять.

migmit в сообщении #608521 писал(а):

Ни в коей мере, но вы-то говорите о натуральных числах, не?

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

migmit в сообщении #608521 писал(а):

"Если $G$ - множество, а $\cdot$ - бинарная операция на $G$, удовлетворяющая аксиомам (здесь перечисление аксиом группы), то..."

Разумеется, в математическом тексте никто так не пишет, на то и придуманы определения, чтобы подобное сокращать до "Если $G$ - группа..."

Но в формуле это должно быть. Либо - не должно быть понятия "группа".

Эти словеса - ещё далеко не формула. Конечно, при некотором усилии их можно довести до формул. Но тут-то Вы как раз и упустите момент, когда "неопределённый символ" превращается в "определённый".

Вот, скажем, формула арифметики:

$\forall x ~ S(x) \ne 0$.

Здесь встречается унарный функциональный символ $S$. Он "определённый" или нет? И если он "неопределённый", то что нужно добавить в формулу, чтобы он стал "определённым"?

migmit в сообщении #608521 писал(а):

Не совсем так. Аксиома индукции второго порядка вводит свободную переменную.

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

В отличие от схемы первого порядка, аксиома индукции второго порядка прямо говорит о ЛЮБЫХ свойствах. Вы не видите здесь никакой разницы?

migmit в сообщении #608521 писал(а):

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

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

[migmit]

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

Но любые символы констант (первого или второго рода) в определённые для них места можно подставлять.

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

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

Эти словеса - ещё далеко не формула.

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

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

Но тут-то Вы как раз и упустите момент, когда "неопределённый символ" превращается в "определённый".

Нет, почему же. Как раз-таки и поймаю.

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

Вот, скажем, формула арифметики:
$\forall x ~ S(x) \ne 0$.
Здесь встречается унарный функциональный символ $S$. Он "определённый" или нет? И если он "неопределённый", то что нужно добавить в формулу, чтобы он стал "определённым"?

В смысле? Если мы работаем в теории, содержащей такие константы, то вполне определённый. Но если её у нас нет - то он бессмысленный.

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

Какую свободную переменную? Аксиомы - это предложения языка (замкнутые формулы), а значит свободных переменных там уже нет.

Ну, подловили, оговорился. Квантифицированную.

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

В отличие от схемы первого порядка, аксиома индукции второго порядка прямо говорит о ЛЮБЫХ свойствах. Вы не видите здесь никакой разницы?

Не о свойствах, а о подмножествах. Или, что эквивалентно, предикатах. А не бессмысленных значках.

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

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

В этом языке слово "свойство" используется для разнообразия как синоним "предиката". А это совсем не то, что метаматематическое свойство.

[epros]

migmit в сообщении #608614 писал(а):

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

Почему же произвольный набор? Мы помним, что "всемогущий" - это константа второго порядка (или одноместный предикатный символ - кому как нравится).

migmit в сообщении #608614 писал(а):

В смысле? Если мы работаем в теории, содержащей такие константы, то вполне определённый. Но если её у нас нет - то он бессмысленный.

А откуда Вы знаете, в какой теории мы работаем? Скажем, если теория состоит из одной этой аксиомы, то символ $S$ уже можно считать "определённым"?

migmit в сообщении #608614 писал(а):

Не о свойствах, а о подмножествах. Или, что эквивалентно, предикатах. А не бессмысленных значках.

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

migmit в сообщении #608614 писал(а):

В этом языке слово "свойство" используется для разнообразия как синоним "предиката". А это совсем не то, что метаматематическое свойство.

Я не знаю, что Вы здесь имеете в виду под "метаматематическим свойством", но в языке логики второго порядка есть символы для переменных первого порядка (про которые удобно говорить, что они обозначают "объекты") и символы для переменных второго порядка (про которые удобно говорить, что они обозначают "свойства"). В логике первого порядка свойство невозможно обозначить символом переменной, только константой (это называется "предикатный символ").

P.S. Напомню, к чему это было сказано: В языке логики второго порядка можно без труда выразить утверждение, что "такое-то свойство существует" - чего не удастся сделать в логике первого порядка, ибо квантор существования на предикатные символы не ставится.

[migmit]

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

Мы помним, что "всемогущий" - это константа второго порядка (или одноместный предикатный символ - кому как нравится).

Это с чего бы???

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

А откуда Вы знаете, в какой теории мы работаем?

А это надо оговаривать до того, как работать.

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

Скажем, если теория состоит из одной этой аксиомы, то символ $S$ уже можно считать "определённым"?

Теория не может состоять из одной этой аксиомы. Теория должна включать, для начала, язык.

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

Не надо тащить сюда никакую семантику.

То есть?

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

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

Ну, и отлично. Всё равно произвольных значков там нет.

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

Я не знаю, что Вы здесь имете в виду под "метаматематическим свойством", но в языке логики второго порядка есть символы для переменных первого порядка (про которые удобно говорить, что они обозначают "объекты") и символы для переменных второго порядка (про которые удобно говорить, что они обозначают "свойства"). В логике первого порядка свойство невозможно обозначить символом переменной, только константой (это называется "предикатный символ").

И вы ещё обвиняете меня в том, что я тащу семантику.

[epros]

migmit в сообщении #608630 писал(а):

Это с чего бы???

Как приняли, так и есть. Число 777 может же быть константой в теории? Почему "всемогущий" не может?

migmit в сообщении #608630 писал(а):

А это надо оговаривать до того, как работать.

Неа. Ничего оговаривать не надо. Мы говорим только об отдельных предложениях языка. Это значит, что если там встречается константа, значит она есть в сигнатуре той теории "с которой мы работаем". Больше про эту теорию нам ничего не ведомо.

migmit в сообщении #608630 писал(а):

Теория не может состоять из одной этой аксиомы. Теория должна включать, для начала, язык.

Ой, ну не изображайте непонимание. Язык определён - это язык исчисления предикатов (пусть будет - второго порядка). И все логические аксиомы вместе с правилами вывода идут к нему в придачу. Но дополнительно к нему определена только вот эта одна аксиома.

migmit в сообщении #608630 писал(а):

Ну, и отлично. Всё равно произвольных значков там нет.

Значки для любых переменных второго порядка там есть.

migmit в сообщении #608630 писал(а):

И вы ещё обвиняете меня в том, что я тащу семантику.

А что не так? Я никакую семантику не тащу.

[migmit]

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

Как приняли, так и есть.

Ничего не понял. Кто принял, когда?

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

Число 777 может же быть константой в теории? Почему "всемогущий" не может?

Вообще-то, число 777 строится.

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

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

Не, не пойдёт. Если теория неизвестна, то работать не с чем. А если даже язык неизвестен, то синтаксическому анализатору нечего проверять.

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

Ой, ну не изображайте непонимание.

Седьмое правило демагога.

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

Язык определён - это язык исчисления предикатов (пусть будет - второго порядка).

Отлично. В нём константы "всемогущий" НЕТ.

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

И все логические аксиомы вместе с правилами вывода идут к нему в придачу. Но дополнительно к нему определена только вот эта одна аксиома.

Которая?

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

Значки для любых переменных второго порядка там есть.

Угу. Замечу, переменная не есть константа.

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

А что не так? Я никакую семантику не тащу.

Да нет, именно что тащите. "Свойство" - это, по-вашему, не семантика?

[epros]

migmit в сообщении #608672 писал(а):

Ничего не понял. Кто принял, когда?

Я. Уже много дней назад.

migmit в сообщении #608672 писал(а):

Вообще-то, число 777 строится.

Я не спрашивал строится оно или выращивается в оранжерее. Я спросил константа это или нет.

migmit в сообщении #608672 писал(а):

Не, не пойдёт. Если теория неизвестна, то работать не с чем. А если даже язык неизвестен, то синтаксическому анализатору нечего проверять.

Пурга, которую Вы сейчас несёте, воистину удивительна. Сами-то себя послушайте: Вы сейчас мне доказываете, что не можете проверить синтаксическую корректность предложения $\forall x ~ S(x)=0$, не имея всей теории целиком (а имея только язык).

(Оффтоп)

migmit в сообщении #608672 писал(а):

Седьмое правило демагога.

Нет, седьмое правило демагога — это после недели демагогических рассуждений обвинить оппонента в демагогии.

migmit в сообщении #608672 писал(а):

Да нет, именно что тащите. "Свойство" - это, по-вашему, не семантика?

Разумеется нет. Это просто слово, которым я называю то, что обозначается большими буковками в формулах.