Dennis Gorelik

Я не понимаю, в чем идея камента Хуана Ганди, но суть вроде такая, что запретительная статья дла λP2, а λPω такая статья не запрещает, а у нас не просто λPω=CoC (с двумя вселенными), а с бесконечным их количеством. Если Хуан Ганди считает мое мнение аргументации (я не говорю о мотивации постановки задачи), пусть потрудится указать на ошибку в моих логических рассуждениях о возможной поставке проблематики (я не говорю что у меня есть готовое решение). Но запретительной статьи именно на невозможность построение терма индукции (или Sigma типа выраженного только на Pi) в CoC + predicative hierarchy of universes, насколько я знаю не существует. Или, если он возьмется за $100/час на 4 часа ее расписать (показать что не существует во всех кодировках (в статье только за Черч Нумералы идет речь, т.е. кодировка без конгруэнтности например), чтобы это не была белетристика или Дилберт в картинках), я с радостью заплачу назамедительно сумму (за 4 часа) и признаю что я нижайший пидоро-червь на планете :-)

Вот линк статьи:
http://www.cs.ru.nl/~herman/PUBS/IndNonder.ps.gz

http://maxim.livejournal.com/485410.html