Логика и методология математики.

[epros]

Феликс Шмидель в сообщении #944404 писал(а):

аксиомы логики высказываний являются несомненными и легко проверяются при помощи таблиц истинности.

Хм. А с моей точки зрения «таблицы истинности» более нуждаются в обосновании, чем большинство аксиом логики высказываний.

Феликс Шмидель в сообщении #944440 писал(а):

Логика первого порядка является стандартом благодаря своей простоте.
В ней нет аксиомных схем, поэтому её немного расширяют.
Более сложная логика с дополнительными правилами вывода не нужна для понимания оснований математики.

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

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

[Феликс Шмидель]

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

Итак, не могли бы Вы сформулировать, в чём заключается цель сего повествования? Просто решили озвучить для общественности свою точку зрения на то, что такое «логика» и почему логика первого порядка — самый правильный вариант логики?

Вовсе нет. Целью является объяснение оснований математики в простой и доступной форме неспециалисту в области математической логики. Представьте себе, что Вы пишите автономный учебник, допустим по алгебре.
В начале классического учебника Ван-Дер-Вардена написано:
"Так как в книге используются логические и общематематические понятия, не очень знакомые начинающему математику, то мы должны начать с посвящённого им короткого раздела. При этом мы не будем вдаваться в трудности, связанные с основаниями математики, а будем повсюду придерживаться "наивной точки зрения", избегая определений, содержащих порочный круг и приводящий к парадоксам."
Преставьте себе, что вместо этого Вы начинаете учебник с короткого объяснения оснований математики, включая начала логики и теории множеств.
Станете ли Вы погружать читателя в сложности логики второго порядка и теории моделей?
Или может быть Вы расскажете ему, что классическая логика высказываний не является единственно возможной и существуют системы логики, в которых нет закона исключения третьего?
Представьте себе, что перед тем как сформулировать аксиомы и аксиомные схемы теории множеств, Вы хотите объяснить читателю, что такое аксиома и аксиомная схема. Почему не определяется понятие $x \in y$ и что такое математическое определение.
Объяснение этих и других вопросов оснований математики и является целью "сего повествования".

[Феликс Шмидель]

Я переписал первый параграф:

Введение в математическую логику.

