> Во-первых, да, ложные выводятся. Но во-вторых то, что вы привели не ложное!

Я как раз имел ввиду, что можно вывести то, что ~A является ложным.

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

> И вот в этом как раз заложен метод от противного. Если мы из гипотезы G вывели A, про которое известно, что оно ложно, то мы тем самым вывели не-G. То есть тогда не-G выводимо и истинно, не-A тоже выводимо и истинно, а A и G невыводимы и ложны.

Только так понимаю что в конце A и G выводимы и ложны.

После некоторых размышлений над всем этим пришёл к следующим выводам.
В теории мы изначально имеем набор аксиом. Они являются истинными утверждениями. Автоматически, если мы к аксиомам прикрутим "не", то получим набор ложных утверждений (например есть аксиома А, значит мы автоматически получаем, что ~A имеет значение "ложно").
Далее по правилам вывода мы можем получать новые утверждения. Если мы из A вывели B, то оно истинно, что автоматически означает, что ~B является ложным.
(?) Аналогично по ложным утверждениям мы тоже можем (или не можем?) применять правила вывода. Например если мы имеем ~A, которое является ложным, то можем попробовать из него вывести C, которое будет тоже ложным. Применив отрицание, можно получить ~C, которое будет уже истинным.
Док-во от противного. Мы берем произвольное утверждение D. И пытаемся из него вывести какое-нибудь известное (истинное или ложное утверждение). Если мы выводим ложное, то получается, что D ложно, соответственно ~D истинно, что и требовалось док-ть. Если же мы выведем истинное, то это означает, что D истинно, и соответственно ~D ложно, и все это уже будет выглядеть как обычное док-во по правилам вывода без противного.

Все верно?