Coq & ProofWeb

在ProofWeb的主页http://prover.cs.ru.nl点击按钮 ,然后在Select a saved file to load:中选择tarski-hg.v,然后在下面的下拉框中选择Coq,点 ,就可以看到Tarski’s Fixed Point Theorem的形式化证明过程,这个证明过程可以作为Coq和ProofWeb的一个不错的demo。

Zorn’s Lemma

Suppose a partially ordered set has the property that every chain (i.e. totally ordered subset) has an upper bound. Then the set contains at least one maximal element.
如果一个偏序集P中的每一个链C(即全序子集)都有上界x(x当然必须属于P),那么该偏序集P至少包含一个极大元。

Zorn’s lemma is equivalent to the well-ordering theorem and the axiom of choice, in the sense that any one of them, together with the Zermelo–Fraenkel axioms of set theory, is sufficient to prove the others.

Zorn’s lemma is equivalent (in ZF) to three main results:

    Hausdorff maximal principle
    Axiom of choice
    Well-ordering theorem

Moreover, Zorn’s lemma (or one of its equivalent forms) implies some major results in other mathematical areas. For example,

    Banach’s extension theorem which is used to prove one of the most fundamental results in functional analysis, the Hahn–Banach theorem
    Every vector space has a Hamel basis, a result from linear algebra
    Every commutative unital ring has a maximal ideal, a result from ring theory
    Tychonoff’s theorem in topology

In this sense, we see how Zorn’s lemma can be seen as a powerful tool, especially in the sense of unified mathematics.

感官感受能欺骗我们么?

有人认为,来自感官的感觉可能会欺骗我们,因此通过感官感受获取的认识都可能是虚假的。这种说法非常误导。

想要受骗,必须具备受骗的能力,而受骗能力则依赖于你有哪些先入为主的偏见。仅当你拥有一个解释感官感觉的理论,才能具有受骗的能力。如果你完全没有任何经验知识,就没法受骗。这种情况下你从感官获得的经验仅仅是一堆零散的感官感受,跟本谈不上受骗与否。发现自己受骗实际上是发现了自己关于经验世界的理论模型失效。感官经验本身并不能欺骗你,只有你从以往经验建立的理论模型才会欺骗你。例如,尺寸相同的情况下,浅色的物体看上去比深色的物体大一些,但如果你之前对自己的视觉大小和物体的尺寸之间的关系毫无概念,你根本不知道尺寸大小的比较和视觉大小的比较之间有什么关系,那么你就不会上当。只有当你心中有这样一个理论:看上去较大的东西实际尺寸也较大,你才会被你的视觉欺骗,以为浅色的物体更大。

恰当的问题

如果你得到一个问题的答案,那么至少要在面对一个答案时有能力判断它是否回答了你的问题。如果连这都做不到,那么这个问题就没必要问了,因为无论给你什么答案你都不知道它是否回答了你的问题。所以,在提问之前不妨先问问自己,自己希望从问题的答案中得到什么,弄清楚满足什么条件的答案才会让你认为自己心中的疑惑被这样的一个答案解决了。这一点如果不能明确,哪怕上帝跳出来直接把答案告诉你,也解决不了你心中的疑惑,如果这样还不如不问。

比方说『意识是什么』这个问题就并不像看上去那么有价值,因为『意识』本身就不是一个有明确含义的概念,在日常语言中在不同的语境下有许多不同的含义。对于这样一个有歧义的概念,无论什么样的答案都难以判断是否回答了问题。因此直接去问意识是什么,还不如先弄清楚意识有哪些不同的明确的含义,然后选择其中若干明确的含义去提问。

黑洞——要么无法形成,要么不会蒸发

我在JCAP上发表了一篇文章:Black hole — never forms, or never evaporates
链接: JCAP, arXiv, DOI, Scholars Portal Journals

这是我手中未经JCAP排版的最新版本,纠正了一些笔误和语法错误:Black hole — never forms, or never evaporates

除了结论,文中还给出了Einstein Field Equation最一般的球对称解,任何球对称解都是其特例,包括Schwarzschild,Reissner-Nordstrom,静态流体球,除此之外还覆盖了所有非真空的有径向运动的情况。

目前已知的引用:
Christian Corda and Herman J. Mosquera Cuesta, Irreversible gravitational collapse: black stars or black holes?

讨论:
Physics Stack Exchange: If blackhole never forms, how important will be to study blackhole paradoxes