我在2016年4月的博客《希尔伯特梦后百年》提出希尔伯特纲要的目标并未被哥德尔证明击垮，而是基本实现了。并在微博（http://blog.sciencenet.cn/u/zhangbeijing）设置向正反方征求反响。虽然反响不大，但多数人仍让坚持希尔伯特之梦并未实现。

现在我发现了一个支持我的观点的佐证：

“从1950年起在数学哲学和逻辑学方面的文献中，这已成为一个普遍共识，即希尔伯特纲要不仅已经被哥德尔不完备性定理’杀死’，而且它如果不是一开始就考虑欠妥的话，就是过于野心勃勃了。尽管如此，在近来的文献中，出现了一些更积极的评价。这大部分原因是希尔伯特学派未发表的作品（尤其是希尔伯特课堂笔记）近年来得到了关注，……希尔伯特的哲学思想能够以怎样的方式得到拯救，这仍有待考察。从上一节的讨论中，无论如何都应该明确的是，那些与希尔伯特思想密切相关的成果已经取得了重大成功。……在过去半个世纪以来，证明论和希尔伯特的目标在更普遍意义上得到了巨大的推进。”

上段文字摘自《爱思唯尔科学哲学手册/逻辑哲学（上）/理查德 扎克：希尔伯特纲领的过去与现在》（北京师范大学出版集团，2015年12月，pp552-553）。

理查德·扎克的基本理由是算术体系结构的建立，但他只引证了几个公理系统（PRA等）-----算术公理体系结构当前的研究进展详情参见本人著作《证明方法与理论》（国防工业出版社，2015年11月），其公理名单如下，先后次序满足相容性≤关系:

(1) PFA

(2) EFA

(3) SEFA

(4) PRA

(5) RCA

(6) IΣ₂

(7) IΣ₃

(8) PA

(9) ACA₀

(10) ACA_{0+ ("n,X)(TJ(n,X))}

(11) ACA

(12) RCA₀ + TJ(w)

(13) ACA₀ + TJ(w).

(14) ACA + TJ(w).

(15) ACA₀ + ("x)(TJ(w,x)).

(16) ACA₀ + {("a,x)(TJ(a,x)):a<w^w}

(17) ACA₀ + {(a<w^w)("x) (TJ(a,x))}.

(18) RCA₀ + TJ(w^w).

(19) ACA₀ + TJ(w^w).

(20) ACA₀ + {("x)(TJ(w^w,x))}.

(21) ACA₀ + {("x)(TJ(a,x)):a<OE₀}

(22) $\Delta$ -CA

(23) RCA₀ + TJ(OE₀):  

(24) ACA₀ + TJ(OE₀).

(25) ACA + TJ(OE₀).

(26) ACA₀ + ("x)(TJ(OE₀,x)).

(27) {ATI(a):a< G₀}

(28) ATR₀

(29) ATI (<G₀).  

(30) ATR

(31)  ^Π-TI₀

(32)  ^Π-TI

(33) TI

(34) _ID2

(35) ID_<w

(36) ^Π-CA₀

(37)  ^Π-CA

(38) ^Π  -CA+TI

(39)  ^Π-TR₀

(40)  ^Π-TR

(41)  ^Π-CA₀

(42)  ^Π-CA

(43)  ^Π-CA+TI

(44) Z₂

(45) Z₃

(46) Type Theory.

(47) Weak Zermelo.

(48) ZC:Zermelo+Choice Axiom

(49) ZC + ("a< w₁)(V(a))

(50) KP (#)

(51) ZFC

(52) ZFC + strongly inaccesible.

(53) ZFC + strongly Mahlo

(54) ZFC + {strongly n-Mahlo: n< w}

(55) ZFC + ("n < w)(stronglyn-Mahlo)

(56) ZFC + (weakly compact)

(57) ZFC + (indescribable)

(58) ZFC + (subtle):ZFC +“there exists a subtle cardinal”.  

(59) ZFC + (almost ineffable):ZFC +“there exists an almost ineffable cardinal”.  

(60) ZFC + (ineffable).

(61) ZFC + {n-subtle: n < w}

(62) ZFC + ("n < w)(n-subtle).

(63) ZFC + kÆw

(64) ZFC + ("n < w₁)(kÆw)

(65) ZFC + 0#

(66) ZFC + ("x Πw)(x#):ZFC +“for all x containing omega, x# exists”.

(67) ZFC + kÆw₁.

(68) ZFC + Ramsey.

(69) ZFC + Measurable

(70) ZFC + Concentrating Measurable

(71) ZFC + Strong

(72) ZFC + Woodin

(73) ZFC + Superstrong

(74) ZFC + Supercompact

(75) ZFC + Extendible

(76) ZFC + Vopenka

(77) ZFC + Almost Huge

(78) ZFC + Huge

(79) ZFC + Superhuge

(80) ZFC + ("n <w)(n-huge)

(81) ZFC + Rank into Itself

(82) ZFC + Rank + 1 into Itself

(83) VB + V into V