正在加载图片...
(a)(vx)(y(x)Vv(x)+(Vr)yp(x)V(vx)v(x) (b)(三x)(y→v(x)→(→(x)v(x), not free in y. (c)(彐x)(y?(x)→v(x)→(y(x)→(m)(x) (d)(x)y(x)→v)→(vax)((x)→v), r is not free in y 2. Let y and a be any formula with free variables y and z: let w be any variable not appearing p and v. Give tableau proofs of the following (a) 3. Vy (Vap V)+3rvyVw(p(a/w)vv) (b)ry(y→Vzv(2)→V3yvu(y→(z/) 3. Let p(a1,., n) be a formula in a languange L with all free variables displayed and let n be constant symbols not in L. Show that Var1... V np(a1, .. In) is tableau prov- able if and only if P(c1(a) (∀x)(φ(x) ∨ ψ(x)) ↔ (∀x)φ(x) ∨ (∀x)ψ(x) (b) (∃x)(φ → ψ(x)) → (φ → (∃x)ψ(x)), x not free in φ. (c) (∃x)(φ(x) → ψ(x)) → (φ(x) → (∃x)ψ(x)). (d) ((∃x)φ(x) → ψ) → (∀x)(φ(x) → ψ), x is not free in ψ. 2. Let φ and ψ be any formula with free variables x, y and z; let w be any variable not appearing in φ and ψ. Give tableau proofs of the following. (a) ∃x∀y(∀zφ ∨ ψ) ↔ ∃x∀y∀w(φ(z/w) ∨ ψ). (b) ∀x∃y(φ → ∀zψ(z)) → ∀x∃y∀w(φ → ψ(z/w)). 3. Let φ(x1, . . . , xn) be a formula in a languange L with all free variables displayed and let c1, . . . , cn be constant symbols not in L. Show that ∀x1 . . . ∀xnφ(x1, . . . , xn) is tableau prov￾able if and only if φ(c1, . . . , c2) is. 6
<<向上翻页
©2008-现在 cucdc.com 高等教育资讯网 版权所有