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.
A question regarding the Sequent Calculus
The ‘for all introduction’ inference rule in SQ requires the antecedents A and X not in free(Gamma) to conclude for all A.
Why must X not be a free variable in Gamma?
Because if it were, the inference rule wouldn’t be sound.
The idea being, that we want to prove \forall X.\phi by showing that \phi holds for an arbitrary element X that we do not make any additional assumptions about. If we were to have additional assumptions (i.e. if X already occurs freely in the context), then we couldn’t conclude that it holds for all elements.
Example: Assume we work in the natural numbers and \Gamma contains the assumption “X is divisible by 4”. Now it’s easy to derive the formula \phi=“X is divisible by 2”. Without the requirement that X is not free in \Gamma, we could now use forall-Introduction to derive the formula “\forall X. X is divisible by 2”, which is clearly wrong.