构造下面推理的证明 前提:p→¬q, r→q, r 结论:¬p
时间: 2024-03-19 07:42:14 浏览: 142
证明如下:
1. 假设p为真,则根据前提1有¬q为真;
2. 根据前提2和3可知q和r都为真;
3. 由2可知,r为真,则根据前提1可知¬q为真,这与2中q为真矛盾;
4. 因此,假设p为真是不成立的,即p为假;
5. 根据1可知¬q为真,再结合4可知p→¬q为真;
6. 综上可得,当p为假时,p→¬q、r→q和r三个前提可以同时成立,故结论是正确的,即¬p为真。
因此,证明完成。
相关问题
构造推理证明:¬("x)R(x) ├─($x)Q(x)
证明:
1. 假设 ¬("x)R(x) 为真。
2. 对于任意元素x,构造条件语句“如果R(x)为真,则Q(x)为真”。
3. 假设存在一个元素a使得Q(a)为假。
4. 由于 ¬("x)R(x) 为真,因此存在一个元素b使得R(b)为假。
5. 对于元素b,由于R(b)为假,因此条件语句“如果R(b)为真,则Q(b)为真”总是成立。
6. 由于条件语句总是成立,因此无论Q(b)为真或假,条件语句都成立。
7. 与假设存在一个元素a使得Q(a)为假矛盾,因此假设不成立。
8. 由于假设不成立,因此 ¬("x)R(x) ├─($x)Q(x)。
证毕。
使用lean 3完成example : (P ∨ Q) → ¬Q → P :=
Lean 3 是一种基于 Lean Proof Assistant 的数学证明环境,它支持严格的数学推理和正式化。要在 Lean 中完成给定的逻辑推理 `(P ∨ Q) → ¬Q → P`,我们首先需要定义命题 `P` 和 `Q`,然后构造前提和结论,并最终证明它们之间的蕴含关系。
这是一个基本步骤的例子:
```lean
import tactic
/-- 定义两个命题 P 和 Q -/
def P : Prop := true
def Q : Prop := false -- 或者你可以定义其他形式
/-- 命题 (P ∨ Q) -/
lemma P_or_Q : P ∨ Q :=
begin
split,
{ exact P }, -- 证明 P 或 Q 的第一部分,这里是直接真
{ intro h, contradiction, -- 如果假设 Q,那么¬Q 就是真的,这与前提 ¬Q 矛盾
exact absurd h not_not Q -- 通过 ¬Q 的否定得到 Q 的矛盾
}
end
/-- 假设 ¬Q 推导出 P -/
lemma from_neg_Q_to_P (h : ¬Q) : P :=
begin
cases P_or_Q with hp or_q, -- 分支处理 P 或 Q
{ exact hp }, -- 如果 P 已经确定,我们就得到了结果
{ exact hp, -- 因为 Q 被否定,所以推断出 P
assumption } -- 利用前提 ¬Q
end
/-- 总结整个论证 -/
theorem main_theorem : (P ∨ Q) → ¬Q → P := from_neg_Q_to_P
```
在这个例子中,我们首先证明了 `P ∨ Q`,然后假设 `¬Q` 并由此推出 `P`。最后,我们把这两个步骤组合成一个完整的定理。
阅读全文