формальные системы с усложняющейся грамматикой

[Padawan]

Бывают ли (в смысле описаны ли в литературе) формальные системы, в которых формальный вывод может включать в себя введение новых правил вывода, которые используются далее?

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

[Xaositect]

Не встречал ничего, кроме кратких (или не очень кратких) упоминаний о том, что каждое доказанное утверждение вида $\Gamma\vdash \Phi$ порождает правило вывода, которое, если добавить его к системе, не дает ничего нового. Или тому подобные утверждений.

[Padawan]

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

[Xaositect]

Padawan в сообщении #282687 писал(а):

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

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

[AD]

Padawan в сообщении #282687 писал(а):

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

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

(это у меня не авторитетный ответ - так, самому интересно)

[AGu]

AD в сообщении #282773 писал(а):

Padawan в сообщении #282687 писал(а):

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

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

Введение новых понятий можно формализовать с помощью теории
формальных языков как расширение синтаксиса, снабженное семантикой,
т.е. правилами перевода формул с расширенного языка на исходный.
(Особенно легко и адекватно практике расширение синтаксиса производится
для контекстно свободных языков — путем расширения набора продукций.)

В подавляющем большинстве случаев определения действительно
являются всего лишь удобными сокращениями, но это не всегда так.
Есть по крайней мере два вида особых случаев:

(1) определение «несуществующего» терма, т.е. такого терма $T$,
что формула $(\exists\,x)(x=T)$ не выводима в рассматриваемой теории;

(2) синтаксически рекурсивное определение.

Пример случая (1): определение терма $\mathbb V$ («класс всех множеств»)
в ZFC с семантическим правилом $(x\in\mathbb V):=(x=x)$.

Пример случая (2): классическое определение формулы
$M\vDash\varphi$ («$\varphi$ истинна во внутренней модели $M$»)
рекурсией по сложности формулы $\varphi$.

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

[Padawan]

AD в сообщении #282773 писал(а):

Padawan в сообщении #282687 писал(а):

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

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

(это у меня не авторитетный ответ - так, самому интересно)

Тогда вся математика - чисто лингвистический акт Ну с точки зрении теории формальных систем так оно и получается

AGu в сообщении #282893 писал(а):

(1) определение «несуществующего» терма, т.е. такого терма $T$,
что формула $(\exists\,x)(x=T)$ не выводима в рассматриваемой теории;

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

Такой немного философский вопрос: чего же мы достигаем введением новых понятий? Неужели только лишь сокращения записи? Или в этом есть и более глубокий смысл?

-- Сб янв 23, 2010 20:42:05 --

AGu в сообщении #282893 писал(а):

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

Красиво

[AD]

Padawan в сообщении #283025 писал(а):

Тогда вся математика - чисто лингвистический акт Ну с точки зрении теории формальных систем так оно и получается

Да нет вроде Ну есть соревнование кто самое красивое предложение запишет на языке, а есть упрощение записи этих предложений. Первое - математика, второе - определения

-- Сб янв 23, 2010 22:55:46 --

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

(Оффтоп)

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

[Padawan]

AD в сообщении #283075 писал(а):

Ну есть соревнование кто самое красивое предложение запишет на языке, а есть упрощение записи этих предложений. Первое - математика, второе - определения

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

(Оффтоп)

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

[AGu]

Padawan в сообщении #283025 писал(а):

AGu в сообщении #282893 писал(а):

(1) определение «несуществующего» терма, т.е. такого терма $T$,
что формула $(\exists\,x)(x=T)$ не выводима в рассматриваемой теории;

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

Не-не, ни в коем случае! Никаких «новых аксиом» и ничего «существенно нового»! Иначе это уже будут не «определения». К примеру, введение терма $\mathbb V$ вовсе не предполагает какое-либо изменение аксиоматики. Мы всего лишь расширяем синтаксис новым термом $\mathbb V$ и используем его наряду со старыми термами самым обычным образом, подразумевая семантику $(x\in\mathbb V):=(x=x)$. При этом формула, содержащая новый терм, считается теоремой в том и только том случае, когда теоремой является ее перевод на исходный язык. В этом смысле ничего «существенно нового» не появляется. Например, формула $(\forall\,x)(x\in\mathbb V)$ является теоремой, так как ее перевод имеет вид $(\forall\,x)(x=x)$ и, разумеется, доказуем.

Кстати, работая в ZFC, бывает очень удобно перемещать аксиому экстенсиональности на уровень синтаксиса и считать формулу $S=T$ (где $S$ и $T$ — термы) сокращением формулы $(\forall\,y)(y\in S\Leftrightarrow y\in T)$. Кое-кто так и поступает. Это действительно удобный прием, так как он приводит к существенной технической экономии (за счет упрощения сигнатуры и сокращения множеств атомарных формул, аксиом и правил вывода), тем не менее сохраняя в неизменном виде множество теорем. При таком подходе, например, формула $(\exists\,x)(x=\mathbb V)$ теоремой не является. Более того, теоремой является ее отрицание $\neg(\exists\,x)(x=\mathbb V)$: действительно, перевод этой формулы с учетом сокращения $(x=\mathbb V):=(\forall\,y)(y\in x\Leftrightarrow y\in\mathbb V)$ имеет вид $\neg(\exists\,x)(\forall\,y)(y\in x\Leftrightarrow y=y)$ или, что эквивалентно, $\neg(\exists\,x)(\forall\,y)(y\in x)$, а последнее доказуемо в ZFC.

