Краткая методичка по логике (стр. 6 из 10)

Правилами тождества, равенства, неотличимости называются следующие три правила соответственно:

(x, x)

(x_1,y₁)Ù…Ù g

(x_n,y_n)Þg

(f(x_1,…,x_n), f(y_1,…,y_n))

Dg² (x_1,y₁)Ù…Ù g

(x_n,y_n)Þ(g f(x_1,…,x_n)Þ(y_1,…,y_n))

Теорема об эгалитарной замене: пусть q есть результат замены в p некоторых вхождений терма a термом b; тогда если выражение g²₀(a, b) является истинным, то p равносильно q.

Теорема о транзитивности логического следствия: если p₁, …, p_n│=q₁,_…, q_m и q₁, …, q_m│= r_{1, …}, r_e, то p₁, …, p_n│= r_{1, …}, r_e.

Теорема о расширении списка гипотез: если p₁, …, p_n│= q, то p₀, …, p_n│= q.

Теорема дедукции: если высказывания p₁, …, p_nявляются замкнутыми, то p₁, …, p_n│= p тогда и только тогда когда ê= p₁Ù…Ù p_nÞp.

Теорема о конъюнктивизации гипотез: p₁, …, p_n│= p тттк p₁Ù…Ùp_n│= p.

Теорема о выводе в эгалитарной логике: правила тавтологии, отделения, обобщения, подтверждения, общевнесения, сущевнесения, тождества, равенства, неотличимости образуют достаточный набор правил вывода в эгалитарной логике, т.е. p₁, …, p_n│= p тттк p может быть получено из p₁, …, p_n с помощью этого набора правил.

Теорема о сравнительной силе выводов. Если p является тавтологическим следствием из p₁, …, p_n, то p является кванторологическим следствием из p₁, …, p_n. Если p является кванторологическим следствием из р₁,…,р_n, то p является логическим следствием из р₁,…,р_n.

Алгоритм – это…

Теорема о неразрешимости проблемы логического следствия (логической истинности): нельзя придумать алгоритм, который для любых высказываний p₀, …, p_n позволял бы разрешить вопрос о том, является или нет p₀ логическим следствием из p₁, …, p_n. Полезно обратить внимание на то, что проблема тавтологического следствия является разрешимой с помощью истинностных таблиц.

Замечание последние семь теорем не исключают случай n = 0.

Замечание если не оговорено противное, слово логика понимается как эгалитарная логика.

Тема 6. Формальные теории

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

Изложение любой формальной теории в принципе можно оформить в виде книжек с доказательными текстами:

1	a₁-×-×-×-×-×-×-×-×-×-	ü индуктивнаяý последовательность þ термов
…	××××××××××××××××××××××××××××××××××××××××××××××××××××××
k	a_k-×-×-×-×-×-×-×-×-×-
k+1	r₁-×-×-×-×-×-×-×-×-×-	ü индуктивнаяý последовательность формулþ на основе a₁,…, a_k
…	××××××××××××××××××××××××××××××××××××××××××××××××××××××
k+е	r_e-×-×-×-×-×-×-×-×-×-
k+е+1	s₁-×-×-×-×-×-×-×-×-×-	ü аксиомыýs₁,…, s_m есть þ среди r₁,…, r_e
…	××××××××××××××××××××××××××××××××××××××××××××××××××××××
k+е+m	s_m-×-×-×-×-×-×-×-×-×-
k+е+m+1	t₁-×-×-×-×-×-×-×-×-×-	ü индуктивнаяý последовательность теоремþt₁,…, t_n есть среди r₁,…, r_e
…	××××××××××××××××××××××××××××××××××××××××××××××××××××××
k+е+m+n	t_n-×-×-×-×-×-×-×-×-×-

Здесь штрих-пунктирная линия обозначает пояснение о том, с помощью какого правила порождения получено соответствующее знакосочетание. Для удобства таких пояснений знакосочетания a₁,…, t_n нумеруются последовательно от 1 до k+е+m+n. Вспомним, что правила порождения теорем являются правилами вывода, что конечная индуктивная последовательность теорем является доказательством и что следующие девять правил, называемых основными, образуют достаточный набор правил вывода из аксиом: правила тавтологии, отделения, обобщения, подтверждения, общевнесения, сущевнесения, тождества, равенства, неотличимости.

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

Способы более компактного изложения формальной теории.

1. Последовательность a₁,…, r_e не записывается, потому что при достаточном навыке термы и формулы распознаются без построения их индуктивных последовательностей.

2. В последовательность t₁,…, t_n включаются теоремы из других доказательных текстов.

3. Для двухместного функционального или предикатного знака v используется операционная форма записи: вместо v(a,b) пишут (a)v(b).

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

5. Используются специальные начертания для функциональных и предикатных знаков. Например в теории чисел: 0, 1, 2, 3 - нульместные функциональные знаки; Ö, sin, cos - одноместные функциональные знаки; +, -, ´, /, - двухместные функциональные знаки; <,>,£,³ - двухместные предикатные знаки.

6. Используются знаковые фигуры. Например, å_х=3х обозначает сумму 3+4+5.

7. Вводится определяющая аксиома g(х₁,...,х₁₁)Û р для нового n-местного предикатного символа g. Здесь переменные х₁,...,х_nпопарно различны, а высказывание р не имеет свободных вхождений переменных, отличных от х₁,...,х_n.

8. Вводится определяющая аксиома р{х, ¦( х₁,...,х_n)} для нового n - местного функционального символа ¦ в тех случаях, когда формула $рх является теоремой. Здесь переменные х, х₁,...,х_nпопарно различны, а р не имеет свободное вхождение переменных, отличных от х, х₁,...,х_n.

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

9. Кроме девяти основных применяются дополнительные правила вывода, например правило отделения конъюнкта DpÙg, р и правило присоединения дизъюнкта Dр, pÚg.

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

Теорема о доказательстве методом от противного: если формальная теория Т₂ получена путем добавления аксиомы Øр к аксиомам теории Т₁ и если формулы q, Øq являются теоремами теории Т₂, то формула р является теоремой теории Т₁.

Формальная арифметика формализует систему знаний о целых неотрицательных числах, использует в качестве исходных четыре функциональных и два предикатных знака

¦	¦	¦	¦	g	g
0	1	+	×	=	<

интерпретируемых в соответствии с их известными со школы специальными начертаниями, имеет такие аксиомы