1. У логіці та теорії моделей — властивість формальної теорії, яка полягає в тому, що для будь-якої істинної в усіх її моделях універсально-екзистенційної пропозиції (формули виду ∀x∃y P(x,y)) в теорії існує такий функціональний символ f, що твердження ∀x P(x, f(x)) можна довести в рамках самої теорії; забезпечує можливість явно знаходити об’єкти, існування яких постулюється.
2. У математичній логіці — властивість формальної системи, яка гарантує, що для будь-якої рекурсивної послідовності формул, які можна довести в системі, узагальнення цієї послідовності (омега-правило) також можна отримати в ній; означає замкнутість системи щодо правила нескінченної індукції.