спасибо за поправку!
насколько я понимаю, в КИВ и в интуиционистской логике вообще не используется понятие дву- или не дву- значности. Там для формул другое деление: не на истинные и ложные, а на аксиомы, теоремы и недоказанные. Иногда, правда, вводят мисволы true и false, но опят-таки, не как истинность, а просто как символы, с которыми надо играть по этим правилам. Т.е. например, нельзя взять и заменить в формуле ~true на false.