Не понял, почему не работают? Это же, вроде, просто одно из правил вывода?
С помощью этого правила вывода и двойственного ему
![$P(t) \vdash \exists x P(t)$ $P(t) \vdash \exists x P(t)$](https://dxdy-01.korotkov.co.uk/f/c/6/2/c62966b8897aac27b9a6e39283285aa582.png)
можно вывести теорему
![$\forall x P(x) \to \exists x P(x)$ $\forall x P(x) \to \exists x P(x)$](https://dxdy-01.korotkov.co.uk/f/4/a/7/4a7bc4aa414241efe245c236c99ed69682.png)
, которая на пустой интерпретации ложна.
Если в языке есть какие-то термы, то там должны быть и константы, чтобы термы из чего-то построить, и тогда его нельзя интерпретировать пустой областью, а такой вывод будет дозволен. Если термов нет, то и правило не к чему будет применять. Или я что-то упускаю.
Но почему это что-нибудь должно быть пустым множеством? Или я чего-то не догоняю...
Потому что тогда добавляют аксиому
![$\forall x(x\notin\varnothing)$ $\forall x(x\notin\varnothing)$](https://dxdy-02.korotkov.co.uk/f/5/b/7/5b75d39bf65360663fa5af3108efbd1682.png)
.
![Smile :-)](./images/smilies/icon_smile.gif)
Такая аксиома получится и в теории, полученной из «обычной» ZFC после определения в ней пустого множества (это как раз добавление константы и определяющей её аксиомы на основании того, что выводится
![$\exists!n(\forall x(x\notin n))$ $\exists!n(\forall x(x\notin n))$](https://dxdy-03.korotkov.co.uk/f/2/a/8/2a806874437968cec1e0467e0227b6c782.png)
). Остальное уже написали, да и это немного дублирует.