作者：Doraemoe

抛弃文件夹！用Plex来管理你MAC下的视频!

Update(2012/5/9): 有鉴于字幕的支持问题，我现在切换到XBMC上了，这篇文章不少地方还适用，不过要补充几点：

1. XBMC支持自定义字体，但是需要将字体文件放入~/.xbmc/temp/fonts文件夹下。另外不知为何，我这里需要将这个文件夹设为只读才可以，否则每次播放文件这个文件夹会被清空。

2. 最新稳定版的XBMC（11.0 eden）不支持10bit视频，但是Nightly版支持，另外预定在下一个稳定版时会支持。
 12.0已支持（2013/02/12）

3. 对于电视剧即使其本身只有只有一季，在文件名里也必须写上S01而不能省略。详细的命名规则在这里。

Update(2012/5/26): 对于iOS版的XBMC，可以将ASS字幕所用字体放入/private/var/mobile/Library/Preferences/XBMC/temp/fonts下（没有就自己新建一个）。不过需要注意的是，对于大码率的视频，带特效的字幕会导致拖慢，这个恐怕除非以后硬件升级，是没有把法解决了。另外使用共享功能观看计算机上的视频我推荐使用这个软件可以使用系统自带的AFP(Apple)或SMB(Microsoft)共享方式，比较方便。其他的使用指南网上有很多，我就不再复述了。

Update(2012/5/29): Nightly版的XBMC现在已经支持BD原盘的HDMV menu功能，只要打开BDMV文件夹下的index.bdmv文件即可，但是仍旧有不少Bug，也不支持BD-J和BD-Live，Windows用户 还是使用TMT或者PowerDVD作为外挂播放程序比较完美，至于MAC用户嘛…去装个Windows吧… 12.0正式版对HDMV Menu的支持有所改善，但仍旧不完美，另外仍旧不支持BD-J和BD-Live（2013/02/12）

Update(2012/7/18): 在iOS上播放如果连普通的字幕都会拖慢，可以考虑安装nightly版本，对于字幕的处理效率比起正式版有了本质的提高。 12.0已解决（2013/02/12）

============================

不知道有多少人和我一样已经习惯了用库来管理自己的文件，iTunes，Papers，iPhoto。之前还嫌他们巨大而又笨拙，但是当习惯之后却再也不想回到用文件夹来管理文档的低级工作中去。那么上面的3个软件分别对应于音乐，论文，照片。但是显然的，我们还有一个重要的类别没有被包含在内，那就是视频。Plex是Mac下一个出名的视频管理软件，不过大部分人应该只把其当作了视频播放器来用。如果只是把它当作视频播放器的话这个软件未免显得太巨大了一点，并且它大部分的功能都没有利用到。那么经过两天的初步摸索，就让我来介绍一下使用Plex管理视频文件的心得体会吧~以下内容适用于Plex的0.9及以上版本，以OS X10.6.6作为运行平台，不过Plex之前放出了Windows版，所以以下内容应该也是部分适用于Windows。

首先要说明的是Plex的管理功能相较于iTunes之类还是稍显麻烦，上面的3个软件你并不需要关心文件夹是否整齐，文件名是否合适。但是显然Plex现在还不是那么的智能，所以我们还是要先从最基本的文件夹和文件名开始整理起，以备Plex的Media Server使用。

对于文件夹的设置，我们需要将电影和电视剧放置在不同的文件夹下，并且，不同的电影和不同的电视剧放在不同的文件夹下。也就是说一个片子一个文件夹，并且电影放到电影的文件夹里，电视剧放到电视剧的文件夹里。接下来就是文件的重命名了，如果说文件夹的问题还好说，那么文件的重命名就绝对就是一大讨厌的事的，特别是对于电视剧而言，动辄十几到几十集，难道我们还要一集一集的更改文件名么？复杂重复的工作自然就要交给机器来做！这时后我们就要请出Apple系统中自带的Automator了。在应用程序中打开Automator，选取服务作为工作流程的模版，在右侧上方将服务接受选定的…改为文件和文件夹，从左侧添加一个“给Finder项重新命名”到右边，它会提示你是否要创建副本，我们选择不添加（当然你要是觉得不保险也可以选择添加，不过仅仅是重命名，问题应该不大）。之后按照图上的样式设置一下就可以了。

Photobucket

接下来只要保存这个工作流程，给它取个名字就可以了，我这里叫做批量重命名。

之后就是批量选择你想要重新命名的文件之后点击鼠标右键，在菜单的下方应该就可以看见刚才保存的那个服务了吧：

