Я использую аксиому бесконечности в виде формулы первопорядковой логики с единственным предикатом "a элемент b" арности 2 в виде изложенном в Мостовский "Конструктивные множества и их приложения".
Вместо описания могли бы и привести её здесь.
Формула
тоже разворачиваема в формулу без
,
и
. Если вы можете установить, имея уже развёрнутую формулу, что
Не возникает противоречия в ZF при добавлении аксиомы - "все множества - конечные".
то вы, думается, без труда можете показать выводимость друг из друга развёрнутой и этой формул.
-- Вт июн 03, 2014 17:45:51 --Кстати, как вы проверяли, что не возникает противоречия?