First-Order Tableaux

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.

First-Order Tableaux
Hello,

in First-Order Tableaux sometimes we substitute with big and sometimes with small letter.
For example: ∀X.P(X) with P(Y) and ∀X.Q(X) with Q(c).

What is the difference there? Is it important if it is small or big letter? How could we know which one should we do?

Thanks in advance!


I am using the convention (I hope somewhat consistently) that lower-case letters are reserved for constants and capital letters are used for variables. This is inspired by ProLog.