Photobucket

点击之后会弹出一个对话框，此时我们就可以按照“剧集名称 – S季数E集数”的格式来修改文件名了，左下角会出现名称的预览，确定前先看看中不中意吧：

Photobucket

好了，点击继续，你就会发现所有文件名都已经更改成功了！（耶~~）

如果是电影的命名，则相对而言容易一些，只需要更改为“电影名 (年代)”就可以了，比如说
The Dark Knight (2008).mkv

如果你的电影文件分为多个部分（这个在几年前很常见）就需要先将保存这个电影的文件夹按照上面的模式重命名，之后再将每个文件命名成形如
The Dark Knight Pt1.avi
The Dark Knight Pt2.avi
的样子就可以了。

折腾了这么半天，我们终于做好了准备工作。的确，就这而言Plex还大有需要改进的地方，我们就期盼制作小组们可以在下一个版本里做出改进吧。

那么之后就是安装Plex了，从http://wiki.plexapp.com/index.php/Downloads 下载最新的0.9版，安装好之后打开就会出现配置界面，这里我就直接盗用官网的图片了：

Photobucket Pictures, Images and Photos

第一个是让你设置电影的文件夹，第二个则是电视剧，最后一个就是音乐，因为我还是倾向于用iTunes来管理音乐，最后这一步我就Skip过了。

安装好了之后在菜单栏就能看见如图所示的图标，那就是Plex Media Server，并且它会自动开始扫描文件。

Photobucket Pictures, Images and Photos

等它扫描完成之后我们就可以察看结果啦~
Photobucket

怎么样，看上去还不错吧。对于每部片子，还可以察看全片的简介和每集的简介（如果有的话）：

Photobucket

Photobucket

封面图，背景图会自动下载，现在看来这个数据库还是挺全的。

之后我们就可以打开Plex了，从Plex里进入剧集浏览界面后会自动播放片头音乐（部分，原理未知），并且会显示媒体分辨率，编码等信息：

Photobucket

至于软件本身的设置大家可以自己摸索，如果需要显示外挂字幕的话需要在Preferences–视频–字幕里将字体调为Arial Unicode MS，字符集可以默认，之后将字幕用文本编辑打开后另存成UTF-8编码的格式才行。

Photobucket Pictures, Images and Photos

不要问我为啥只能用该死的Arial，我也想知道。MKV的内封字幕不用管，软件会自己加载。另外播放的时候也可以按M键调出菜单，有兴趣的就请去看看吧~

说了这么多好处，现在来说说缺点吧。首先需要手动改名绝对是一大坑爹的事啊，虽说对于0Day的命名格式这个软件可以自己识别，但是如果是按照国内字幕组的命名格式的话这软件就直接呈天然呆状了，字幕也是个问题，普通的srt字幕倒是没啥大事，但是对于有着各种特效的ass字幕显示效果就不那么尽如人意了。所以虽然我标题写的野心很大的样子，不过实际上现阶段这个软件还有不少的路要走，恐怕我也还没办法在这一个软件里实现全部我所希望的视频功能吧。

最后，如果想要看看详细的软件使用指导，可以去Plex的Wiki页面察看，当然是英文的。

我知道你不知道我知道你知道

技术宅结城浩写了几本Java，C，Perl的书后估计是觉得程序猿的钱不好赚，于是打起了宅们的主意，一本数学少女就这么红起来了。第一次听说这本书还是大一，听介绍还挺有趣的，可惜当时没有中文版，真正看到还是几年后的事了。前些日子听说这书居然还出系列了，并且还漫画化了，我该说11区已经没有救了么。看了漫画第一话的内容，居然是经典的泥孩子问题，上次说到的模态逻辑和可能世界理论正巧能够用的上，那么既然上次只是很简单的说了一下大概，这次借这个机会我就再多说两句好了。

泥孩子问题是这样的：

想象一下有n个孩子在一起玩，他们的母亲告诉他们如果他们弄脏了自己，后果会很严重。所以，理所应当的，这些孩子不愿意自己变脏，但是却非常乐意别人变脏（这腹黑的……）。现在，我们假设在这n个孩子中有k个在玩的时候弄脏了他们自己的额头，每个人都能看到其他人的的额头但是不能看到他们自己的额头。所以，没人会坦白他看到了什么。当然为了不至于回家后面对不知道是什么的“很严重的后果”，他们一起来到了父亲那里。这个父亲显然也不是省油的灯，他并没有直接告诉这些小孩他们头上有没有泥巴，只是说了“你们之间至少有一个人头顶有泥巴”。之后这个父亲就一遍又一遍的问“你们知道自己头上有泥巴么？” 我们假设所有小孩都足够聪明，诚实，并且他们总是同时回答，那么将会发生什么？

