Полнота языков

[Krepko]

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

(Оффтоп)

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

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

1). Можно ли считать грамматику формальной системой ?
Думаю да, т.к. ее можно переписать в терминах обычных математических теорий (теории множеств, арифметики).
Попробую описать такую теорию на примере арифметики Пеано.
Объектами теории будем считать не натуральные числа, а символы из алфавита формальной грамматики (или конечное множество натуральных чисел им сопоставленных).
Аксиомами определим свойства этих символов и их сочетаний, или сопоставленных им натуральных чисел (естественно эти свойства не часто будут совпадать со свойствами натуральных чисел в арифметике).
Например, введем две аксиомы $1 \in U ; x \in U \rightarrow S(x) \in U$, где под единицей понимается первый символ терминального алфавита арифметики (далее под арифметикой понимается: аксиомы арифметики Пеано, логика предикатов, правила вывода), под $U$ понимается множество всех грамматически правильных предложений языка арифметики, под $x$ понимается любой объект теории (начиная с терминальных символов). $S(x)$ определяет следующее слово из предыдущего. В данном примере достаточно считать, что этот способ есть (если нужно буквально пусть это добавление пары скобок и символа S), но в целом придется описать аксиомами каждое порождающее правило формальной грамматики.
Правилами формального вывода укажем способы доказательства в нашей теории утверждений о том, является ли произвольное сочетание символов из алфавита грамматически корректной конструкцией (словом арифметики). В некотором смысле доказательства таких теорем можно считать аналитическими правилами грамматики, а сами теоремы порождающими правилами.
Так например, истинность гипотезы о грамматической корректности утверждения: "количество пар простых чисел бесконечно" (естественно на языке арифметики), доказывается в теории путем применения правил вывода. В то время, как само это утверждение может быть порождено аксиомами теории (а может и не быть).

2). Может ли формальная система представляющая грамматику быть неполной ?
Думаю да, т.к. формальная система может быть теорией, включающей арифметику. Эта теория как минимум включает в себя натуральные числа, т.к. все утверждения арифметики о натуральных числах должны быть корректными грамматически. Любое натуральное число в арифметике в простейшем случае представлено набором цифр или последовательностью $S(S(…))$). Последовательности таких слов арифметики соответствует последовательность теорем грамматики об их синтаксической корректности. Т.к. формальная теория (грамматики) может включать в себя арифметику, следовательно к ней применима теорема Геделя о неполноте формальных систем.

3). Как интерпретировать существование Геделевских предложений в формальной системе грамматики и можно ли привести пример ?
Интерпретировать можно следующим образом. Существуют формулы в алфавите арифметики, грамматическую корректность которых (принадлежность к языку арифметики) нельзя ни доказать ни опровергнуть. Привести пример затрудняюсь.

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

[mihaild]

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

Утверждение о том, что данная строка невыводима в данной грамматике уже принадлежит не теории грамматики, а какой-то метатеории (например, арифметике Пеано). И тут вопрос в том, какая у нас была изначально теория, и какая метатеория. Если скажем метатеория не слабее арифметики Пеано, а грамматика хотя бы контекстно-зависимая - то для каждого слова метатеория сможет доказать или опровергнуть его выводимость в грамматике. Если грамматика произвольная типа 0, а метатеория перечислима, то могут найтись слова, про которые метатеория не может сказать, выводятся они или нет (более точно: для каждой метатеории найдется такая грамматика и слово).

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

[Krepko]

mihaild в сообщении #1349097 писал(а):

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

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

mihaild в сообщении #1349097 писал(а):

Утверждение о том, что данная строка невыводима в данной грамматике уже принадлежит не теории грамматики, а какой-то метатеории (например, арифметике Пеано).

Еще раз попробую про велосипед, чтобы обозначить разногласия. Дан терминальный алфавит, условной арифметики <символы используемые в этой арифметике>. Множество всевозможных строк из этого алфавита, большая часть из которых абракадабра. Дан нетерминальный алфавит и правила вывода, собственно грамматика. Она порождает (или выделяет) из множества всевозможных строк терминального алфавита грамматические верные. Эти строки исключительно из терминальных символов алфавита, образуют множество синтаксически корректных формул данной арифметики. В арифметике эти формулы выражают свойства натуральных чисел, например: "существует единица, за единицей следует следующая $S(S(1))$, или в расширенном виде $1+1=7$". Арифметика в свою очередь выделяет из множества этих всевозможных грамматически верных формул доказуемые (истинные), т.е. определяет истинность или ложность этих формул, т.к. для арифметики это утверждения о натуральных числах.
Утверждение о том, что данная строка не выводима в данной грамматике, я понимаю как невозможность вывода данной строки терминальных символов, используя нетерминальный алфавит и правила вывода грамматики.

