Аксио́ма своди́мости, аксиома, добавленная Б. Расселом к его разветвлённой теории типов с целью избежать расслоения понятий (см. в статье Непредикативное определение). В разветвлённой теории типов множества данного типа разделяются на порядки. Так, вместо понятия множества натуральных чисел появляется понятие множества натуральных чисел данного порядка. При этом множество натуральных чисел, определяемое формулами без использования каких-либо множеств, принадлежит первому порядку. Если в определении используется совокупность множеств первого порядка, а совокупности множеств высшего порядка не используются, то определяемое множество принадлежит второму порядку, и т. д. Например, если $S$ – семейство множеств, состоящее из множеств одного и того же порядка, то множество

$$M=\{x\mid\exists y(y\in S \wedge x\in y)\}$$должно принадлежать следующему порядку, т. к. в его определении содержится квантор по множествам данного порядка. Аксиома сводимости утверждает, что для каждого множества существует равнообъёмное ему (т. е. состоящее из тех же самых элементов) множество первого порядка. Таким образом, аксиома сводимости фактически сводит разветвлённую теорию типов к простой теории типов.