Математика занимается определением вводимых понятий, формулировкой утверждений и доказательством их истинности.
Доказательство это убедительное рассуждение, которое, при необходимости, можно перевести на формальный язык.
Формальный язык отличается от обычного тем, что существует автоматическая процедура (алгоритм), позволяющая проверять правильность записанного на этом языке математического текста.
Перевод математического текста на формальный язык редко осуществляется на практике, обычно достаточно понимания, что такой перевод возможен.
Математические доказательства основаны на логике, которая позволяет выводить одни утверждения из других.
Основное правило логического вывода называется Modus ponens, оно позволяет вывести истинность некоторого утверждения $\beta$ из истинности двух других утверждений $\alpha$ и "если $\alpha$, то $\beta$".
Примером применения правила Modus ponens является вывод утверждения:
"число 1001001 делится на 3" из утверждений: "сумма цифр числа 1001001 делится на 3" и "если сумма цифр числа 1001001 делится на 3, то число 1001001 делится на 3"
Правило Modus ponens применяют один или более раз, до тех пор, пока ни будет получено доказываемое утверждение.
Поскольку доказательство опирается на уже известные истины, то первоначальные истины доказать невозможно.
Утверждения, принимаемые за истину без доказательства, называются аксиомами.
Аксиомы не нуждаются в доказательстве по той причине, что они являются определением вводимых понятий и математических теорий в целом.
Например, стандартная теория арифметики определяется аксиомами Пеано, евклидова геометрия - аксиомами Евклида, а стандартная теория множеств - аксиомами Цермело-Френкеля.
Определение любой математической теории состоит из определения её понятий, которое даётся в форме аксиом.
Кроме правила Modus ponens, в логике есть и другие методы доказательства утверждений.
Например, метод доказательства от противного, в котором для доказательства некоторого утверждения предполагают обратное и из этого ложного обратного выводят абсурдное следствие.
Различные методы доказательства нуждаются в обосновании, для этого мы предлагаем следующую логическую систему.
В этой логической системе есть правило вывода Modus ponens и список логических аксиом.
Никаких других правил вывода и методов доказательства в этой логической системе нет.
Назовём такую логическую систему базовой логикой, а доказательства в ней - базовыми доказательствами.
Базовая логика является формальным языком, непригодным к практическому применению в математике, но удобным для обоснования различных методов доказательства.
Условием применимости любого метода доказательства является существование базового доказательства любого утверждения, доказанного этим методом.
Базовая логика близка к стандартному формальному математическому языку, который называется логикой первого порядка.
В логике первого порядка есть короткая форма записи утверждений, например, утверждение "для любого x: x=x" можно записать в короткой форме "x=x".
В логике первого порядка есть два правила вывода: Modus ponens и правило обобщения, которое позволяет из короткой формы утверждения "x=x" получить более длинную: "для любого x: x=x".
Из утверждения "для любого x: x=x" можно вывести утверждение "y=y", используя одну из аксиом и правило вывода Modus ponens.
Применяя к утверждению "y=y" правило обобщения, получим утверждение "для любого y: y=y".
В базовой логике есть утверждение "для любого x: x=x" из которого можно вывести утверждение "для любого y: y=y" используя аксиомы этой логики и правило вывода Modus ponens.
В логике первого порядка можно доказать те же утверждения, что и в базовой логике, поэтому проблемы обоснования логики первого порядка не возникает.
Логика первого порядка удобнее и является стандартом, поэтому мы будем пользоваться только этой логикой.
Изучением логики первого порядка и других формальных логических систем занимается особый раздел математики, который называется математической логикой.
Математическая логика также изучает вопросы непротиворечивости и полноты математических теорий.
Система аксиом математической теории (и сама теория) нызывается противоречивой, если в ней можно доказать некоторое утверждение $\alpha$ и его отрицание "не $\alpha$".
Система аксиом математической теории (и сама теория) называется полной, если любое утверждение теории можно или доказать или опровергнуть.
В идеале, система аксиом математической теории должна быть непротиворечивой и полной, но этот идеал недостижим.
Если теория достаточна для того, чтобы в ней можно было определить арифметику, то утверждение о непротиворечивости теории невозможно доказать в рамках этой теории.
Утверждение о непротиворечивости теории можно перевести на язык арифметики, и, в таком виде, оно не следует из аксиом теории.
Поэтому, если такая теория непротиворечива, то она не является полной.
Это доказал австрийский математик Курт Гёдель в 1931 году.
Из теорем Гёделя не следует, что нельзя доказать непротиворечивость арифметики никаким способом.
Доказательства непротиворечивости арифметики имеются в теории множеств.
Изучение математической логики не является целью этого введения.
У нас другая цель: объяснить основания математики в простой и доступной форме непрофессионалу.
Логика первого порядка подходит для этой цели, и мы не будем рассматривать более сложные логические системы.
Но логика первого порядка не отвечает на все вопросы, связанные с основаниями математики.
Она не объясняет как определяются математические теории, какие бывают виды аксиом и как даются математические определения.
Кроме этого, логика первого порядка недостаточна для формулировки стандартных математических теорий.
Поэтому логику первого порядка немного расширяют, и на её основе определяют формальный язык, у которого нет этих недостатков.
Примером такого формального математического языка является язык "Мицар".
Мы выделили этот язык из других формальных математических языков по двум причинам.
Во-первых, "Мицар" близок к обычному математическому языку и доказательства, написанные на этом языке можно читать без больших усилий.
Во-вторых, на этом языке написано большое количество доказательств, проверенных компьютером.
Вместе с тем у языка "Мицар" есть недостатки, и в будущем появятся гораздо более совершенные формальные математические языки.
Мы не будем заниматься изучением формального языка "Мицар" или ему подобных.
Для того, чтобы понимать как строится математический текст и как его, в принципе, можно формализовать не нужно детальное знание формального математического языка.
Принципы формальной логики можно объяснить на примерах, используя для этого обычный математический язык.
Кроме логики в основании математики лежит теория множеств, без которой не обходится ни один раздел современной математики.
Поэтому логику и теорию множеств часто формулируют вместе.
Мы предпочитаем сначала объяснить логику и принципы построения математических теорий.
Теория множеств не рассматривается в этом введении.

