Видите ли, если уж у нас есть формальная теория, то автоматически предполагается, что её предметная область не является пустой
Не факт. До тех пор, пока не был решен вопрос с ВТФ, предположения как о наличии, так и об отсутствии решений у этого уравнения рассматривались как равновозможные.
Наличие или отсутствие решений любого уравнения не имеет отношения к предметной области арифметики. Предметная область арифметики — совокупность натуральных чисел. Она предполагается непустой. Есть ли у какого-то уравнения решения, нет ли — это совсем другой вопрос.
То же самое относится к теории грибов и к теории умпасонов.
Ели у нас есть некая формальная теория грибов, то её предметная область — совокупность грибов. И она предполагается непустой. А уж есть ли среди них съедобные или несъедобные, значения не имеет. Конечно, это влияет на истинность или ложность некоторых высказываний, но не более того.
Ага. После чего это можно преобразовать в

— «все вещи — не (несъедобные грибы)», или дальше «для всякой вещи, она съедобна или она — не гриб».
Какие вещи? Не знаю. Я же вот этим
Вовсе не расширил универсум.
Но можно представить себе более общую теорию, некоторые объекты которой являются грибами, некоторые — умпасонами, и так далее. В такой теории предполагается, что область всех объектов является непустой, хотя может оказаться, что, например, ни одного гриба нет, если нет специальной аксиомы, требующей существования хотя бы одного гриба. Также в такой теории должны существовать специальные предикаты, выделяющие объекты того или иного типа. Например, пусть

— предикат, означающий, что объект

есть гриб. Тогда высказывание "некоторые грибы несъедобны" запишется в виде

, а его отрицание (после ряда преобразований, погружающих символ "

" максимально глубоко внутрь формулы) — в виде

(замечу, что предикат может обозначаться специальным символом или записываться некоторой формулой).
Если из аксиом теории следует, что не существует ни одного объекта, то такая теория является противоречивой (просто есть такая теорема: формальная теория непротиворечива тогда и только тогда, когда она имеет модель; а в определении модели имеется требование, чтобы предметная область (универсум) была непустой).
неверно, что

равносильно тому, что

Вы хотели сказать "неверно, что

равносильно тому, что

?
Нет, он хотел сказать, что высказывание "неверно, что

" равносильно высказыванию "

", но забыл первое высказывание как-то выделить, из-за чего возникла неоднозначность прочтения. Но первое высказывание и есть "

".