Q: 命题演算形式系统 L L L中的形式语言 L 0 \mathscr L_0 L0由哪两部分构成? A: 一个(可能无穷)的符号集 ∼ , → , ( , ) , p 1 , p 2 , ⋯ \sim,\to,(,),p_1,p_2,\cdots ∼,→,(,),p1,p2,⋯,以及一个合式公式(well-formed formulas)集。 注:回忆 { ∼ , → } \{\sim,\to\} {∼,→}是完备集。 合式公式集是递归定义的。即 p i p_i pi是公式;且对于公式 A , B \mathscr A,\mathscr B A,B,有 ( ∼ A ) (\sim \mathscr A) (∼A)和 ( A → B ) (\mathscr A\to\mathscr B) (A→B)是公式。 注:当然也可以采用前缀表达式,从而不需要引入括号。
Q: 上面的符号集中的符号 ∼ \sim ∼和函数 f : { 0 , 1 } → { 0 , 1 } ; f ( 0 ) = 1 , f ( 1 ) = 0 f:\{0,1\}\to\{0,1\};f(0)=1,f(1)=0 f:{0,1}→{0,1};f(0)=1,f(1)=0有什么联系? A: 形式系统 L L L中的字符 → \to →和 ∼ \sim ∼是抽象的记号,我们并不天然地认为它们代表了用真值表或布尔函数定义的“具体”的连接符 → , ∼ \to,\sim →,∼. 但是 L L L的公理模式和推理规则实际上从某种程度上符合了 → , ∼ \to,\sim →,∼的意义。
Q: 说“ L L L的公理只有三条”有何不准确之处? A: L L L有三个公理模式。每个公理模式中的 A , B \mathscr A,\mathscr B A,B等都可以代表任意公式(命题形式),从而有无数条公理。 当然,也可以引入替换规则,这样可以只使用三条公理而不用前面说的“公理模式”了。
Q: L L L中的公理模式和演绎规则有什么密切的联系? A: 可以发现所有的公理模式都是 A → B \mathscr A\to\mathscr B A→B形式。因此如果另已知 A \mathscr A A,就可以通过分离规则得到直接后承 B \mathscr B B. 这体现了两者的密切关系。
Q: 依据形式证明的定义,能否在 L L L中证明 L L L的公理? A: 按照定义, L L L中的公理自然也是 L L L中的定理。证明是只含有自身的序列。 注:公理是没有经过证明,但被当作不证自明的命题。这和“在 L L L中证明公理”是两个方面的东西。
Q: 从什么集合的演绎就是证明? A: 空集(或:包含若干条公理的集合) 注:从集合 Γ \Gamma Γ的演绎和从 Γ ∪ Γ ′ \Gamma\cup \Gamma' Γ∪Γ′的演绎(其中 Γ ′ \Gamma' Γ′中所有公式都是公理)依据定义是相同的。 注:因此 A \mathscr A A是 L L L中定理可以简记为 ∅ ⊢ L A , ⊢ L A , ⊢ A \emptyset\vdash_L\mathscr A,\vdash_L\mathscr A,\vdash\mathscr A ∅⊢LA,⊢LA,⊢A.
Q: 使用前缀表达式(前置式),在 L L L中构造 A , → B → A C ⊢ → B C \mathscr A, \to \mathscr B\to\mathscr A\mathscr C\vdash\to \mathscr B\mathscr C A,→B→AC⊢→BC的演绎。 A: (1) A \mathscr A A(假设) (2) → B → A C \to \mathscr B\to\mathscr A\mathscr C →B→AC(假设) (3) → A → B A \to \mathscr A \to \mathscr B \mathscr A →A→BA(L1) (4) → B A \to \mathscr B \mathscr A →BA((1)(3)MP) (5) → → B → A C → → B A → B C \to\to \mathscr B\to \mathscr A \mathscr C \to\to \mathscr B \mathscr A\to \mathscr B \mathscr C →→B→AC→→BA→BC(L2) (6) → → B A → B C \to\to \mathscr B \mathscr A\to \mathscr B \mathscr C →→BA→BC((2)(5)MP) (7) → B C \to \mathscr B\mathscr C →BC((4)(6)MP)
Q: 在证明元定理 ⊢ → A A \vdash\to \mathscr A\mathscr A ⊢→AA和 ⊢ → ∼ B → B A \vdash\to\sim\mathscr B\to\mathscr B\mathscr A ⊢→∼B→BA时,所使用的隐含分配(L2)分别具体是什么? A: 可能的答案: → → A → → A A A → → A → A A → A A \to \to\mathscr A \to\to \mathscr A\mathscr A\mathscr A \to\to\mathscr A\to \mathscr A\mathscr A\to\mathscr A\mathscr A →→A→→AAA→→A→AA→