我们先假设只有3个孩子，那么如果我们用一个三元组(q_1, q_2, q_3)来表示这三个孩子的状态，以0或1分别表示某人头上没有或有泥巴，则我们知道所有的可能世界有8种：（0，0，0），（1，0，0），（0，1，0），（0，0，1），（0，1，1），（1，0，1），（1，1，0），（1，1，1）。如果我们把“0个孩子头上有泥巴”，“1个孩子头上有泥巴”，“2个孩子头上有泥巴”，“3个孩子头上有泥巴” 分成4组的话，我们可以画出下面的这副图M_0：
Photobucket

其中每个点代表一个可能世界，这个可能世界的状态则被标注在旁边，那么边是按照什么规矩连接起来的呢？从数值上讲，是连接有且仅有一位与起始点不同的点，所以（1，0，0）可以连接（1，0，1），（1，1，0），（0，0，0）而不能连接（0，1，1）因为他们有3位不同而不是一位。从含义上来讲，由于某个点代表着一个可能世界，则和它连接的点就是这个可能世界的所有可能世界，但是这里稍微有点复杂，因为这些可能世界是从不同人眼里出发得到的可能世界。回到具体的含义上来，（1，0，0）代表了孩子A头上有泥巴而孩子B，C上没有，那么这个世界中，由孩子A看来，他知道B和C头上没有泥巴，但是不知道自己头上有没有泥巴，所以A的所有可能世界是（1，0，0）和（0，0，0）。同理，B的所有可能世界则是（1，0，0）和（1，1，0），C的就是（1，0，0）和（1，0，1）。

那么为了明确区分到底是谁眼里的可能世界，我们在每条边上对此做出标示，则这个图就可以变为M_1：
Photobucket Pictures, Images and Photos

所以在他们的父亲说任何话之前，所有可能世界和他们的关系就如上如图所示。但是，当父亲说：“你们之间至少有一个人头上有泥巴”的时候这些可能世界就发生了变化，（0，0，0）变成不可能的了，所以就成了这样，图M_2：
Photobucket Pictures, Images and Photos

此时，如果只有一个孩子头上有泥巴，那么头上有泥巴的那个孩子则必然知道自己头上有泥巴，而另外两个孩子则仍没有足够的信息来确定是否自己头上有泥巴。为什么呢？我们假设此时的世界是（0，0，1）那么以这个世界为基准，对于A而言虽然他不知道自己所在的世界，但是通过观察其他的两个孩子，他可以知道自己必定在（0，0，1）和（1，0，1）这两个世界其中之一，但是这两个世界里A头上有没有泥巴是不一样的，所以A无法判定自己头上有没有泥巴，B同理。唯独C在这里除了（0，0，1）外不存在其余的可能世界，所以对于C而言，他可以确定自己头上一定有泥巴。到这里，我们可以说，如果孩子们可以判断在所有可能世界里，自己头上有没有泥巴这件事情况都是一样时，他就可以确定自己头上有没有泥巴了。

那么数学上我们如何表示？在这里我们最终要推出的是A，B，C知道自己头上有（或没有）泥巴，于是如果我们用p表示自己头上有泥巴，q表示自己头上没泥巴，那么p，q就是我们常说的命题（一个能区分真假的语句），K_A，K_B，K_C分别表示A，B，C知道，我们把它们叫做模态算子。则K_A p的含义就是A知道自己头上有泥巴，如果我们再加入\lnot来代表否定，那么K_A \lnot K_B p就表示A知道B不知道自己头上有泥巴。当然这么下去也可以造出像标题一样绕口的句子，不过把人绕晕乎是没有任何好处的，就在此打住。所以上面提到的（0，0，1）世界的情况，我们就可以写为：

  • $$(M_2, (0, 0, 1))\models \lnot K_A p$$
  • $$(M_2, (0, 0, 1))\models \lnot K_B p$$
  • $$(M_2, (0, 0, 1))\models K_C p$$

这些式子的含义是，在图M_2所示的情况下，当世界为（0，0，1）时，A，B，C三者的知识情况，言下之意就是当世界为（0，0，1）时，A，B一定不知道自己头上有没有泥巴，而C一定知道自己头上有泥巴。

