Я начал как раз с предложения обсудить, что такое ложь, и в чем ее отличие от противоречия, т.к. об истине и так говорят достаточно. Но я не могу сформулировать, что такое ложь.
Ну что ж, обсудить понятие лжи можно, но чтобы было что обсуждать, нужно дать какое-нибудь определение.
Есть такой подход: вводится базовое (неопределяемое) понятие "универсальной лжи" или "абсурда", обозначаемое символом

. Предположение

считается опровергнутым, если в теории есть вывод

, т.е. если оно сводится к абсурду. Соответственно, отрицание по определению вводится как сведение к абсурду. Т.е. вводится логический закон:

. Иногда вместо "сведения к абсурду" говорят о "сведении к противоречию", поскольку подразумевается логический закон

(т.е. доказательство одновременно и высказывания, и его отрицания автоматически считается абсурдом).
Согласно такому определению "ложное" - это есть отрицание "истинного". Это всё работает и в классическом, и в интуиционистском исчислениях предикатов.
К вопросу о том, что одно и тоже утверждение в теории и метатеории может быть ложным и не ложным. Выше я привел пример с "множеством всех множеств", которое обозначил:

.
Противоречивость или ложность этой формулы не очевидна, т.к.

и

могут быть объектами разного уровня. Эта формула ложна в теории, где все объекты одного уровня и может быть истинной в метатеории: "существует каталог всех множеств".
Совершенно верно! Вся проблема в том, что

не может быть объектом того же уровня иерархии, что и другие объекты теории множеств. Если определить новый уровень иерархии, то проблема снимается. Мало того, поскольку метатеория
уже работает с объектами другого уровня иерархии, она без дополнительных определений может непротиворечиво утверждать существование "множества всех множеств":

Как видите, формулировка несколько отличается от Вашей: здесь есть дополнительное условие, которое говорит о том, что речь идёт о множестве не всех множеств "вообще", а о множестве всех множеств, определённых теорией

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

, но его отрицание и есть обсуждаемая формула.
Здесь Вы ошиблись: Отрицание

это

, да и то только в классической логике (в интуиционистском исчислении предикатов всё несколько сложнее).
Если же в теории это не утверждается, то приведенный Вами закон:

, можно интерпретировать так:

не противоречиво, т.к.

и

определяют объекты разного уровня.
Непонятно о чём тут Вы. Утверждение высказывания и одновременно его отрицание - это и называется "противоречием", по определению.