В статье описывается подход к анализу пропозициональных уста­новок, опирающийся на теоретико-типовую семантику, предло­женную А. Ранта и основанную на теории типов П. Мартин-Лёфа. Теоретико-типовая семантика в явном виде содержит контексты и способы извлечения информации из них. Это позволяет кор­ректно формализовать зависимость от контекста, характерную для пропозициональных установок. В статье контекст представ­ляется в виде типа зависимой суммы (тип Record в системе рабо­ты с доказательствами Coq), при этом подход А. Ранта уточняется и применяется к анализу фразы Куайна «Ральф верит, что кто-то шпион». Описано три варианта формализации этой фразы, ко­торые различаются содержанием контекстуального знания и способом вывода из него истинностных значений фразы. Связь между контекстами устанавливается функцией преобразования, позволяющей соотносить значения истинности. В результате, средства для работы с контекстами, предоставляемые теорети­ко-типовой семантикой, позволяют избежать проблем непро­зрачности, описанных Куайном. Формализация вместе с доказа­тельствами кодирована в Coq и свободно доступна.