[epros]

Феликс Шмидель в сообщении #946366 писал(а):

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

Популяризация с целью привлечения интереса к матлогике широкой общественности? Или всё-таки учебник? Для какого начального уровня и чему в конечном итоге хотите научить?

Это я к тому, что из Вашего текста это непонятно. С одной стороны, всё известные вещи рассказываете, которые в любом учебнике есть. Хотя терминология у Вас не везде стандартная. С другой стороны — язык не настолько художественный и доходчивый, чтобы широкую публику привлечь. Вашему потенциальному читателю может лучше просто Мендельсона открыть? э

Феликс Шмидель в сообщении #946366 писал(а):

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

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

А вот со схемами интереснее. Извините уж, не найду где у Вас об этом сказано. Не подскажете? Особенно интересно как Вы объясняете
1) зачем нужны схемы
2) и как они формализуются

[Феликс Шмидель]

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

Популяризация с целью привлечения интереса к матлогике широкой общественности? Или всё-таки учебник? Для какого начального уровня и чему в конечном итоге хотите научить?

Учебник по какому-нибудь предмету, содержащий все необходимые для изложения сведения.
Для того же начального уровня, что и книга Ван-Дер-Вардена, то есть для начинающих.
Научить излагаемому предмету и точному определению всех используемых понятий.

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

С одной стороны, всё известные вещи рассказываете, которые в любом учебнике есть. Хотя терминология у Вас не везде стандартная. С другой стороны — язык не настолько художественный и доходчивый, чтобы широкую публику привлечь. Вашему потенциальному читателю может лучше просто Мендельсона открыть?

Зачем изучающему какой-либо предмет читать 300 страниц текста по математической логике?

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

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

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

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

А вот со схемами интереснее. Извините уж, не найду где у Вас об этом сказано. Не подскажете? Особенно интересно как Вы объясняете
1) зачем нужны схемы
2) и как они формализуются

Феликс Шмидель в сообщении #943498 писал(а):

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

Таким образом, аксиомная схема порождает бесконечное множество аксиом.

Например, выражение "если $x=y$ то $\alpha(x) \Longleftrightarrow \alpha(y)$" с предикатной переменной $\alpha(x)$ является аксиомной схемой.

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

[Феликс Шмидель]

Уважаемый arseniiv, я убедился, что все или почти все Ваши критические замечания правильны.
Я работаю над исправлением текста, ещё раз спасибо.
Я выложил первый параграф с исправлениями, по-моему только ссылка на теоремы Гёделя осталась неисправленной.
Буду благодарен если Вы его покритикуете.

Я также исправил следующее место, в соответствии с Вашими замечаниями:

Цитата:

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

Первоначальным понятиям даётся интуитивное и аксиоматическое определение.
Интуитивное определение описывает смысл первоначальных понятий и их свойства, лежащие в основе аксиоматического определения.
Аксиоматическое определение первоначальных понятий даётся в форме аксиом.

Любые математические понятия (как первоначальные, так и непервоначальные) имеют тип объекта или утверждения и записываются с использованием переменных.
Например, понятие "$x+y$" имеет тип объекта, а понятие "$x=y$ имеет тип утверждения.
Переменные тоже имеют тип объекта или утверждения, в частности в приведённых понятиях, $x$ и $y$ - переменные типа объекта.
Переменные объекты обозначаются латинскими буквами, возможно с индексами, например $x, y, z, X, Y, Z, x_1, y_2, z_3$.
Переменные утверждения обозначаются по-разному, здесь они обозначаются греческими буквами, например, $\alpha, \beta$.

Если что-то не так, буду благодарен, если укажите.

[epros]

Феликс Шмидель в сообщении #946641 писал(а):

Зачем изучающему какой-либо предмет читать 300 страниц текста по математической логике?

Т.е. Вы ориентируетесь на такого читателя, для которого 300 страниц — это много? А Вам не кажется, что такой человек скорее предпочтёт прочесть статью википедии про логику первого порядка?

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

