В нескольких недавних публикациях я описал логику CWPL, предназначенную для моделирования рассуждений, содержащих кросс-мировую предикацию. Семантическая специфика этой логики состоит в том, что она базируется на кросс-мировой интерпретации предикатов. Для CWPL и ряда ее модификаций существуют исчисления генценовского типа. В данной статье предложено исчисление гильбертовского типа для одной из модификаций CWPL и предложена модификация метода канонических моделей для доказательства ее полноты.