Ступе́нчатая семанти́ческая систе́ма, вариант конструктивной семантики, предложенный А. А. Марковым (Markov. 1971; Марков. О языке Я₀. 1974). Основное внимание при построении этой системы уделяется одной из проблем семантики – конструктивному истолкованию импликации. Традиционное интуиционистское разъяснение смысла утверждения $(A\supset B)$ состоит в том, что $(A\supset B)$ выражает осуществимость конструкции $p$ такой, что если $q$ – произвольная конструкция, подтверждающая $A$, то $p$ и $q$ в совокупности позволяют отыскать конструкцию, подтверждающую $B$. Приведённое неформальное разъяснение по ряду причин плохо поддаётся уточнению. Идея А. А. Маркова состоит в том, что импликация $(A\supset B)$ рассматривается как формулировка утверждения о выводимости $B$ из посылки $A$ средствами некоторой теории с правилом бесконечной индукции (полуформальной теории). При этом рассматриваемая полуформальная теория, так же как и семантика формул $A$ и $B$, должна быть объяснена ранее, на некотором предыдущем этапе построения. В результате возникает ступенчатая семантическая система, в которой смысл формул следующей ступени определяется в терминах объектов предыдущей ступени.

А. А. Марков построил два эквивалентных варианта ступенчатой семантической системы – «длинная башня» (Markov. 1971) и «короткая башня» (Марков. О языке Я₀. 1974). Ниже кратко описан вариант построения «короткой башни» в традиционных обозначениях исчисления предикатов и для языка формальной арифметики (сам А. А. Марков использовал бесскобочные обозначения формул). Элементарные формулы языка $\text{Я}_0$ имеют один из видов ($t=r$) или ($t\ne r$), где $t$, $r$ – примитивно-рекурсивные термы (термы $\text{Я}_0$). Остальные формулы $\text{Я}_0$ строятся обычным образом – с помощью логических связок конъюнкции $\wedge$, дизъюнкции $\lor$ и ограниченных кванторов $(\forall x\le t)\varphi$, $(\exists x\le t)\varphi$, где $\varphi$ – формула $\text{Я}_0$ и $t$ – терм $\text{Я}_0$. Язык $\text{Я}_0$ разрешим в том смысле, что имеется общий способ распознавания истинных замкнутых формул $\text{Я}_0$ среди всего множества формул $\text{Я}_0$. Семантика формул $\text{Я}_0$ определяется индукцией по построению формулы. Всякая формула $\text{Я}_0$ эквивалентна бескванторной формуле.

Формулы $\text{Я}_1$ строятся исходя из формул $\text{Я}_0$ с помощью любого числа применений связок $\wedge$, $\lor$ и квантора существования. Язык $\text{Я}_1$ неразрешим, но может быть построено некоторое исчисление $\text{И}$, в котором выводятся все истинные замкнутые формулы $\text{Я}_1$, и только они.

Формулы $\text{Я}_2$ строятся индуктивно исходя из формул $\text{Я}_1$ с помощью однократного применения связки $\supset$ и любого числа применений конъюнкции $\wedge$ и квантора общности $\forall$. Таким образом, формулы $\text{Я}_2$ имеют один из следующих видов: 1) формулы $\text{Я}_1$; 2) $(\varphi\wedge\psi)$, где $\varphi$, $\psi$ – формулы $\text{Я}_2$; 3) $(\alpha\supset\beta)$, где $\alpha$, $\beta$ – формулы языка $\text{Я}_1$; 4) $\forall x\varphi$, где $\varphi$ – формула $\text{Я}_2$. Импликации $(\alpha\supset\beta)$ понимаются следующим образом: $(\alpha\supset\beta)$ выражает наличие общего метода, позволяющего по любому слову $Q$ в алфавите языков устанавливать, что $Q$ не есть вывод формулы $\alpha$ в исчислении $\text{И}$, либо давать вывод $\beta$ в исчислении $\text{И}$. Затем строится полуформальная теория $S_2$, в которой выводимы замкнутые формулы $\text{Я}_2$ (роль $S_2$ для $\text{Я}_1$ играет $\text{И}$). Аксиомами $S_2$ являются верные формулы $\text{Я}_2$. Среди обычных правил вывода имеется и эффективное $\omega$ – правило с бесконечным числом посылок: если имеется общий метод, позволяющий вывести в $S_2$ формулу $\varphi(n)$ при всяком натуральном $n$, то и формула $\forall\, \varphi(x)$ может считаться выводимой в $S_2$. Семантическая пригодность $S_2$ выражается следующей теоремой: всякая замкнутая формула $\text{Я}_2$, выводимая из верной формулы $\text{Я}_2$ как из посылки, верна в $\text{Я}_2$.

