On 2020-08-22 21:39, mechvel at scico.botik.ru wrote: > [..] > I say "unsafe usage" because there also is a safe usage of EM - when > the predicate P is solvable. Corrrection: I meant "the related predicate". Wile in the example with Nat, this predicate is (exists n such that P n), and it is not solved. -- SM