Не могу понять доказательство разрешимости класса формул в исчислении предикатов с одноместными предикатами у Игошина в книге Математическая логика и теория алгоритмов, в его книге - это теорема 23.2. Утверждение теоремы следующее:
Теорема 23.2. Если формула логики предикатов, содержащая только одноместные предикатные переменные, выполнима, то она выполнима на конечном множестве, содержащем не более

элементов, где

— число различных предикатных переменных, входящих в рассматриваемую формулу.
Если лень открывать книгу, то можно прочитать доказательство дословно
здесь.
Прежде всего я не могу понять, где автор использует одноместность предикатов (Ctrl-F подтверждает). Уже 3 раза прочел, все равно не понимаю. Попробовал конкретные формулы рассматривать - тоже в голову ничего не приходит.
Вообще, попробую доказательство укоротить и выложить здесь и перечитать, может пойму тогда.
Если эта теорема есть в другом источнике - сообщите пожалуйста.
upd: у меня появилась мысль, что доказывается разрешимость не для всего класса формул с одноместными предикатами, а для более узкого класса: для всех формул ИП с одноместными предикатами, такими, что каждый предикат имеет свою переменную, входящую только в него и не входящую ни в какие другие предикаты (т.е. биекция между предикатами и переменными). Если так, тогда действительно очевидно: просто перебираем для каждого предиката значения

- они будут независимы от истинностных значений других предикатов и все...
upd2:
upd: у меня появилась мысль, что доказывается разрешимость не для всего класса формул с одноместными предикатами, а для более узкого класса: для всех формул ИП с одноместными предикатами, такими, что каждый предикат имеет свою переменную, входящую только в него и не входящую ни в какие другие предикаты (т.е. биекция между предикатами и переменными).
Попробовал - получается, что это роли не играет. На самом деле между множеством одноместных предикатов и множеством переменных есть сюрьекция. При проведении индукции просто тогда надо делать подстановку предмета

не в один предикат, а в несколько. А дальше все равно все обеспечивает квантор

.
А одноместность, видимо, нужна для того, чтобы при подстановке хотя бы одной переменной в предикат из последнего получалось высказывание. Хотя не очевидно.