回到最初的问题，如果世界不是（0，0，1）而是（1，0，1）呢？(M_2, (1, 0, 1))又能得到什么？此时我们可以看到，无论是A，B，还是C，在（1，0，1）这个世界下，对于他们自己的总有另一个可能世界，在那个可能世界中自己头上有没有泥巴是不一样的，所以要是这样，他们都不会知道到底自己头上有没有泥巴，于是三人都会回答：不知道。这时情况又起了变化，当所有人回答不知道时，这就意味着必定存在着两个或两个以上的人，他们头上有泥巴，于是这个世界又变成了M_3:
Photobucket Pictures, Images and Photos

此时，除了对于B而言还存在两个可能世界以外，A，C均只有一个可能世界，所以在图M_3的情况下我们有：

  • $$(M_3, (1, 0, 1))\models K_A p$$
  • $$(M_3, (1, 0, 1))\models \lnot K_B p$$
  • $$(M_3, (1, 0, 1))\models K_C p$$

那么，当世界是（1，1，0）时也可以“同理可得”，就不用多说了吧。如果你对这些感兴趣，可以另外参考MIT出版的Reasoning About Knowledge，上面说的很详细，当然数学上也要严谨的多。

TNND，回头看这文的时候突然反应过来，这泥马的拿手摸一下不就知道有没有泥巴了，还弄得这么麻烦，搞数学的还真是没事干啊。

GEB读书笔记之二——形式系统的相容性

上次说到了形式系统大概是个什么样子，不过光用语言描述总是很抽象的，不好理解。那么就来举一个书上给出的例子来看看：

pq系统

  • 字符集：p   q    –
  • 公理：设 x 是包含且仅包含一个或多个字符’-‘的字符串，则 x-qxp- 是这个系统中的串。
  • 推理规则：设 x，y，z 的含义如上 x 所述，如果 xqypz 是这个系统中的一个串，则 x-qypz- 也是这个系统中的串。

这个系统就是这样了，字符集和公理应该很好理解，至于最后的推理规则，虽然不难，但是对有些人可能看上去有点陌生。这种形式的定义我们一般称之为递归定义，至于递归的含义，有一个关于它的经典笑话：

     递归 [名词]：见递归。

这个笑话很形象的描述了递归的一个特点：自己定义自己。这听上去有点坑爹，自己定义自己不是说永远没完么？是的，所以递归的定义和这个有区别，自己定义自己没错，但是重要的一点是：定义用的是简单一些的版本，并且，起点是给定的。那么在这里，起点就是已经是系统中的，形如 xqypz 的串。那么这种串又是哪来的呢？向上看，这种串是由公理给出的。如果要再举一个例子的话那就是数学里著名的斐波那契数列，我们将这个数列的第 i 个数表示为 Fib(i) 则我们有：

  1. Fib(0) = 0
  2. Fib(1) = 1
  3. Fib(n) = Fib(n – 1) + Fib(n – 2)     (n > 1)

是不是很类似呢？好了，理解了这个我们就可以先来试试看看 pq 系统里都有哪些字符串。最简单的当然是当 x 只是一个 – 的时候，那么按照公理,字符串 – -q-p- 就可以算一个。之后由于有了这个串，我们就可以按照推理规则进行扩充，在这里，x 是 – -，y 是 – ，z 是 – ，所以扩充后就会变为 – – -q-p- – 。数一数，不要眼花了哦。按照这种想法，我们就可以生成不计其数的这个系统里的字符串。那么也许你很快就注意到了，所有的字符串，无论它们有多么长，长相都会是形如 “一堆横杠后面跟着一个q，q后面再来一堆横杠，之后连着一个p，p之后再有若干个横杠，结束”  凡是不是这个形式的串，肯定不会是这个系统中的串。于是我们把这种形式的串叫做良构的（Well-Formed）。这也是之前所说的特定的排列顺序，这是由规则决定的。

那么我们知道了只有这个形式的串才有可能是系统中的串，但是这并不意味着凡是这种形式的串都是这个系统中的串。那么有没有什么办法来判定任意这种形式的串是不是这个系统中的串呢？这个并不难，如果你愿意考虑一下的话可一先停在这里。如果你写了足够多的串，那么应该可以发觉这些串都有一个相似的性质，这个性质就是在字母 q 前的横杠个数等于在q，p之间的横杠个数与 p 之后的横杠个数的和。换句话来说，这个系统和加法有着异曲同工之妙。如果我们把q解释为等于，p解释为加法，- 解释为数字1，- – 解释为数字2，等等，我们就可以把这个系统中的每一个串翻译为一句形如“3等于2加1”之类的正整数加法等式，我们把这个叫做形式系统的解释，而正整数加法和这个形式系统的关系我们称之为同构，就如同“苍井空.rmvb”和显示器上的图像的关系 就如同“爱情买卖.mp3”和从你音响里发出的噪音音乐一样。那么，解释是唯一的吗？答案是否定的，如果稍加考虑我们就可以给出另一个解释：对于横杠的解释不变，但是将 q 解释为减法，p 解释为等于。虽然我们改变了解释，但是这个系统仍旧可以解释的通。

