Думаю, можно ввести по определению: если квантору существования не предшествует квантор общности, то квантор существования убираем, а соответствующую предметную переменную заменяем на константу; если предшествует (возможно, несколько), то квантор существования убираем, а предметную переменную заменяем на новую предметную функцию, зависящую от предметных переменных, связанных кванторами общности. Но как доказать теорему о выполнимости?
Помимо этого, заметил, что в литературе под сколемовской формой понимаются различные вещи.
-- 21.02.2017, 12:41 --Ясно, что выражение "для любого

найдётся

" символизирует зависимость

от

. Но как это обосновать, если не вводить по определению?