Погружающая операция

- в математической логике операция, переводящая выражения одного логико-математич. языка в выражения другого с сохранением тех или иных дедуктивных свойств. П. о. широко используются для установления взаимосвязи между различными логич. теориями, исчислениями. Напр., если формуле Аформальной арифметики сопоставить формулу А* этого же языка, вставив два отрицания перед ней и перед каждой ее подформулой (напр., [img: http://localhost:8080/file/041718-89.jpg] есть [img: http://localhost:8080/file/041718-90.jpg]), а [img: http://localhost:8080/file/041718-91.jpg] есть [img: http://localhost:8080/file/041718-92.jpg], и т. д.), то из выводимости Ав классической формальной арифметике следует выводимость А* уже в интуиционистской формальной арифметике. Отсюда вытекает, что непротиворечивость интуиционистской формальной арифметики влечет непротиворечивость и классической формальной арифметики. Описанная негативная интерпретация Гёделя позволяет, следовательно, указать важное взаимоотношение между интуиционистской и классич. арифметиками. Другой типичный пример П. о.- перевод Гёделя - Тарского, позволяющий установить взаимосвязь модальных и интуиционистских логик. Построение моделей в аксиоматич. теории множеств также может быть обычно интерпретировано синтаксически как построение нек-рой П. о.- внутренней модели теории множеств.