Феликс Шмидель в сообщении #946641 писал(а):

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

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

Феликс Шмидель в сообщении #946641 писал(а):

и что определение любого понятия выражается аксиомой?

А вот этот тезис (про то, как формализуются определения), как мне кажется, Вы высказали, но недостаточно раскрыли. Потому что бывают «явные» определения, когда вновь введённому предикатному символу сопоставляется формула:
$isEven(x) \leftrightarrow \exists y \, y \times 2 = x$
и «неявные», когда ни в одной аксиоме определяемый термин не присутствует. Например, натуральные числа определяются аксиоматикой Пеано, в которой, записанной на формальном языке, слова «натуральное число» не звучат.

Феликс Шмидель в сообщении #946641 писал(а):

Феликс Шмидель в сообщении #943498 писал(а):

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

Таким образом, аксиомная схема порождает бесконечное множество аксиом.

Например, выражение "если $x=y$ то $\alpha(x) \Longleftrightarrow \alpha(y)$" с предикатной переменной $\alpha(x)$ является аксиомной схемой.

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

Мне кажется, что Вы объясняете то, что и так ясно, но умалчиваете о том, что может вызывать вопросы. В данном случае Вы рассказали о том, как нужная Вам вещь формализуется в языке логики второго порядка (ибо неявно предполагается квантор всеобщности по предикату $\alpha$), но ничего не сказали о том, откуда, собственно, возьмётся схема. Это ведь беконечное множество аксиом. А что если читатель спросит: «Вы с ума сошли, как Вы собираетесь записывать бесконечное множество аксиом»?

[arseniiv]

(Оффтоп)

Феликс Шмидель в сообщении #946668 писал(а):

Буду благодарен если Вы его покритикуете.

Хочу честно сказать, что пока лень. Всё-таки тема теперь уже и не так безлюдна…

-- Пн дек 15, 2014 19:12:11 --

Феликс Шмидель в сообщении #946641 писал(а):

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

Опять же, это всё вещи в какой-то степени относительные:
• Можно исключить все аксиомы-формулы, вместо этого используя правила вывода вида $\frac{}{\text{аксиома}}$. Да и даже если не делать так, то то, что аксиома выводима, следует из того же, из чего следует выводимость любой другой теоремы — наличия вывода. А то, что аксиомы в выводе могут появляться ex nihilo, это вещь отдельная, несмотря на то что до выводимости аксиомы от неё один шаг.
• Определения можно рассматривать исключительно как синтаксические замены. То, что обычно хватает таких определений, которые выражаются в добавлении функционального/предикатного символа и соответствующей аксиомы — отдельная вещь.

Феликс Шмидель в сообщении #946641 писал(а):

Зачем изучающему какой-либо предмет читать 300 страниц текста по математической логике?

Может быть, и минимум в 50—80 страниц достижим. А вот даже десятка будет мало. Надо сформировать mindset; надо привести объяснения текущего положения дел, которое описывается; надо разобрать детали.

-- Пн дек 15, 2014 19:16:37 --

Грубо говоря, вам надо совместить в одном тексте четыре: «в чём дело», «что это значит», «как так вышло» и «а как могло бы выйти», иначе понимания не будет. Вы пока ограничиваетесь только первой четвертью.

-- Пн дек 15, 2014 19:19:18 --

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

[Феликс Шмидель]

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

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

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

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

Т.е. Вы ориентируетесь на такого читателя, для которого 300 страниц — это много? А Вам не кажется, что такой человек скорее предпочтёт прочесть статью википедии про логику первого порядка?

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

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

Может быть, и минимум в 50—80 страниц достижим. А вот даже десятка будет мало. Надо сформировать mindset; надо привести объяснения текущего положения дел, которое описывается; надо разобрать детали.

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

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

А вот этот тезис (про то, как формализуются определения), как мне кажется, Вы высказали, но недостаточно раскрыли. Потому что бывают «явные» определения, когда вновь введённому предикатному символу сопоставляется формула:
$isEven(x) \leftrightarrow \exists y \, y \times 2 = x$
и «неявные», когда ни в одной аксиоме определяемый термин не присутствует. Например, натуральные числа определяются аксиоматикой Пеано, в которой, записанной на формальном языке, слова «натуральное число» не звучат.