刚才说到了“可以解释的通”，这实际上就涉及到了形式系统的一个重要性质：相容性。或者叫无矛盾性，一致性。显然的，有矛盾的东西对于我们而言价值不大，我们想要的系统理所应当应该是无矛盾的。书上将这一性质分成了两层，外部一致性和内部一致性，外部一致性比较好理解，它指的是系统中的每一个定理（在pq系统中就是那些公理和由推理规则生成的串）经过解释后都成为一个真的陈述。即所有系统中的陈述都与外部世界相符，这里的外部世界自然就是我们的世界了。而内部一致性则是指系统中不存在两个或更多的定理，他们之间是彼此不相容的。一个最简单的例子就是如果一个系统中同时有“小明今天早上造的桌子A是方形的”和“小明今天早上造的桌子A是圆形的”，那么这个系统就是内部不一致的。因为虽然我们也许不知道小明今天早晨造的桌子A是什么样的（甚至小明到底会不会造桌子我们也不知道），但是我们可以肯定这个桌子不可能既是方的又是圆的。这其实就是我们判断一个系统是否是内部一致的过程：我们先想象一个世界，这个世界要尽量符合这个系统内的所有定理。像上面，我们想像一个存在小明的世界，并且这个小明能够造桌子，但是我们再怎么想也想不出一个桌子要怎样才能即是方形的也是圆形的，所以我们说这个系统不是内部一致的。换句话说，如果这两个命题是“小明今天上午睡觉了”和“小明今天下午跑步了”，我们就可以想象出一个世界，在这个世界里小明上午睡觉了并且小明下午跑步了，所以我们说这个系统是内部一致的。需要注意的是现实世界里小明到底做了什么无所谓，在内部一致里，只要在我们的一个想象的可能世界里所有的陈述之间没有冲突就可以了。

不过想象的可能的世界这种说法有点坑爹，我偏要想一个桌子即是圆的又是方的的世界你能把我咋地？（好吧，其实我承认我想不出来）作者给出的结论是说想象的世界要和真实世界的数学和逻辑相一致才行。不知道多少人愿意就这么算了，凭啥只是数学和逻辑，物理呢？生物呢？化学呢？语文呢？政治正确性都不顾了你想死么？所以这里就让我多解释一下。不过这里要牵扯到模态逻辑和可能世界理论，当然只是初步的。首先在一般的逻辑里，一个命题（能够判断真假的语句）的表述方式无非有两种：直接表示和添加否定的表示。但是在模态逻辑里，增加了“可能”和“必定”两种“形容词”，也就是说，一个命题，比如“Sony是业界的良心” 在一般的逻辑里顶多可以再表述为“并非Sony是业界的良心”。而在模态逻辑里，还可以表示为“有可能Sony是业界的良心”和“一定有Sony是业界的良心”。虽然这些命题的真假在你看来可能取决于考虑问题的人是任青，索匪，还是果粉（？）。但是在可能世界理论之下，我们如何定义这些命题的真假呢？下面以一定为例，解释真值是如何定义的。

     命题 A 在某一可能世界里是必然的,当且仅当 A 在那个世界的所有可能世界里都是真的

由此可见，首先在判定一个以一定开头的命题的真假时，我们会限定说它在某一基本的可能世界里。之后，我们说如果在那个可能世界的所有可能世界里这个命题都是真的，那么原命题为真。这里稍微有点绕，那么来举个例子好了：我们首先限定我们当前的世界是讨论问题的基本的可能世界，那么这样的话“任天堂是游戏业霸主”的世界，“索尼是游戏业霸主”的世界，和“苹果是游戏业霸主”的世界，就是我们当前世界的可能世界，但是“雅达利是游戏业霸主”的世界就不是我们当前世界的可能世界了，因为它已经死了。（现在的雅达利和以前的没什么关系，就像现在的AT&T和以前的AT&T不是一回事一样）

