С фокуса на modus tollens вроде как понятно, и чуть прояснилось..

А что происходит в случае, если при док-ве от противного мы берем некоторое противное утверждение Z, которое на самом деле невыводимое, но мы об этом не знаем? Получится, что мы не сможем ничего доказать (выйти на известные истинные или ложные), или мы можем все таки выйти на какие-то известные или ложные?

И становится непонятным, можно ли каким-либо образом доказать, что Z невыводимо?