Аксиом схема

- единый способ задания аксиом, обладающих одной и той же синтаксич. структурой. Конкретная А. с. обычно реализуется при помощи фиксирующего ее синтаксич. структуру выражения [img: http://localhost:8080/file/010109-267.jpg] (чаще всего не принадлежащего языку, в к-ром записываются аксиомы) и правил, позволяющих, исходя из выражения [img: http://localhost:8080/file/010109-268.jpg] получить произвольную аксиому данной структуры. В контекстах с заранее сформулированными или однозначно подразумеваемыми правилами порождения аксиом с помощью выражения [img: http://localhost:8080/file/010109-269.jpg] А. с. обычно наз. самовыражение [img: http://localhost:8080/file/010109-270.jpg] Так, напр., говорят о А. с. [img: http://localhost:8080/file/010109-271.jpg] пропозиционального исчисления Р, подразумевая под этим совокупность аксиом вида [img: http://localhost:8080/file/010109-272.jpg] где Аи В - произвольные формулы исчисления Р. Примером схемы нелогических аксиом является следующий вариант схемы индукции в традиционных аксиоматизациях арифметики: [img: http://localhost:8080/file/010109-273.jpg] здесь [img: http://localhost:8080/file/010109-274.jpg] предполагаются не принадлежащими алфавиту языка рассматриваемой формализации арифметики и интерпретируются, соответственно, как произвольная формула и произвольная переменная этой формализации. Применение А. с. обычно позволяет обойтись без правила подстановки при построении формальных теорий. Так, напр., во всяком достаточно сильном пропозициональном исчислении с двумя правилами вывода - правилом подстановки и правилом заключения - оказывается возможным ограничиться при выводах подстановками только в аксиомы, что позволяет эквивалентным образом модифицировать такое исчисление, заменив каждую аксиому соответствующей А. с. и удалив правило подстановки из числа действующих в нем правил вывода.