Как раз у меня это определение возможно: вводим первоначальные понятия натурального числа, единицы, сложения и умножения двух натуральных чисел, затем определяем эти первоначальные понятия системой аксиом Пеано.

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

Мне кажется, что Вы объясняете то, что и так ясно, но умалчиваете о том, что может вызывать вопросы. В данном случае Вы рассказали о том, как нужная Вам вещь формализуется в языке логики второго порядка (ибо неявно предполагается квантор всеобщности по предикату $\alpha$), но ничего не сказали о том, откуда, собственно, возьмётся схема. Это ведь беконечное множество аксиом. А что если читатель спросит: «Вы с ума сошли, как Вы собираетесь записывать бесконечное множество аксиом»?

Никакого квантора всеобщности по предикату $\alpha$ не предполагается. Моё введение, как и формальный язык "Мицар" основан на расширенной логике первого порядка, в которой предикатные переменные не связываются кванторами. Что странного в том, что при замене предикатного переменного предикатами получается бесконечное множество аксиом? Это общепринятый в математике способ задания бесконечного множества аксиом аксиомными схемами.

[epros]

Феликс Шмидель в сообщении #947352 писал(а):

Как раз у меня это определение возможно: вводим первоначальные понятия натурального числа, единицы, сложения и умножения двух натуральных чисел, затем определяем эти первоначальные понятия системой аксиом Пеано.

Т. е. Вы именуете «первоначальными» именно те понятия, для которых в языке формальной теории не введён термин (обычно говорят: «символ»)? Просто это как-то явно не прозвучало. Кстати, единица, сложение и умножение явно определены в языке арифметики Пеано (а вот «натуральное число» — нет).

Феликс Шмидель в сообщении #947352 писал(а):

Никакого квантора всеобщности по предикату $\alpha$ не предполагается. Моё введение, как и формальный язык "Мицар" основан на расширенной логике первого порядка, в которой предикатные переменные не связываются кванторами.

Я не знаю что такое Мицар, но то, что Вы сказали про $\alpha$, предложением логики первого порядка не формализуется (только второго). Именно потому, что утверждение должно распространяться на «все $\alpha$». Используется ли при этом значок $\forall$ или предложение формализуется в бескванторной записи — несущественно.

Феликс Шмидель в сообщении #947352 писал(а):

Что странного в том, что при замене предикатного переменного предикатами получается бесконечное множество аксиом?

Опять же, обратите внимание, что в логике первого порядка нет предикатных переменных. И на что Вы собрались заменять переменную? На константу? Для этого нужно в языке теории определить символы для ВСЕХ предикатных констант, которые Вы собираетесь использовать. Короче, схема аксиом формализуется не так.

Феликс Шмидель в сообщении #947352 писал(а):

Это общепринятый в математике способ задания бесконечного множества аксиом аксиомными схемами.

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

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

[vicvolf]

epros писал(а):

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

Согласен с Вами. Наверно автор просто хочет сам разобраться в этом вопросе. Но тогда так и надо писать - помогите разобраться. Это не дискуссионная тема, так как нет предмета для обсуждения.

[Феликс Шмидель]

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

[Xaositect]

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

[epros]

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

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

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

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

[Феликс Шмидель]

Я полностью согласен с тем, что написал уважаемый Xaositect.
В моём тексте сказано:

Феликс Шмидель в сообщении #943498 писал(а):

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

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

Цитата:

Феликс Шмидель, обратите внимание, что вместо метапеременной здесь подставляется не предикат (как Вы сказали), а синтаксически правильная формула в языке теории.

В моём тексте сказано:

Феликс Шмидель в сообщении #943498 писал(а):

Математические утверждения со свободными объектными переменными называются предикатами.

На формальном языке предикат и есть "синтаксически правильная формула в языке теории".
Я не понимаю, в чём разница.

vicvolf в сообщении #947501 писал(а):

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

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