所以说，在这里，提到可能世界，我们总有一个基准，“所有可能世界”不是指绝对意义上的所有可能世界，而是与基准世界相关联的所有可能世界。如果某一个可能世界里的规则与基准世界里的规则相矛盾，那么这个可能世界就不是我们想要的可能世界，他对于我们没有意义。所以回到主题，在内部一致性里，我倾向于把我们现实世界当作基准，那么如果存在一个在这基准之上的可能世界，在那个世界里系统中的所有定理的解释之间都不存在矛盾，则我们说这个系统是内部一致的。所以此时一个“桌子同时是方的和圆的”的可能世界就不是一个可以被接受的可能世界了，因为在基准世界（我们的世界）里，这是不可能的。

好了，那么关于形式系统的相容性大概就是这么多了，下次应该就是关于形式系统的另外一个重要性质了。下一次应该可以和哥德尔扯上关系了……吧—_卅……

GEB读书笔记之一——形式系统初步

之前开始学数理逻辑的时候听说了《哥德尔，艾舍尔，巴赫》这本书，不过实在是太忙，这书又很厚，结果最后并没有去看。前两天看到Twitter上有人提到这本书再版了，正好现在放假无事，于是便到书店把这本书买了回来。要说这本书里讲到的哥德尔不完备性定理，可以说是上个世纪人类最为伟大的发现了，不过似乎听说过的人并不多，这的确很可惜。译者在前言里称这本书是一本奇书，我觉得不虚此言，总之看的我是非常的兴奋。所以作为看书后的回顾，这里就记录一些阅读后的感想，供自己作为回顾以及没时间看书又想稍作了解的人。

在谈论哥德尔伟大的定理之前我们需要了解一些基本的概念，首先就是形式系统。不过在解释什么是形式系统之前请让我们回想一下初中学过的几何。如果你用过人教2000年版的初中数学书的话你一定还记得那本和代数一样厚（或者反过来说也一样）的几何，里面充斥着诸如“公理”“定理”一类的表述。如果你和我一样对这些表述并不以为然并且认为它们基本上是一回事的话，那么恭喜你，你和我一样犯下了一个严重的错误。不过这个错误并不会影响到你的中考或者高考成绩，所以大概从考试的角度来说这并不严重。但是如果我们要讨论形式系统的话我们还是先搞清楚这两个词是怎么回事。

首先是公理：

公理是无法被证明或决定对错，但被设为不证自明的一个命题。

也就是说，公理是一切证明的起点，它被视为是理所应当的。所以，公理应该是一些简单的，而且符合直觉的陈述。那么回过头来看看我们当时几何，也就是欧几里德几何中的那些公理：

  1. 任意两个点可以通过一条直线连接。
  2. 任意线段能无限延伸成一条直线。
  3. 给定任意线段，可以以其一个端点作为圆心，该线段作为半径作一个圆。
  4. 所有直角都全等。
  5. 若两条直线都与第三条直线相交，并且在同一边的内角之和小于两个直角，则这两条直线在这一边必定相交。

是不是很浅显易懂并且你会认为是理所应当的？当然了，你可能看着第5条公理不是那么的浅显易懂，是的，欧几里德也这么想，很多人都这么想，以至于由这条公理生出了其他的几何学说！这个我们之后再说。最后一个公理的一个等价表述其实是“通过一个不在直线上的点，有且仅有一条不与该直线相交的直线。”这个是不是稍微浅显一些？

那么定理呢？

定理是经过受逻辑限制的证明为真的陈述。

也就是说定理与公理都是真的,但是两者最大区别是定理需要证明。那么所谓的经过受逻辑限制的证明又是什么东西？与其找个解释，我想我们不如直接来看看欧几里德是怎么证明其几何中的定理的：

定理1：通过一个已知有限长的直线可以作一个等边三角形

Photobucket

设AB是已知有限直线

  1. 以A为圆心，以AB为距离画圆B\Gamma\Delta 。 (公理3)
  2. 以B为圆心，以BA为距离画圆A\Gamma E 。 (公理3)
  3. 由两圆的交点\Gamma向A，B连线。\Gamma A，\Gamma B (公理1)
  4. 因为点A是圆B\Gamma\Delta的圆心，所以AB=A\Gamma。
  5. 因为点B是圆A\Gamma E的圆心，所以BA=B\Gamma。
  6. 因为已经证明了A\Gamma=AB，所以B\Gamma，A\Gamma都等于AB。
  7. 所以三条线段B\Gamma，A\Gamma,AB彼此相等。
  8. 所以三角形AB\Gamma是等边的，即在个已知有限长的直线AB上作出了一个等边三角形。

