形式化系统——数学或逻辑能力的局限？

 

        做否证是个“缺德”的事，有点那么“一将功成万骨枯”的韵味，也有点那么“舍我其谁，颐指气使”的嚣张劲。做“否证”，砸了一个行当，肥了一己之私。哥德尔，算不上空前绝后，但就影响，堪称深远。或许几千年来为人所迷惑，唯此君拨开云雾尚算不上经典，只怕数百年后，人人仍口口相传，其洞见历久弥坚，犹如笛卡尔，方可算一代大家。

        同所有的否证一样，尺规问题的代数化破灭了“三等分角”、“倍立方体”、“化圆为方”。哥德尔不完备定理也彻底让希尔伯特的“元数学”计划破产。GEB里不无有趣的调侃其“阿拉丁神灯”的段子。“愿望类型化”、“元灯”、“元怪物”、“元元怪物”……罗素的类型化从逻辑为基础重塑数学大厦，但应用到现实颇为繁琐，主流上，从集合论公理化（ZFC）解决了可怕的罗素悖论，数学大厦之基得以保全。虽根基得以幸免，然则疆域却被哥德尔硬生生给划拨了一块去了神秘的未知。数学、逻辑并非万能！

         人工智能先驱们也有彷徨，无论确定形式系统怎样的一集公理，其不完全皆已根深蒂固、先天决定。人，才是系统外洞察秋毫之神明。智慧，则潜藏在这洞察之中，这一集公理之外。马尔文·明斯基如是说：“感觉，而非逻辑，那正是智能之所在！”直觉主义与形式主义的PK似乎，这一段落下，笛卡尔之流这样的二元论者着实是占了上风。不得不感叹400年前，这位爱睡懒觉、“我思故我是”的先贤之深思远见。

        罗素、怀特海的《数学原理》仍被奉作今逻辑之正统经典，其规划的类型体系杜绝了悖论，逻辑之旁枝声势依然孱弱。达·斯科特的次协调逻辑在这众多派系中并不显眼。或许该成果只是专营之堆砌，但其大胆弱化矛盾律，抛弃司各脱律之创见，愚深以为然！！！如作者之比喻，关于几何平行第五公设之解禁，非欧几何，奇葩般绽放盛开。并非所有矛盾都是无意义的！这不正是黑格尔和维特根斯坦的哲学远见之所在吗？

        或许对待矛盾、悖论，我们换副眼镜，变个万花筒，智能是什么？这就更清澈了。

       

对哥德尔定理的一大误解是,歌德尔定理只对一阶谓词有效.但是计算机未必是使用一阶谓词的.

高阶逻辑 没怎么深入。查过维基，只知道有些什么不相容的，不是太明白。

难道高阶逻辑 就能有“智慧”了吗？觉得高阶逻辑不过类型论化而已。请赐教！

事实上这里说的未必是一阶逻辑，是指非一阶逻辑.可以是经典逻辑,也可以是非经典逻辑.
当然，人工智能是否能够用逻辑进行形式化构造,现在基本是否定的.但是这个否定的原因并非来自歌德尔定理.

还想请教否定 人工智能逻辑形式化的 原因 究竟是什么呢？

BTW，上次那本《美德的起源》着实不错。

找到了思路契合者:

罗素悖论——哥德尔——次协调逻辑——佛学浅谈
http://www.cnblogs.com/SawAngel/archive/2004/11/21/66677.html

似乎否定 人工智能逻辑形式化 可以从这里看出些缘由：
http://www.phil.pku.edu.cn/cllc/archive/papers/logic/LiuXiaoli_logicLimitsOfAI.pdf