数理逻辑2 B卷

Mathematical Logic 完全理解！

Coqide

A

P ∧ (Q ∧ R), (S ∧ E) ∧ U, E ⇒ W ⊢ (Q ∧ P) ∧ W

Require Import Classical.

Parameters P Q R S U E W: Prop.

Hypothesis P1: P /\ (Q /\ R).
Hypothesis P2: (S /\ E) /\ U.
Hypothesis P3: E -> W.
Goal (Q /\ P) /\ W.

Proof.

pose proof(proj1 P1).
pose proof(proj2 P1).
pose proof(proj1 H0).

pose proof(conj H1 H).

pose proof(proj1 P2).
pose proof(proj2 H3).

pose proof(P3 H4).

pose proof(conj H1 H).
pose proof(conj H6 H5).

exact H7.
Qed.

B

Q, Q ⇒ P ∨ R, R ⇒ S ⊢ P ∨ S

Require Import Classical.

Parameters P Q R S: Prop.

Hypothesis P1: Q.
Hypothesis P2: Q -> P \/ R.
Hypothesis P3: R -> S.
Goal P \/ S.

Proof.

pose proof(P2 P1).
destruct H.

left.
exact H.

right.
pose proof(P3 H).
exact H0.

Qed.

C

S ⇒ P, Q ⇒ E ⊢ (P ⇒ Q) ⇒ (S ⇒ E)

Require Import Classical.

Parameters P Q E S: Prop.

Hypothesis P1: S -> P.
Hypothesis P2: Q -> E.
Goal (P -> Q) -> (S -> E).

Proof.

intros H.
assert(S -> E).
intros H1.
apply P2.
apply H.
apply P1.
exact H1.
exact H0.

Qed.

D

(P ⇒ Q) ⇒ (P ⇒ R) ⇒ (Q ⇒ R ⇒ W) ⇒ P ⇒ W

Require Import Classical.

Theorem Implies : forall P Q R W : Prop, (P -> Q) -> (P -> R) -> (Q -> R -> W) -> P -> W.
Proof.
intros P Q R W PQ PR QR PW.

apply QR.
apply PQ.
exact PW.

apply PR.
exact PW.

Qed.

Symbolize

1. No superhero is faster than Spiderman.
2. Some evil superheros can climb on the wall.
3. Evil superheros are not faster than Spiderman.
4. If someone is faster than Spiderman, then Spiderman is evil.
5. Everone who is faster than Spiderman is evil and can climb on the wall.
6. There is someone who is faster than anyone who can climb on the wall.
7. Someone who is faster than Spiderman is evil.
8. Only those who are evil can be faster than those who are not faster than Spiderman.

Find Truth

UD: { Potter, Granger, Weasley }
Extension H: { Potter, Weasley }
Extension W: { Granger, Weasley }
Extension R: { (Potter, Granger), (Granger, Potter), (Weasley, Granger) }
Referent a: Potter

1. ∃x(Rxa ∧ Rax)
2. ∀x(Rxa ∨ Rax)
3. ∀x(Hx ⇔ Wx)
4. ∀x(Rxa ⇒ Wx)
5. ∀x[Wx ⇒ (Hx ∧ Wx)]
6. ∃x(Rxx)
7. ∃x∃y(Rxy)
8. ∀x∀y(Rxy)
9. ∀x∀y(Rxy ∨ Ryx)
10. ∀x∀y∀z[(Rxy ∧ Ryz) ⇒ Rxz]

IsConsistent

P ⇒ Q, Q ∧ (P ∨ P), ¬(Q ∨ R)

IsValid

1. R ⇒ (P ∨ Q), R ∧ Q ⊢ R ⇒ P
2. ¬R ⇒ Q, ¬P ∨ ¬Q, ¬(P ⇔ Q) ⊢ ¬(P ∨ Q)

Symbolize & IsValid

Every dwarf that saw Snowhite biting into the apple want to save her.
Someone (a dwarf) let the stepmother into the house.
Those dwarfs that want to save Snowite did not let the stepmother into the house.
Therefore: Not every dwaft saw Snowhite biting the apple.

Natural Deduction

1. P ∨ Q ⇒ R ⊢ (P ∧ Q) ⇒ R

Require Import Classical.

Parameters P Q R: Prop.

Hypothesis P1: P \/ Q -> R.
Goal (P /\ Q) -> R.

Proof.

intro.
destruct H.

apply P1.
left.
exact H.

Qed.

2. (R ∧ S) ⇒ (P ∧ ¬Q), E ∧ (E ⇒ S), Q ⊢ R ⇒ P

Require Import Classical.

Parameters P Q R S E: Prop.

Hypothesis P1: (R /\ S) -> (P /\ ~Q).
Hypothesis P2: E /\ (E -> S).
Hypothesis P3: Q.
Goal R -> P.

Proof.

intro.

pose proof(proj1 P2).
pose proof(proj2 P2).
pose proof(H1 H0).

pose proof(conj H H2).
pose proof(P1 H3).

pose proof(proj1 H4).
exact H5.

Qed.

3. j is a constant, ∀x(¬Mx ∨ Ljx), ∀x(Bx ⇒ Ljx), ∀x(Mx ∨ Bx) ⊢ ∀xLjx
4. ∃x∀yPxy ⊢ ∀y∃xPxy
5. ∀xPx, ∃x(Px ⇒ ∀yQy), ∀x(Qx ⇒ Rx) ⊢ ∃x(Qx ∧ Rx)

Argument invalid, Prove

∃x(Dx), ∃x(Ex), ∀x(Dx ∨ Ex) ⊢ ∃x(Dx ∧ Ex)