好了，证明结束，我想如此简单的证明不会有人看不懂吧，那么现在我们回过头来看看这个证明是怎么做到的。前3步是之前提到的公理，是最基本的东西，我们可以直接这么做而不必多加考虑，因为理智告诉我们这样一定没错。而4-6步呢？他们都是“因为…所以…”的句式，这个句式告诉我们，由于“因为”给出的前提条件，可以得到“所以”当中的结论。并且，如果“因为”所说的是正确的，那么，“所以”当中的结论也一定正确。在这里，这个正确性是显然的（好吧，我知道有些数学证明的一个偷懒技巧就是在不会证的时候写“显然可得”但是我相信这里的结果对于任何一个心智正常的人而言都是显然的）。这其实就是一种逻辑：当你接受前提“因为”时，你就要接受结果“所以”。而到了第7步，则是由第6步的结论而自然得到的结果。最后，在第8步，由于有了上一步的结论，我们得到了我们想要有的那个三角形。

这就是一个典型的证明过程，由逻辑将一些正确的事物连接到一块，并且，得到另一个正确的结论，再而且，这个过程被我们的理智所认可。到这里就比较好玩了，我们有了公理，有了逻辑规则，而且这些东西看上去又相当有规律，那么是不是我们可以弄出一套东西来，这套东西里有公理，有规则，然后只要通过公理和规则进行推理，那么就能得到有用的结论呢？特别的，这套东西最好能让机器来做，我们把公理和规则输入进去，机器来给我们给出源源不断的正确结论，要是这个系统要是能够包含一切的现实规律，那就更好了。这样我们就可以放手让机器去给我们创造一切，我们自己就可以活在没有饥饿没有寒冷的新闻联播的世界里了。我X，想想就给力啊！

是够给力，而这个的实现便是数学中的形式系统。欧几里德几何本身已经有那么些形式系统的意思了，比如说作为基础的公理，比如说严密的逻辑推理。不过并不够，欧氏几何的推理是由自然语言做的，虽然已经足够简单，但是还是不够简单，并且，自然语言的复杂性，二义性也不是可以轻松就发觉的。另外，还记得那个看上去不怎么顺眼的第五公理么？历史上有不少人想要证明这个公理可以不用，大量的尝试竟然衍生出了其他的系统，比如说椭圆几何，仅仅将第五公理所说的“过直线外一点有且仅有一条直线与之平行”否定为没有直线与之平行，再加上其他的4公理，就能推出一套自己的系统。这样初看会觉得造成了系统的矛盾，但是让我们想一想，我们会觉得矛盾的原因是什么？关键就是在欧氏几何中提到的“点”，“线”这些东西，我们要怎么解释？这个问题可能有点奇怪，“点”就是点呗。但是如果我们跳出“点”这个词给我们固有印象，假装把它当作一个没有意义的符号（或者干脆换个不认识的字，免得我们潜意识里的联想，比如用“齾”），然后重新进行解释，我们就会发现，如果把“点”解释为球上直径的一对端点，把“线”解释为以球直径做为直径的球面上的圆，一切就迎刃而解了，此时公理1“任意两个‘点’可以通过一条‘直线’连接”是不是也能解释的通？两条‘线’不可能无交点是不是也能解释的通？也就是说普通的点的概念并不是这里“点”的唯一解释！那么是不是说我们可以抛弃这些具体的概念，而是使用一些抽象的，和具体现实无关的词汇，而在使用时根据需要给这些抽象词汇予以解释呢？是的，而这正是形式系统所要做的。

那么按照上面的想法，让我来叙述一下什么是形式系统。

首先我们需要一个抽象的符号集合，从某种意义上讲，符号和现实生活的联系越少越好，免得使我们产生不必要的联想。但是实际上，形式系统在怎么样也是要实用的，所以其中符号还是难免要和现实紧密联系起来，免得在我们的理解上造成太大的麻烦（你能想象一个充斥着“棏彎嗄齾”之类完全看不懂的字的一个系统么？）

其次，一套文法。我们要知道如何将这些符号按照一定的规则组织到一起。胡乱堆放到一起的字符是没有意义的，他们的顺序需要有规则来确定。

然后是上面已经提到多次的公理–推理的基础。还有推理规则，这些规则一般是非常简明的，足以让机器也能实现的“死”规则

最后，有了上面的东西，我们可以得到一些定理，这些定理的集合就是这个形式系统的理论。

需要再次强调的是，形式系统里的字符是高度抽象的，所以，任何想当然的结论都是危险的，例如，如果形式系统公理中有a+b，这并不意味着b+a也是公理，而是需要证明的，因为+并不是加法，而仅仅是一个符号。对于符号的解释是之后按照我们的需求，或者对这个系统本身含义的观察得出的。并且，解释也不是唯一的。