Padawan в сообщении #283025 писал(а):

Такой немного философский вопрос: чего же мы достигаем введением новых понятий? Неужели только лишь сокращения записи? Или в этом есть и более глубокий смысл?

Как я уже говорил, в большинстве случаев это всего лишь сокращение. Случай $\mathbb V$ — это на самом деле тоже сокращение, но не сводящееся к добавлению определимой (по Бету) константы. А вот $M\vDash\varphi$ — это уже не просто сокращение. Это, если угодно, схема сокращений: каждая формула вида $M\vDash\varphi$ является сокращением соответствующей формулы, получаемой из $M\vDash\varphi$ в результате применения алгоритма перевода, раскрывающего рекурсию по сложности $\varphi$. Но если отвлечься от такого рода нюансов и придать термину «сокращение» более общий смысл, — считая раскрытие сокращения алгоритмом перевода формулы с расширенного языка на исходный, — то всякое определение является сокращением. Никакого более глубоко смысла тут нет. И это хорошо, ибо согласуется с интуитивным пониманием определения как введения новой записи для какого-либо утверждения или терма. Чистой воды прагматизм и никакой философии.

AD в сообщении #283075 писал(а):

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

Нет, так как аксиома — это не определение. Упоминая аксиому пустого множества, Вы, возможно, имели в виду определение пустого множества, т.е. расширение синтаксиса термом $\varnothing$ с семантикой $(x\in\varnothing):=(x\ne x)$. Это уже определение, но оно все равно не относится к случаю (1), так как формула $(\exists\,x)(x=\varnothing)$ является теоремой, т.е. мы вводим «существующий» терм. (Что же касается аксиомы бесконечности, то тут я даже отдаленной аналогии с определением не вижу.)

[AD]

Тема перемещена в дискуссионный раздел по просьбе автора.

[vek88]

Padawan в сообщении #282639 писал(а):

Бывают ли (в смысле описаны ли в литературе) формальные системы, в которых формальный вывод может включать в себя введение новых правил вывода, которые используются далее?

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

Может быть Вам будет полезна книжка "Представление в ЭВМ неформальных процедур" (дайте поиск в Яндексе)? Тематика книги где-то на стыке искусственного интеллекта, математической логики и логического программирования. Там была сделана попытка автоматизировать "развитие" формальной системы. Кроме того, дано нефинитное обобщение канонических систем (исчислений) Поста.

[Профессор Снэйп]

Мы вот в арифметике Пеано получаем утверждение, истинное на $\mathbb{N}$ (конечно при условии, что непротиворечива сама арифметика, но это вроде можно счесть самоочевидным), но не доказуемое в этой арифметике. Но оно ведь истинно! Но его вывод невозможен. Значит, надо добавить новое правило вывода для него.

С получившийся системой можно проделать ту же процедуру. И так далее, по конструктивным ординалам...

Наверное, топикстартер имел в виду нечто подобное.

-- Вс янв 31, 2010 10:44:06 --

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

[AGu]

Профессор Снэйп в сообщении #284700 писал(а):

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

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

Итак, для каждого нетерминала $N$ добавим новый терминал $N'$.
(Тем самым для стартового нетерминала $S$ тоже добавляется $S'$.)
Неформально слово $N'w$ считается кодом правила $N\to w$.

Идея — консервативно расширить обобщенную грамматику так,
чтобы обобщенная выводимость $N\Rrightarrow^+ w$
была равносильна обычной выводимости $S\Rightarrow^+ N'w$.

Для каждого правила $N\to w$ добавим правило $S\to N'w$.
Добавим также правила $N\to N'$ и $S\to N'N$.
Может, еще что-нибудь этакое добавить, не знаю, а может, и этого хватит.
Возможно, подобного рода извратами, можно расширить грамматику
так, что расширенная грамматика уже будет «самоописывающей»
(т.е. будет удовлетворять написанному выше), а также будет
консервативным расширением обобщенной исходной
(т.е. обобщенно выводимые в ней слова, составленные их старых символов,
будут обычно выводимы в старой грамматике).

P.S. Кстати, появление новых терминалов мешать не будет, так как
их можно удалить из расширенного контекстно-свободного языка
путем пересечения с (регулярным) языком всех слов старого алфавита,
тем самым вновь получив контекстно-свободный язык.

[vek88]

vek88 в сообщении #283476 писал(а):

Padawan в сообщении #282639 писал(а):

Бывают ли (в смысле описаны ли в литературе) формальные системы, в которых формальный вывод может включать в себя введение новых правил вывода, которые используются далее?

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

Может быть Вам будет полезна книжка "Представление в ЭВМ неформальных процедур" (дайте поиск в Яндексе)? Тематика книги где-то на стыке искусственного интеллекта, математической логики и логического программирования. Там была сделана попытка автоматизировать "развитие" формальной системы. Кроме того, дано нефинитное обобщение канонических систем (исчислений) Поста.

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

1. За основу представления теории берется нефинитная формальная система (К-система).

2. Рассмотрение ограничивается классом полных К-систем (т.е. все теоремы теории либо истинны, либо ложны).

3. В рамках полных К-систем теории могут достраиваться новыми правилами, знаками (константами) и пременными.

4. Единственное ограничение - при расширении теории должна сохраняться полнота.

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