for questions or link request: module admin

A simple implication:

**1. Proposition**

∀x R(x) → ∃x R(x) (predtheo1)

1 | ∀x R(x) → R(y) | add axiom axiom5 |

2 | R(y) → ∃x R(x) | add axiom axiom6 |

3 | ∀x R(x) → ∃x R(x) | hypothetical syllogism with 1 and 2 |

qed |

A well known implication:

**2. Proposition**

∃x R(x) → ¬∀x ¬R(x) (predtheo2)

1 | ∀x R(x) → R(y) | add axiom axiom5 |

2 | ∀x ¬R(x) → ¬R(y) | replace predicate variable R(@S1) by ¬R(@S1) in 1 |

3 | ¬∀x ¬R(x) ∨ ¬R(y) | use abbreviation impl in 2 at occurence 1 |

4 | (P ∨ Q) → (Q ∨ P) | add axiom axiom3 |

5 | (¬∀x ¬R(x) ∨ Q) → (Q ∨ ¬∀x ¬R(x)) | replace proposition variable P by ¬∀x ¬R(x) in 4 |

6 | (¬∀x ¬R(x) ∨ ¬R(y)) → (¬R(y) ∨ ¬∀x ¬R(x)) | replace proposition variable Q by ¬R(y) in 5 |

7 | ¬R(y) ∨ ¬∀x ¬R(x) | modus ponens with 3, 6 |

8 | R(y) → ¬∀x ¬R(x) | reverse abbreviation impl in 7 at occurence 1 |

9 | ∃y R(y) → ¬∀x ¬R(x) | particularization by y in 8 |

10 | ∃x R(x) → ¬∀x ¬R(x) | rename bound variable y into x in 9 at occurence 1 |

qed |

The reverse is also true:

**3. Proposition**

¬∀x ¬R(x) → ∃x R(x) (predtheo3)

1 | R(y) → ∃x R(x) | add axiom axiom6 |

2 | ¬∃x R(x) → ¬R(y) | apply proposition hilb7 in 1 |

3 | ¬∃x R(x) → ∀y ¬R(y) | generalization by y in 2 |

4 | ¬∀y ¬R(y) → ¬¬∃x R(x) | apply proposition hilb7 in 3 |

5 | ¬∀y ¬R(y) → ∃x R(x) | elementary equivalence in 4 at 1 of hilb6 with hilb5 |

6 | ¬∀x ¬R(x) → ∃x R(x) | rename bound variable y into x in 5 at occurence 1 |

qed |

Exchange of universal quantors:

**4. Proposition**

∀x ∀y R(x, y) → ∀y ∀x R(x, y) (predtheo4)

1 | ∀x R(x) → R(y) | add axiom axiom5 |

2 | ∀y R(y) → R(u) | substitute variables in 1 |

3 | ∀y R(z, y) → R(z, u) | replace predicate variable R(@S1) by R(z, @S1) in 2 |

4 | ∀v R(v) → R(z) | substitute variables in 1 |

5 | ∀v ∀w R(v, w) → ∀w R(z, w) | replace predicate variable R(@S1) by ∀w R(@S1, w) in 4 |

6 | ∀x ∀y R(x, y) → ∀y R(z, y) | substitute variables in 5 |

7 | ∀x ∀y R(x, y) → R(z, u) | hypothetical syllogism with 6 and 3 |

8 | ∀x ∀y R(x, y) → ∀z R(z, u) | generalization by z in 7 |

9 | ∀x ∀y R(x, y) → ∀u ∀z R(z, u) | generalization by u in 8 |

10 | ∀x ∀y R(x, y) → ∀y ∀z R(z, y) | rename bound variable u into y in 9 at occurence 1 |

11 | ∀x ∀y R(x, y) → ∀y ∀x R(x, y) | rename bound variable z into x in 10 at occurence 1 |

qed |

Implication of changing sequence of existence and universal quantor:

**5. Proposition**

∃x ∀y R(x, y) → ∀y ∃x R(x, y) (predtheo5)

1 | ∀x R(x) → R(y) | add axiom axiom5 |

2 | ∀y R(y) → R(u) | substitute variables in 1 |

3 | ∀y R(x, y) → R(x, u) | replace predicate variable R(@S1) by R(x, @S1) in 2 |

4 | R(y) → ∃x R(x) | add axiom axiom6 |

5 | R(x) → ∃z R(z) | substitute variables in 4 |

6 | R(x, u) → ∃z R(z, u) | replace predicate variable R(@S1) by R(@S1, u) in 5 |

7 | ∀y R(x, y) → ∃z R(z, u) | hypothetical syllogism with 3 and 6 |

8 | ∃x ∀y R(x, y) → ∃z R(z, u) | particularization by x in 7 |

9 | ∃x ∀y R(x, y) → ∀u ∃z R(z, u) | generalization by u in 8 |

10 | ∃x ∀y R(x, y) → ∀y ∃x R(x, y) | substitute variables in 9 |

qed |