mihaild в сообщении #1349097 писал(а):

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

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

[mihaild]

Krepko в сообщении #1349139 писал(а):

Все строки в алфавите грамматики - это ведь не множество всевозможных строк данного алфавита ?

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

Krepko в сообщении #1349139 писал(а):

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

Я вроде бы вас так и понял.

Утверждение о том, что данная строка не выводима в грамматике - это уже утверждение в какой-то другой теории (метатеории, в которой мы и формализовывали грамматику).

Krepko в сообщении #1349139 писал(а):

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

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

[Soul Friend]

(Оффтоп)

скажем, что любой язык начинается с алфавита, где $n$ количество букв в языке, далее метатеория устанавливает для языка какие буквы можно связывать друг с другом в зависимости от количества букв в слове, то есть отсеивает некоторые перестановки букв $x_i$ в слове длинной $y$. После, метатеория устанавливает другое правило, для оставшихся слов после первого правила, какие слова можно связывать друг с другом, и как, в предложениях длинной в $z$. Имея полный словарь языка, можно переходить сразу ко второму правилу, то есть к синтаксису языка, после которой следует пунктуация.

[Krepko]

mihaild в сообщении #1349143 писал(а):

Все.

Все таки я уточню для полного понимания на примере.
$\{(,),…\}$ - алфавит терминальных символов (используется для строк (формул) предметной теории, в нашем случае арифметики)
$\{parenthesis,…\}$ - алфавит нетерминальных символов грамматики (в предметной теории не используется)
Правила вывода:
$1.parenthesis\to (parenthesis)$
$2.parenthesis\to ()$
…
Докажем, что строка $(())$ выводима в грамматике.
$parenthesis\to (parenthesis)$
$(parenthesis)\to ((parenthesis))$
$((parenthesis))\to (())$
$(())$ - формула арифметики
.
Т.е. из всевозможных строк состоящих только из открывающих и закрывающих скобок, грамматика выделяет(порождает) только строки с парными скобками. К примеру, строка $(()$ не является формулой арифметики, нельзя определять истинна она или ложна применительно к натуральным числам. Хотя она и входит в множество «все» (всевозможные строки в алфавите арифметики $\{(,),…\}$).

Как то мое «все» и Ваше «все» не совпадают.

mihaild в сообщении #1349143 писал(а):

Утверждение о том, что данная строка не выводима в грамматике - это уже утверждение в какой-то другой теории (метатеории, в которой мы и формализовывали грамматику).

То что я написал в начале ответа можно считать формализацией грамматики ? Этот алфавит, правила вывода, доказательство выводимости строки $(())$ - это грамматика или метатеория об этой грамматике ?

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

mihaild в сообщении #1349143 писал(а):

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

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

[iifat]

Вы таки тщательно избегаете ответа на буквально первый вопрос:

mihaild в сообщении #1349097 писал(а):

Пока что непонятно, что вы хотите сделать

Замечу в скобках, что теорема Гёделя, помнится, таки как-то ограничивает исходную систему аксиом.

Krepko в сообщении #1349188 писал(а):

можно считать формализацией грамматики? Этот алфавит, правила вывода, доказательство выводимости строки $(())$ - это грамматика или метатеория об этой грамматике?

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

[mihaild]

Krepko в сообщении #1349188 писал(а):

Как то мое «все» и Ваше «все» не совпадают.

Формулы грамматики и формулы арифметики - это разные множества. Формулы грамматики - это то, про что можно спрашивать, выводятся ли они в грамматике. Формулы арифметики - это то, что в грамматике выводится ("теоремы" грамматики).

Krepko в сообщении #1349188 писал(а):

Этот алфавит, правила вывода, доказательство выводимости строки $(())$ - это грамматика или метатеория об этой грамматике ?

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

Krepko в сообщении #1349188 писал(а):

Но Вы имеете в виду кодировку элементов множества формул (уже готовых - Ваше «все»), а не кодировку множества всевозможных строк из алфавита (мое «все»).

Нет, я имею в виду кодировку всех строк в арифметической сигнатуре.

[epros]

mihaild в сообщении #1349097 писал(а):

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

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

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

[mihaild]

epros, согласен, бред сказал.