这样我们就对形式系统有了一个初步的了解，之后我会举例说明一个书上的讲到的简单的形式系统，以及容易产生的误解。当然还有形式系统的两个重要性质。听说文章太长了没人看，所以这些就推后吧。

同人？

在ACG的圈子里面呆的久了，即使不是那么的沉迷，也难免会接触到同人的作品。我对同人作品最初的理解仅仅是“对喜欢的作品的二次创作”，虽然不能说错，但是并没有包含所有的内容。按照维基百科的说法，同人是指“自创、不受商业影响的自我创作”，或“自主”的创作。也就是说重点在于自主，以及非商业。至于对喜欢的作品的二次创作则只是其中的一种。扩展一下到电影方面，应该和“独立电影”的概念比较相似，西方的游戏业也有独立游戏的说法，每年也有独立游戏节来评选各种优秀的作品。不过既然这里说的是同人，那么就局限在日本ACG产业内吧。

最初接触的同人物是什么已经不太记得了，不过第一个印象深刻的同人物倒是还记得，那是在某一期大众软件上介绍的《东方妖妖梦》。不过我当时也没有同人这个概念，仅仅是把其当作了一个制作精良音乐优美的打飞机小游戏游戏来玩的。第一次有同人这个概念应该是和听说Comic Market是同一个时期，不过也仅仅是稍作了解，当作新闻来看罢了，并没有有意识的去寻找同人物来看看。事情大概就是这么回事，这么些年接触的同人物也不少，不过说来都是已经非常出名的，或者在各论坛引起轰动的，话题性的作品，比如说东方，比如说寒蝉，再比如说那个快要坏掉的八音盒。也听说过不少同人组转行做商业产品的事情，另外不止是日本，最近连国内都到处听说有在办同人展。觉得这个行业也算是欣欣向荣，同人作品虽然或多或少的有那么些不尽如人意，甚至有些作品还很稚嫩，但是在这些作品中我能看到作者们的热情，显然他们是在用心来制作着这些作品。

之前我也说了，我不是一个热心于同人作品的人，自己自没有参与做过，接触的也是少数，不过那些作品的确给我留下了很好的印象。那么这个假期，在无意间看到了C79的合集后，仗着有比以前更为闲暇的时间，便抱着反正硬盘还有空间，不下白不下的想法下载了下来。至于之后的结果嘛，该说是比较失望吧，虽然只是从头到尾扫了一下，但是能够让人觉得眼前一亮的屈指可数。剩余的绝大部分作品只是让我觉得……其存在的必要性有待商榷。先不说工口物那高的吓人的比例是否正常，我无意做一个卫道士在这里唧唧歪歪，但是其中那些无论如何总之上来先干了再说，或者说只要啪啪啪了那么其他都无所谓的本子，其存在的意义难道仅仅是为了可以卖一笔钱？或者说画着自己喜欢的角色在一起啪啪啪很有趣？我无法理解这算是对自己喜欢作品的感情。我看不出这些东西里作者的“爱”在哪里，我不会用商业的标准来评价一个同人作品，工口也罢，简陋也罢，我想看到的是作者的想法。或者，另一方面，如果是有特点的作画也很不错。也许我这是站着说话不腰疼了，不过在光鲜的背后（谁也不会说去Comiket的人少吧）如果仅仅是充斥着这样的本子说实话我真不知道那么多人是去干什么的。或者说，仅仅是因为我不理解这些本子背后的价值？

那么到最后还是回到国内吧，这些年听说国内也办了不少同人展，奈何自己一直住在小地方，没有什么参与的机会，虽然合肥这两天听说有一个同人展，结果我已经回家了，既然没参与过也就不多说了，只是国内的环境相较于国外要恶劣不止一点（好吧，你懂的…），如果和国外一样的玩法那么后果基本上就是毁灭性的了。展会变的红火起来是好事，不过背后的老大哥也会关注起来，很多事情就没有道理可言了。

总之从个人角度而言我乐于看见更多优秀的同人作品，相较于商业作品，同人作品在某些方面要更加的自由，也可以不拘泥于现有的表现手法，加入更多实验性的东西，在商业作品越加流水线化的今天这是非常难能可贵的。虽然这次感觉有点坑爹，不过想来优秀的作品也并不少见，我又不是什么液内人士，瞎操心干么什么…最后推荐一个刚在Twitter上看到有人推荐的短篇，另外我还是决定等着看别人推荐了，自己扫真是太浪费时间了，我还是没那个爱啊。