а + 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₁... "x₉ (P ¹ Q ) невыводима, хотя и выражает истинное суждение, а именно непротиворечивость Ф. а. Поэтому неразрешимость диофантова уравнения Р - Q = 0 недоказуема в Ф. а. Непротиворечивость Ф. а. доказана с помощью трасфинитной индукции до ординала e (наименьшее решение уравнения w^e = e). Поэтому схема индукции до e недоказуема в Ф. а., хотя там доказуема схема индукции до любого ординала a < e . Класс доказуемо рекурсивных функций Ф. а. (т. е. частично рекурсивных функций, общерекурсивность которых может быть установлена средствами Ф. а.) совпадает с классом ординально рекурсивных функций с ординалами < e .

  Не все теоретико-числовые предикаты выразимы в Ф. а.: примером является такой предикат T, что для любой замкнутой арифметической формулы А имеет место Т (éА ù) « А, где éА ù – номер формулы А в некоторой фиксированной нумерации, удовлетворяющей естественным условиям. Присоединение к Ф. а. символа Т с аксиомами типа

Т (éА & B ù) « Т (éА ù) & Т (éB ù),

выражающими его перестановочность с логическими связками, позволяет доказать непротиворечивость Ф. а. Похожая конструкция (но уже внутри Ф. а.) доказывает, что схему индукции нельзя заменить никаким конечным множеством аксиом. Ф. а. корректна и полна относительно формул вида $x₁ ... $x_k (P = Q ); замкнутая формула из этого класса доказуема тогда и только тогда, когда она истинна. Так как этот класс содержит алгоритмически неразрешимый предикат, отсюда следует, что проблема выводимости в Ф. а. алгоритмически неразрешима.

  При задании Ф. а. в виде генценовской системы осуществима нормализация выводов, причём нормальный вывод числового равенства состоит только из числовых равенств. На этом пути было получено первое доказательство непротиворечивости Ф. а. Нормальный вывод формулы с кванторами может содержать сколь угодно сложные формулы. Полная подформульность достигается после замены схемы индукции на со-правило, позволяющее вывести В ® "xA (x ) из В ® A (0), B ® A (1),... Понятие w-вывода (т. е. вывода с w-правилом) высоты < e выразимо в Ф. а., поэтому переход к w-выводам позволяет устанавливать в Ф. а. многие метаматематические теоремы, в частности полноту относительно формул вида $x₁ ... $x_k (P = Q ) и ординальную характеристику доказуемо рекурсивных функций.

  Лит.: Клини С. К., Введение в метаматематику, пер. с англ., М., 1957; Hilbert D., Bernays P., Grundlagen der Mathematik, 2 Aufl., Bd 1–2, В., 1968–70.

  Г. Е. Минц.

Форма'льная грамма'тика, в языкознании, одно из средств строгого описания естественных языков; один из разделов математической лингвистики (см. Грамматика формальная ).

Форма'льная ло'гика, наука о мышлении, предметом которой является исследование умозаключений и доказательств с точки зрения их формы и в отвлечении от их конкретного содержания. Ф. л. – базисная наука; её идеи и методы используются как в повседневной практике, например в качестве средства предотвращения логических ошибок, так и в особенности в теории для логического анализа научного знания. См. Логика .

Форма'льная систе'ма, неинтерпретированное исчисление , класс выражений (формул) которого задаётся обычно индуктивно – посредством задания исходных («элементарных», или «атомарных») формул и правил образования (построения) формул, а подкласс доказуемых формул (теорем) – посредством задания системы аксиом и правил вывода (преобразования) теорем из аксиом и уже доказанных теорем. Термин «Ф. с.» имеет многочисленные синонимы (иногда, впрочем, этими терминами обозначают родственные, но не совпадающие понятия): формальная теория, формальная математика, формализм, формальное исчисление, абстрактное исчисление, синтаксическая система, аксиоматическая система, логистическая система, формализованный язык , формальная логика , кодификат, дедуктивная система и др.

Форма'льный аксиомати'ческий ме'тод, см. Аксиоматический метод .

«Форма'льный ме'тод» в литературоведении, теоретическая концепция, утверждающая взгляд на художественную форму как категорию, определяющую специфику литературы и способную к саморазвитию. «Ф. м.» в определённой мере подготовлен неокантианством . Как особое направление сложился на рубеже 19–20 вв. первоначально как реакция на импрессионистическую критику и позитивистски окрашенные направления в литературоведении и искусствознании (например, культурно-историческая школа в литературоведении), позднее – как теоретически обосновываемая методика, устремленная к изучению внутренних (структурных) закономерностей художественного произведения.

  На Западе в 1910-е гг. «Ф. м.» ярче всего проявил себя в теории изобразительного искусства (Г. Вёльфлин ) и при сравнительном изучении различных искусств (О. Вальцель – Германия), что имело положительным результатом наблюдения в области описательной (формальной) типологии. В литературоведении «Ф. м.» был представлен изучением «морфологии романа» (В. Дибелиус – Германия), «языковой стилистики» (Л. Шпитцер ) и др. Методические принципы ряда разновидностей «Ф. м.» на Западе сводились к «пристальному чтению» произведений при игнорировании всех «внелитературных» компонентов. Итоги его развития в 1920-е гг. – утверждение статистической описательной методики, отказ от генетических и эволюционных планов изучения литературы.

  Существенно иное явление по генезису и методологии – «формальная школа» в России (середина 1910-х – середина 1920-х гг.), исходившая не из искусствоведческих концепций, а из ориентации на лингвистику (что характерно в первую очередь для ОПОЯЗ а и Московского лингвистического кружка). Учение И. А. Бодуэна де Куртенэ о языке как функцией, системе, переосмысленное применительно к литературным явлениям, способствовало переходу от ранней механистической доктрины, в силу которой произведение рассматривалось как «сумма» (В. Б. Шкловский ) составляющих его «приёмов» («формальная поэтика»), к взгляду на произведение как «систему» (Ю. Н. Тынянов ) функциональных единиц (представление, характерное для «функциональной поэтики»). Одновременно эволюционирует взгляд на основные понятия теоретической и исторической поэтики: от оценки формы как единственной носительницы художественной специфики и игнорирования содержания как «внехудожественной» категории – к постановке и обоснованию в общем виде концепции «содержательной формы»; от представления о смене литературных явлений в результате разрушения автоматизма восприятия и борьбы «старшей» (канонизированной) линии с неканонизированной «младшей» линией к историко-литературному осмыслению смены жанров и стилей.