作者cmlrdg (心之语)
看板logic
标题Re: [请益] axiom system
时间Sun Feb 8 19:39:18 2009
※ 引述《MathTurtle (恩典)》之铭言:
: 我来补充一下好了。
: ※ 引述《cmlrdg (心之语)》之铭言:
: Mendelson这本是本经典的好书,
: 不过真的要读完它也不是很容易,
: 加油 ^^
感谢MathTurtle大的补充 ^_^
小弟才疏学浅, 是逻辑学入门新手
谢谢您点出我想法上的一些漏洞 :)
: : ^^^^^^^^^^^^^^^ ^^^^^^^^^^^^
: : 是的...
: : 简单来说, 他的公理有A1, A2, 和A3三种型式
: : 每一个型式都有(可数)无限多个逻辑句子.
: : 你可以发现若将上述的A, B, C看成Boolean variables,
: : 则A1, A2, A3都是tautologies, 因此被列为axioms.
: : 其他tautologies都可以藉由这些axioms透过inference rules(如modus ponens)
: : 来"证明."
: 用 tautology来说明axiom是什麽, 可以帮助理解,
: 不过还是必须小心:
: (1) tautology 本身并不是一个很清楚的概念 (except in something like TLP)
: 而且多半预设了 true in all models 之类的 semantic notions.
我对於逻辑的认知
绝大多数来自於C. H. Papadimitriou的书
因此也采用了不少他的说法 :)
在这里 我所谓的tautology
意思是指在truth table当中
truth value恒为true的句子
而句子当中的变数(至少就"形式"上而言)都是boolean
因此 在探讨first-order logic的logical axioms(有别於
nonlogical axioms, 稍後说明:))时
他这本书里提到有以下三种型式 (不多赘述)
1) "形式"上是boolean的tautology
(例如 (for all x, x < y) => (for all x, x < y) "形式"上为p => p
为tautology. p这个"形式"上的boolean变数用来代表(for all x, x < y)
这个first-order句子)
2) 等号的关系
(例如 x = y => f(x) = f(y), 其中f是unary function symbol)
3) quantifiers
(例如 (for all x ψ) => ψ)
而true in all models的句子
在Papadimitriou的书里
叫做valid expression
(我发现Papadimitriou的名词跟其他作者所采用的似乎有些不同 XD
例如在first-order里他不用interpretation这个名词, 而一律用model
有别於其他书采用这两个名词并且意思不同)
: (2) axioms 如你所言, 是透过infernece rules可以推导出这理论中的所有定理
: 的一些命题。这里纯粹是syntactic notions.
: (3) 为何设定 A1 A2 A3这三个命题为axiom, 严格说并不是因为它们是tautology,
: 而是因为这三条配合此系统的推论规则可以推导出所有的定理。
真的是非常感谢MathTurtle大 <(_ _)>
我忽略掉很重要的一点:
之所以把他列为axiom, 不光是他是tautology(或valid expression)
而是这几个句子形成一个complete axioms set
也就是所有这个系统的tautologies都可以利用这个set里的句子搭配
inference rules而证明出来
(我印象中在H. Enderton的书里有看到
propostional logic是完全的axiomatizable
也就是存在有complete axioms set...不过我不太确定^^"
或许可以请MathTurtle大解说一下:P)
不过predicate logic就没那麽幸运了 XD
(K. Godel说predicate logic有些句子是valid却不能证)
: : 值得一提的是:
: : 这个系统探讨的逻辑句子应该只有Boolean logic而已,
: : 跟real number system的axioms不太相同,
: : (real number system的某些axioms写成Boolean型态并非tautologies,
: : 因此这些axioms更像是人规定的...XD)
: : 逻辑句子也不同,
: : 不过意义是一样的.
: : (都是作为证明之前的基本事实...也就是规定是对的, 不需要证明)
: 应该这麽说, 一般设定实数系统包含了PA (Peano Arithmetics),
: 而PA又包含了述词逻辑系统(predicate logic), 再包含了命题逻辑系统,
: 因此命题逻辑系统通常是被其它系统「预设」。
: 不过选哪些命题作为公理, 通常是看你的系统有哪些primitives,
: 然後选一些足够推导出所有定理的最小集合为公理。
: 这其实没有什麽原因, 像是自然演译法中, 你可以完全没有公理。
: 而这里的这三条, 主要是因为这个系统把 material implication 与 negation
: 当成惟一的两个primitives.
: 实数系统当然需要多一些公理, 毕竟它有更多的primitives,
: 像是大小就是最重要的一个要去characterise的东西。
: 我们不太能说实数系统的公理不是tautologies,
: 如果你tautology 指的是necessary truth的话,
: 实数系统里的命题也都是necessary truth.
: 当然如果你的tautology指的是true in all models,
: 你当然可以construct 非实数系统的model使其公理为假,
: 但这似乎不是证明这些不是tautology。
如同前面所描述的
true in all models的句子
若探讨的是propostional logic时, 的的确确就是tautology;
若探讨的是predicate logic时, 称作valid expression.
而这些句子当中有些被列为(logical) axioms
也就是前述的那三种来源
在Papadimitriou的书里, 把前述的三种axioms 称为logical axioms
的原因在於 他们是"true in all models" 在任何model、任何theories
(例如number theory, graph theory, group theory, etc.)
都成立
有别於logical axioms, Papadimitriou在他书中提到每个特定的theory (如
number theory) 都有专属於自己的axioms, 这些称为nonlogical axioms
(nonlogical翻译成中文的意思是"非"逻辑的; illogical翻译成中文是
"不合"逻辑的...有差 XD)
这些就不是"true in all models"了
以Papadimitriou的说法来看
MathTurtle大所提到的PA
当中的数学归纳法公理应该就是nonlogical axiom了
(PA其他的axioms我就不清楚了, 跟PA不熟...XD)
原po说的关於实数系的axioms set
是logical axioms set和nonlogical axioms set的union
最後, 藉由这个话题
我来讲一下我读Papadimitriou的心得XD
在predicate logic里(严格来说是first-order logic)
Godel's incompleteness theorem说明的是
在number theory当中
没有一个enumerable axioms set足以完全"捕捉"到整数的性质
或者说没有一个enumerable axioms set可以过滤掉其他的models
只剩下我们想要的那一个
(给了一个(enumerable) axioms set, 可以满足的models似乎可以有很多个
彼此之间的差异是没有办法用这些axioms来加以区别的)
不知道各位的看法如何?
有错欢迎指正! 谢谢^^
再一次感谢MathTurtle大的补充
让我了解了更多:)
: : 这个版上之前有人讨论过, 你可以按z进入查一下
: : 大致上来说, well-formed formulas是用recursive方式定义:
: : 1) Boolean variable (如p)是wff
: : 2) 若p和q都是wffs, 则 p and q, p or q, not p都是wffs
: : 上述所说是Boolean logic的wffs.
: : 因此像 (p and q) => p 是一个wff.
: : 希望有解决你的问题^^
: : 各位板大有错请指正<(_ _)>
: 如果要了解什麽是 wff,
: 或许也要举个不是wff 的例子, 下面三个都不是:
: 1. p xxx q not
: 2. p q ( not
: 3. (p and q) and r)
--
我是新手@@, 感谢各位的指教 <(_ _)>
--
※ 发信站: 批踢踢实业坊(ptt.cc)
◆ From: 211.74.96.226
1F:推 aletheia:logical/non-logical axiom的区分 似乎不是那麽漂亮 02/09 01:26
2F:推 aletheia:就logicism的立场来说 会反对这样的区分吧 02/09 01:27
3F:→ cmlrdg:呵 Papadimitriou这本书的定义方式有别於其他作者,或许是因 02/09 10:38
4F:→ cmlrdg:为要简化说明.毕竟这本书叫做computational complexity... 02/09 10:39
5F:→ cmlrdg:逻辑扮演辅助工具的脚色,因此没有着墨太多吧...:) 02/09 10:41
6F:推 Hseuler:那本是在说可计算理论还是计算理论呢? 02/10 21:06
7F:→ cmlrdg:回楼上,那本是在讨论计算复杂度,有逻辑和计算理论的部分,不 02/10 22:11
8F:→ cmlrdg:过不多就是了:) 02/10 22:11
9F:→ cmlrdg:顺带一提,Mendelson的这本书还满棒的,如M大所言^^ 另外,我 02/11 01:13
10F:→ cmlrdg:最近在读Ebbinghaus的Mathematical logic,这本也很棒!虽然 02/11 01:15
11F:→ cmlrdg:只有将近300页,但是内容详尽丰富.这本好像也是交大资科正规 02/11 01:18
12F:→ cmlrdg:语言这门课用的课本:) 02/11 01:18
13F:推 Hseuler:谢谢! 02/19 22:32