Лит.: Чёрч А., Введение в математическую логику, пер. с англ., т. 1, М., 1960, Введение (§§ 00–09).
Формалин
Формали'н, формоль, водный (обычно 37–40% -ный) раствор формальдегида , содержащий 4–12% метилового спирта в качестве стабилизатора; бесцветная жидкость со своеобразным острым запахом. При длительном хранении (особенно на холоду) Ф. мутнеет вследствие выпадения белого осадка – параформальдегида . Применяют как удобный источник формальдегида, например в производстве поливинилформаля (см. Поливинилацетали ), как антисептическое и дезодорирующее средство, например для дезинфекции помещений, одежды, инструментов, обработки рук, спринцевании, для сохранения анатомических препаратов, дубления кожи, как фунгицид для протравливания семян, клубней и семенных корнеплодов перед посевом или посадкой. Входит в состав формальдегидной мази и формидрона, применяемых при повышенной потливости; лизоформа, используемого для спринцеваний, дезинфекции рук и помещений. Ф. среднетоксичен для человека и теплокровных животных.
Формальдегид
Формальдеги'д (от лат. formica – муравей), муравьиный альдегид, CH2 O, первый член гомологического ряда алифатических альдегидов ; бесцветный газ с резким запахом, хорошо растворимый в воде и спирте, t кип – 19 °С. В промышленности Ф. получают окислением метилового спирта или метана кислородом воздуха. Ф. легко полимеризуется (особенно при температурах до 100 °С), поэтому его хранят, транспортируют и используют главным образом в виде формалина и твёрдых низкомолекулярных полимеров – триоксана (см. Триоксиметилен ) и параформа (см. Параформальдегид ).
Ф. очень реакционноспособен; многие реакции его лежат в основе промышленных методов получения ряда важных продуктов. Так, при взаимодействии с аммиаком Ф. образует уротропин (см. Гексаметилентетрамин ), с мочевиной – мочевино-формальдегидные смолы , с меламином – меламино-формальдегидные смолы , с фенолами – феноло-формальдегидные смолы (см. Феноло-альдегидные смолы ), с фенол- и нафталинсульфокислотами – дубящие вещества, с кетеном – b-пpoпиолактон . Ф. используют также для получения поливинилформаля (см. Поливинилацетали ), изопрена , пентаэритрита , лекарственных веществ, красителей, для дубления кожи, как дезинфицирующее и дезодорирующее средство. Полимеризацией Ф. получают полиформальдегид . Ф. токсичен; предельно допустимая концентрация в воздухе 0,001 мг/л.
Формальная арифметика
Форма'льная арифме'тика, формулировка арифметики в виде формальной (аксиоматической) системы (см. Аксиоматический метод ). Язык Ф. а. содержит константу 0, числовые переменные, символ равенства, функциональные символы +, •, ' (прибавление 1) и логические связки (см. Логические операции ). Постулатами Ф. а. являются аксиомы и правила вывода исчисления предикатов (классического или интуиционистского в зависимости от того, какая Ф. а. рассматривается), определяющие равенства для арифметических операций:
а + 0 = а , а + b’ = (а + b ),
а •0 = 0, а •b’ = (а •b ) + а ,
аксиомы Пеано:
ù(а’ = 0), a’ = b’ ® а = b ,
(a = b & а = с ) ® b = с , а = b ®a ' = b '
и схема аксиом индукции:
А (0) & " x (А (х ) ® А (x ')) ® " xa (x ).
Средства Ф. а. достаточны для вывода теорем элементарной теории чисел. В настоящее время, по-видимому, неизвестно ни одной содержательной теоретико-числовой теоремы, доказанной без привлечения средств анализа, которая не была бы выводима в Ф. а. В Ф. а. изобразимы рекурсивные функции и доказуемы их определяющие равенства. Это позволяет, в частности, формулировать суждения о конечных множествах. Более того, Ф. а. эквивалентна аксиоматической теории множеств Цермело – Френкеля без аксиомы бесконечности: в каждой из этих систем может быть построена модель другой.
Ф. а. удовлетворяет условиям обеих теорем Гёделя о неполноте. В частности, имеются такие полиномы Р , Q от 9 переменных, что формула " x 1 ... "x 9 (P ¹ Q ) невыводима, хотя и выражает истинное суждение, а именно непротиворечивость Ф. а. Поэтому неразрешимость диофантова уравнения Р - Q = 0 недоказуема в Ф. а. Непротиворечивость Ф. а. доказана с помощью трасфинитной индукции до ординала e0 (наименьшее решение уравнения we = e). Поэтому схема индукции до e0 недоказуема в Ф. а., хотя там доказуема схема индукции до любого ординала a < e0 . Класс доказуемо рекурсивных функций Ф. а. (т. е. частично рекурсивных функций, общерекурсивность которых может быть установлена средствами Ф. а.) совпадает с классом ординально рекурсивных функций с ординалами < e0 .
Не все теоретико-числовые предикаты выразимы в Ф. а.: примером является такой предикат T, что для любой замкнутой арифметической формулы А имеет место Т (éА ù) « А, где éА ù – номер формулы А в некоторой фиксированной нумерации, удовлетворяющей естественным условиям. Присоединение к Ф. а. символа Т с аксиомами типа
Т (éА & B ù) « Т (éА ù) & Т (éB ù),
выражающими его перестановочность с логическими связками, позволяет доказать непротиворечивость Ф. а. Похожая конструкция (но уже внутри Ф. а.) доказывает, что схему индукции нельзя заменить никаким конечным множеством аксиом. Ф. а. корректна и полна относительно формул вида $x 1 ... $xk (P = Q ); замкнутая формула из этого класса доказуема тогда и только тогда, когда она истинна. Так как этот класс содержит алгоритмически неразрешимый предикат, отсюда следует, что проблема выводимости в Ф. а. алгоритмически неразрешима.
При задании Ф. а. в виде генценовской системы осуществима нормализация выводов, причём нормальный вывод числового равенства состоит только из числовых равенств. На этом пути было получено первое доказательство непротиворечивости Ф. а. Нормальный вывод формулы с кванторами может содержать сколь угодно сложные формулы. Полная подформульность достигается после замены схемы индукции на со-правило, позволяющее вывести В ® "xA (x ) из В ® A (0), B ® A (1),... Понятие w-вывода (т. е. вывода с w-правилом) высоты < e0 выразимо в Ф. а., поэтому переход к w-выводам позволяет устанавливать в Ф. а. многие метаматематические теоремы, в частности полноту относительно формул вида $x1 ... $xk (P = Q ) и ординальную характеристику доказуемо рекурсивных функций.
Лит.: Клини С. К., Введение в метаматематику, пер. с англ., М., 1957; Hilbert D., Bernays P., Grundlagen der Mathematik, 2 Aufl., Bd 1–2, В., 1968–70.
Г. Е. Минц.
Формальная грамматика
Форма'льная грамма'тика, в языкознании, одно из средств строгого описания естественных языков; один из разделов математической лингвистики (см. Грамматика формальная ).
Формальная логика
Форма'льная ло'гика, наука о мышлении, предметом которой является исследование умозаключений и доказательств с точки зрения их формы и в отвлечении от их конкретного содержания. Ф. л. – базисная наука; её идеи и методы используются как в повседневной практике, например в качестве средства предотвращения логических ошибок, так и в особенности в теории для логического анализа научного знания. См. Логика .
Формальная система
Форма'льная систе'ма, неинтерпретированное исчисление , класс выражений (формул) которого задаётся обычно индуктивно – посредством задания исходных («элементарных», или «атомарных») формул и правил образования (построения) формул, а подкласс доказуемых формул (теорем) – посредством задания системы аксиом и правил вывода (преобразования) теорем из аксиом и уже доказанных теорем. Термин «Ф. с.» имеет многочисленные синонимы (иногда, впрочем, этими терминами обозначают родственные, но не совпадающие понятия): формальная теория, формальная математика, формализм, формальное исчисление, абстрактное исчисление, синтаксическая система, аксиоматическая система, логистическая система, формализованный язык , формальная логика , кодификат, дедуктивная система и др.
