Resolva os seguintes exercícios mediante o método de dedução natural proposto por Gentzen para lógica de predicados aplicando as regras básicas de inferência expostas na teoria da demonstração:
NÍVEL 1
| [Exercício 13] | [Exercício 14] | ||
-1.∀x(Px→ Qx) |
⊦∃xQx | -1.∀xPx^∀xQx | ⊦∀x(Px^Qx) |
| -2. Pa | |||
| 3. Pa → Qa | E∀1 (x:a) | ||
| 4. Qa | E→ 2,3 | ||
| 5. ∃xQx | I∃4 | ||
NÍVEL 2
| [Exercício 15] | [Exercício 16] | ||||
| -1.∀xPx ∨ ∀xQx | ⊦∀x(Px^Qx) | -1.∀x∀y∀z((Rxy^Ryz)→Rxz) | ⊦∀x∀y(Rxy→¬Ryx) | ||
| -2.∀x¬Rxx | |||||
| ┌ | 3. Rab | ||||
| | | ┌ | 4. Rba | |||
| | | | | 5. Rab ∧ Rba | I^3,2 | ||
| | | | | 6. Rab ^Rba --> Raa | E∀1 (x:a, y: b, z:a) | ||
| | | | | 7. Raa | E→5,6 | ||
| | | | | 8. ¬Raa | E∀2 (x:a)E | ||
| | | ┗ | 9. Raa∧¬Raa | i^7,8 | ||
| ┗ | 10. ¬Rba | i^4-9 | |||
| 11. Rab --> ¬Rba | i→3-10 | ||||
| 12. ∀x∀y(Rxy→¬Ryx) | i∀11 | ||||
NÍVEL 3
| [Exercício 17] | ||
| -1.∀x(Px→ Qx) | ⊦∀x(∀y(Px^Ryx)→∀y(Qx ^Ryx)) | |
| ┌ | 1. ∀y(Pa^Rya) | |
| | | 2. Pa ∧ Rba | E∀1 (y:b) |
| | | 3. Pa | E^2 |
| | | 4. Pa→ Qa | E∀1 (x:a) |
| | | 5. Qa | E→3,4 |
| | | 6. Rba | E^2 |
| | | 7.Qa ∧ Rba | I^5,6 |
| ┗ | 8. ∀y(Qa^Rya) | I∀7 (b:y) |
| 9. ∀y(Pa^Rya) →∀y(Qa^Rya | I→1-8 | |
| 10. ∀x(∀y(Px^Ryx)→∀y(Qx ^Ryx)) | I∀9 (a:x) | |
| [Exercício 18] | |
-1.∀x(Px→( ∀y(Qy^Ryz)↔¬Sx)) |
⊦∀x((Px^∀y¬(Qy^Ryx))→ ¬Sx) |