Question about exam WS1819 task 5.2 (Natural Deduction with Quantifiers)

Master / Vertiefung Künstliche Intelligenz
1

Disclaimer: Dieser Thread wurde aus dem alten Forum importiert. Daher werden eventuell nicht alle Formatierungen richtig angezeigt. Der ursprüngliche Thread beginnt im zweiten Post dieses Threads.

2

Question about exam WS1819 task 5.2 (Natural Deduction with Quantifiers)
Hello,

https://kwarc.info/teaching/AI/exams/exam-WS2018-19-with-solutions.pdf

((∀X.∀Y.R(Y, X)⇒P(Y))∧(∃Y.R(c, Y)))⇒P(c)

1(Assumption)1(∀X.∀Y.R(Y, X)⇒P(Y))∧(∃Y.R(c, Y))
2∧-Elimination on1∀X.∀Y.R(Y, X)⇒P(Y)
3∧-Elimination on1∃Y.R(c, Y)
4∀-Elimination on2∀Y.R(Y, X)⇒P(Y)
5∀-Elimination on4R(c, X)⇒P(c)
6∀-Introduction on5∀X.R(c, X)⇒P(c)
7(Assumption)2R(c, d)
8∀-Elimination on6R(c, d)⇒P(c)
9⇒-Elimination on8,7P(c)
10∃-Elimination2on3,9P(c)
11⇒-Introduction1on10((∀X.∀Y.R(Y, X)⇒P(Y))∧(∃Y.R(c, Y)))⇒P(c)

Could we replace the X immediately with d when dropping the forAll in line 4?
Or do we really have to recreate the forAll and drop it again? Why?

1 „Gefällt mir“
3

I am not too familiar with the precise notation in AI 1, but [m]7(Assumption)2 R(c, d)[/m] sounds a bit fishy to me. Where does this assumption come from? Shouldn’t the whole point of the exercise be to extract an [m]R(c, d)[/m] from the second conjunct ([m]∃Y.R(c, Y)[/m])?

1 (Assumption) 1 (∀X.∀Y.R(Y, X)⇒P(Y))∧(∃Y.R(c, Y))
2 ∧-Elimination on 1 ∀X.∀Y.R(Y, X)⇒P(Y)
3 ∧-Elimination on 1 ∃Y.R(c, Y)
4 ∀-Elimination on 2 ∀Y.R(Y, X)⇒P(Y)
5 ∀-Elimination on 4 R(c, X)⇒P(c)
6 use \exists elimination to get R(c, d) from second conjunct
7 ⇒-Elimination on 5 and 6 to get P(c)
8 ⇒-Introduction 1 on 7((∀X.∀Y.R(Y, X)⇒P(Y))∧(∃Y.R(c, Y)))⇒P(c)

Mind you, I deliberately used natural language in line 6 as I don’t know how you are writing it in AI. Perhaps your existential elimination rule is also different from the usual one? The usual one is [m](∃Y. phi) (phi[Y/Z] … psi) // psi[/m], where [m]Z[/m] is a fresh variable, [m]phi[Y/Z] … psi[/m] a subproof proving [m]psi[/m] from the assumption [m]phi[Y/Z][/m]. Since your notation is linear, there must be some difference in how you denote subproofs.

4

There is no reason. This is a proof, but not not the best one. I will change the master solution.

5

Ok, thanks, I was just wondering whether it’s correct.