Тема 6. Формальные теории
предназначены для четкого изложения и развития тех или иных отраслей человеческих знаний. Задать формальную теорию – значит задать ее функциональные и предикатные символы, а также аксиомы, т. е. некоторые из высказываний, которые являются истинными в данной отрасли знаний. Развивать формальную теорию – значит пополнять запас ее теорем, т. е. таких высказываний, которые являются логическими следствиями аксиом. Изложение любой формальной теории в принципе можно оформить в виде книжек с доказательными текстами:
Здесь штрих-пунктирная линия обозначает пояснение о том, с помощью какого правила порождения получено соответствующее знакосочетание. Для удобства таких пояснений знакосочетания a1,…, tn нумеруются последовательно от 1 до k+е+m+n. Вспомним, что правила порождения теорем являются правилами вывода, что конечная индуктивная последовательность теорем является доказательством и что следующие девять правил, называемых основными, образуют достаточный набор правил вывода из аксиом: правила тавтологии, отделения, обобщения, подтверждения, общевнесения, сущевнесения, тождества, равенства, неотличимости. Такая форма изложения делает доказательство легко проверяемым, но практически не применяется из-за ее громоздкости. Способы более компактного изложения формальной теории. 1. Последовательность a1,…, re не записывается, потому что при достаточном навыке термы и формулы распознаются без построения их индуктивных последовательностей. 2. В последовательность t1,…, tn включаются теоремы из других доказательных текстов. 3. Для двухместного функционального или предикатного знака v используется операционная форма записи: вместо v(a,b) пишут (a)v(b). 4. При операционной форме записи принимается соглашение об упразднении некоторых пар скобок в соответствии с соглашением об убывании силы связи в последовательности: одноместный функциональный знак, двухместный функциональный знак, одноместный предикатный знак, двухместный предикатный знак, логический знак. 5. Используются специальные начертания для функциональных и предикатных знаков. Например в теории чисел: 0, 1, 2, 3 - нульместные функциональные знаки; Ö, sin, cos - одноместные функциональные знаки; +, -, ´, /, - двухместные функциональные знаки; <, >, £, ³ - двухместные предикатные знаки. 6. Используются знаковые фигуры. Например, åх=3х обозначает сумму 3+4+5. 7. Вводится определяющая аксиома g(х1,...,х11)Û р для нового n-местного предикатного символа g. Здесь переменные х1,...,хn попарно различны, а высказывание р не имеет свободных вхождений переменных, отличных от х1,...,хn. 8. Вводится определяющая аксиома р{х, ¦( х1,...,хn)} для нового n - местного функционального символа ¦ в тех случаях, когда формула $рх является теоремой. Здесь переменные х, х1,...,хn попарно различны, а р не имеет свободное вхождение переменных, отличных от х, х1,...,хn.
Теорема об определениях: если теория Т2 получена из теории Т1 путем добавления определяющей аксиомы для нового функционального или предикатного символа v то для каждой теоремы теории Т2 существует равносильная ей теорема теории Т1.
9. Кроме девяти основных применяются дополнительные правила вывода, например правило отделения конъюнкта D pÙg, р и правило присоединения дизъюнкта Dр, pÚg. 10. Применяются известные методы доказательства. Обоснование таких методов дается в учебниках логики. Например метод доказательства от противного основан на следующей теореме.
Теорема о доказательстве методом от противного: если формальная теория Т2 получена путем добавления аксиомы Øр к аксиомам теории Т1 и если формулы q, Øq являются теоремами теории Т2, то формула р является теоремой теории Т1.
Формальная арифметика формализует систему знаний о целых неотрицательных числах, использует в качестве исходных четыре функциональных и два предикатных знака
интерпретируемых в соответствии с их известными со школы специальными начертаниями, имеет такие аксиомы Ø1=0 х + 1= y + Þ x = y x + 0 = x x + (y + 1) = (x + y) + 1 x×0 = 0 x×(y + 1) = x×y + x Øx < 0 x < y + 1 Û x < y Ú x = y p íx, 0ýÚ"(pÞíx, x + 1ý)Þ p
Здесь при записи аксиом использованы ранее перечисленные соглашения о компактизации изложения и известное соглашение о том, что знак умножения связывает сильнее знака сложения. Если такие соглашения не принимать, то к примеру первую аксиому следовало бы записать в виде Ø(g (¦ ,¦ )).
Пример определяющих аксиом для новых нульместных функциональных знаков 2, 3, 4, 5 и новых двухместных предикатных знаков >, £ ,³ ,¹ :
Заметим, что знак < можно было бы не включать в перечень исходных знаков формальной арифметики, а ввести его с помощью определяющей аксиомы c1<c2 Û $c3(Øc3 = 0 Ù c1+ c3 = c2). Пример доказательного текста в формальной арифметике (k = 3, е = 6, m = 1, n = 3):
Компактизированный текст:
Словесный вариант: «Если единица не равна нулю, то тем самым существует не равное нулю число. Но единица не равна нулю. Следовательно, существует число, не равное нулю».
Популярное: Организация как механизм и форма жизни коллектива: Организация не сможет достичь поставленных целей без соответствующей внутренней... Как распознать напряжение: Говоря о мышечном напряжении, мы в первую очередь имеем в виду мускулы, прикрепленные к костям ... Почему люди поддаются рекламе?: Только не надо искать ответы в качестве или количестве рекламы... ©2015-2024 megaobuchalka.ru Все материалы представленные на сайте исключительно с целью ознакомления читателями и не преследуют коммерческих целей или нарушение авторских прав. (201)
|
Почему 1285321 студент выбрали МегаОбучалку... Система поиска информации Мобильная версия сайта Удобная навигация Нет шокирующей рекламы |