Итак. Если универсальный квантор в нестандартной интерпретации раскладывается на возможно

Question

Итак. Если универсальный квантор в нестандартной интерпретации раскладывается на возможно

бесконечную конъюнкцию, а это возможно бесконечная формула,

то будет ли верно, что

при актуальном бесконечном числе x, которые x : A, тип-произведение (который П-тип) может быть преобразован в бесконечную формулу?

0

12.08.2024

2 ответов

23 просмотра

Brenoritvrezorkre Автор вопроса

Alexander Chichigin
Так понятно. Но ты ж сам написал ответ. В "обычно...

Ну дело в чём

0

3 месяца назад

Alexander Chichigin · Accepted Answer

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

Похожие чаты

Итак. Если универсальный квантор в нестандартной интерпретации раскладывается на возможно

2 ответов

Похожие вопросы