63. Формальные теории. Принципы построения формальной теории.

Алфавит и слова

• Алфавит A — конечное множество, элементами которого являются символы (буквы, цифры, знаки препинания, знаки операций и т.д.).

• Элементы An называют словами длины n в алфавите A

• Множество всех слов в алфавите A — это множество

• Формальные системы — это системы операций над объектами, понимаемыми как последовательности символов (т.е. как слова в фиксированных алфавитах); сами операции также являются операциями над символами.

• «Формальный» = объекты и операции рассматриваются чисто формально, без каких бы то ни было содержательных интерпретаций символов.

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

Принципы построения формальной теории

Всякая точная теория определяется:

• языком, т.е. некоторым множеством высказываний, имеющих смысл с точки зрения этой теории,

• совокупностью теорем — подмножеством языка, состоящим из высказываний, истинных в данной теории.

Аксиоматическая (формальная) теория T считается определенной, если выполнены следующие условия:

1) задано некоторое счетное множество символов — алфавит теории T. Конечные последовательности символов теории называются выражениями теории T;

2) определяется подмножество правильно построенных выражений теории T, называемых формулами теории T — язык теории. Это подмножество задается конструктивными средствами (как правило, индуктивным определением);

3) выделяется некоторое множество формул, называемых аксиомами теории T;

4) задается конечное множество R1, R2, ..., Rn отношений между формулами, называемых правилами вывода. Правило вывода R(F1, …, Fn, G) — это вычислимое отношение на множестве формул. Если формулы F1, …, Fn, G находятся в отношении R, то формула G называется непосредственно выводимой из F1, …, Fn по правилу R. формулы F1, …, Fn, называются посылками правила R, а G — его следствием или заключением.

Вывод в T

• Выводом в T формулы B из формул A1, …, An, называется всякая последовательность F1, F2, ..., Fm формул такая, что Fm = B, а для любого i формула Fi есть либо аксиома теории T, либо одна из исходных формул A1, …, An, либо непосредственно выводима из формул F1, …, Fi-1 (или какого-то их подмножества) по одному из правил вывода.

• Если существует вывод B из A1, …, An, то говорят, что B выводима из A1, …, An. Этот факт обозначается A1, …, An |— B.

• Формулы A1, …, An называются гипотезами или посылками вывода.

• Переход в выводе от Fi-1 к Fi называется i-м шагом вывода.

Разрешимость

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

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

Доказательство

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

• Формула B, для которой существует доказательство, называется формулой, доказуемой в теории T, или теоремой теории T. Факт доказуемости B обозначается |— B.

• Очевидно, что присоединение формул к гипотезам не нарушает выводимости.