Формулы $\text{Я}_3$ строятся индуктивно исходя из формул $\text{Я}_2$ с помощью однократного применения связки $\supset_1$ и любого числа применений $\wedge$ и $\forall$. Импликация $(\alpha\supset_1\beta)$ выражает, что $\beta$ выводится из формулы $\alpha$ в теории $S_2$. Можно показать, что два вида импликаций в языке $\text{Я}_3$ согласованы между собой там, где оба они применимы. Затем строится полуформальная теория $S_3$ и доказывается её семантическая пригодность. Аналогичным образом определяются языки $\text{Я}_4, \text{Я}_5,\dots$ и полуформальные теории $S_4, S_5,\dots$ . Формулы $Я_{n+1}$ строятся исходя из формул $\text{Я}_n$ с помощью однократного применения связки $\supset_{(n-1)}$ к формулам предыдущего языка $\text{Я}_n$ и любого числа применений связок $\wedge$ и $\forall$ к формулам языка $\text{Я}_{n+1}$. Импликация $(\alpha\supset_{(n-1)}\beta)$ выражает, что $\beta$ выводится из $\alpha$ в теории $S_n$. Все $S_n$ семантически пригодны: всякая замкнутая формула $\text{Я}_n$, выводимая из верной формулы, верна. Импликации различных уровней согласованы там, где обе они применимы.

Указанная согласованность даёт возможность объединить все языки $\text{Я}_n$ в один язык $\text{Я}_\omega$, формулы которого получаются, если у импликаций всех языков $\text{Я}_n$ убрать индексы. Формула $\varphi$ языка $\text{Я}_\omega$ считается верной, если она верна в некотором языке $\text{Я}_n$ при произвольной расстановке индексов у импликаций, превращающей $\varphi$ в формулу языка $\text{Я}_n$.

Если ввести в $\text{Я}_\omega$ отрицание $\neg\varphi$ как сокращение для $(\varphi\supset 0=1)$, то формула вида $\neg\neg\alpha\supset\alpha$ верна в $\text{Я}_\omega$ для всякой формулы $\alpha$ языка $\text{Я}_1$. Таким образом, принцип конструктивного подбора оказывается верным в $\text{Я}_\omega$. Языки $\text{Я}_n$ образуют существенно невырожденную иерархию с точки зрения выразительных возможностей формул этих языков. Классическое исчисление предикатов со связками $\wedge$, $\neg$, $\supset$, $\forall$ является полным относительно истинности в $\text{Я}_\omega$.

Наконец, язык $\text{Я}_{\omega+1}$ содержит все формулы формальной арифметики. С помощью алгоритма выявления конструктивной задачи по Шанину (Шанин. 1958) всякая замкнутая формула $\varphi$ языка $\text{Я}_{\omega+1}$ может быть приведена к виду $\exists x\ \psi(x)$, где $\psi(x)$ – формула языка $\text{Я}_\omega$. Формула $\varphi$ считается верной, если осуществимо натуральное число $n$ такое, что $\varphi(n)$ верна в $\text{Я}_0$. Такое понимание суждений арифметики хорошо согласовано со всеми основными принципами конструктивной математики. В частности, всякая формула $\text{Я}_{\omega+1}$ эквивалентна утверждению о собственной рекурсивной реализуемости по Клини (Драгалин. 1979).