Варианты понятия реализуемости для пропозициональных формул, приводящие к логике слабого закона исключенного третьего

До сих пор неизвестно, является ли конечно (или хотя бы рекурсивно) аксиоматизируемой логика реализуемых пропозициональных формул. Мы предлагаем несколько естественных ослаблений клиниевской реализуемости пропозициональных формул, основанных на следующей неформальной идее: пропозициональная формула реализуема, если при любой подстановке у нее найдется “простая” реализация. Мы доказываем, что все эти ослабления приводят к одной конечно аксиоматизируемой логике — логике слабого закона исключенного третьего. Доказательство использует характеризации суперинтуиционистских логик с интуиционистским позитивным фрагментом, полученные в 60-е годы Ю. Т. Медведевым и В. А. Янковым.