Re: Раз уж зашёл, обозначу присутствие
В точном смысле "констуктивной математики" там, конечно, ничего не доказать. В смысле же интерпритации - таки да - модель строится из формул (точней - констант, которые этим формулам соотвествуют). Просто непонятно, какой смысл при этом остается у "конструктивных" философствований, когда и так известно, что формально доказать непротиворечивость нельзя - хоть конструктивно, хоть в ZF, а никаких метафизических бесконечностей и прочей лабуды в счетной модели нет.

PS: Если интересно, могу доказательство из Коэна закинуть - оно всего на страничку и он у меня есть в электронном виде