帮我解离散数学的一条逻辑谓词证明题

论域为人的全体,定义谓词如下:P(x):x怕困难;Q(x):x能成功;R(x):x失败
前提符号化为:如果一个人怕困难就不能成功:(Ax)(P(x)→非Q(x))
每一个人或者成功或者失败:(Ax)(Q(x)∨R(x))
有个别人没有失败:(Ex)(非R(x))
结论符号化为:有存在不怕困难的人:(Ex)(非P(x))
(1)(Ex)(非R(x)) P
(2)非R(a) T ES(1)
(3)(Ax)(Q(x)∨R(x)) P
(4)Q(a)∨R(a) T US(1)
(5)Q(a) T(2)(4)
(6)(Ax)(P(x)→非Q(x)) P
(7)P(a)→非Q(a) T US(6)
(8)非P(a) T(5)(7)
(9)(Ex)(非P(x)) T EG(8)
(Ax)全称量词,(Ex)存在量词,P规则,T规则,ES存在指定,US全称指定,EG存在推广
回答你的补充,成功或者失败从语义上讲是对立的,即非成功必失败,但现在是形式证明,不考虑语义,不能从语义上理解,仅从逻辑构成或形式上理解,否则前提"每一个人或者成功或者失败"是多余的,因为"非P或P"是永真的,不需作为前提.
形式证明中常用的两个规则,P规则,T规则,证明过程是由一系列公式构成,每个公式独占一行,并且每行的前面按顺序加上行号,最后一行是代表结论的公式,其它行的公式或是由前提中的公式中直接拿来(P规则),或是由前面一行或几行公式蕴含得到的(T规则).将所用规则标记在行末,如果是T规则还要标记出由哪些行蕴含得到的,并记下行号.
P规则 在演绎过程中,可随时直接引入前提中的公式
T规则 在演绎过程中,随时可以引入由前面一行或几行公式蕴含得到的公式