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.
Question regarding propositions with free variables
I don’t quite see the difference between propositions with free variables and these propositions with all free variables being bound via universal quantors, e.g.
forall x.p(x) and p(x) with p being a predicate, since with the natural deduction calculus we can get
forall x.p(x) → p(y) and p(y) → forall x.p(x) by forall elimination/introduction resp.
Not considering variable names, p(y) and forall x.p(x) seem to be equivalent but since they differ in bound variables they should be something completely different (at least I got this idea from the lecture).
What’s going on here?
2 „Gefällt mir“
That is a very good question. Let me try to explain (if my explanation here does not help, please ask again in the lecture on thursday).
I indeed said that bound and free variables are completely different animals, and I stand by this even though semantically, we can express almost the same things with it for validity.
Indeed, if you have the formula all x. p(x) is valid, iff p(x) is valid. (BTW, so is p(c), since in all cases, I can interpret x (and c) with anything I like: for x via the variable assignment and for c via the interpretation.
BUT, sytactically I can rename all x. p(x) to all z. p(z) whereas I cannot rename p(x) or p(c) → first difference
Also if I am interested in satisfiability all x. p(x) may be unsatisfiable (e.g. because p(a) is false) while p(x) is satisfiable (e.g. because p(b) is true). There p(x) and p(c) for that matter behave like ex x. p(x).
I look at this problem in this way. The universal and existential quantifiers make explicit in the language what we might mean with a free variable. And since we can make the behavior variables explicit by binding them, we can restrict ourselves to talking about propositions without free variables (sentences).
I am not sure this explanation helps, … but I hope it does.
This helped a lot, thanks! I’m a bit bewildered by the fact that validity and satisfiability of propostions with free variables in first order logic (like p(x)) can be rewritten as validity of sentences (all x.p(x) and exists x.p(x) respectively) in first order logic. It feels as though we should switch realms when considering such questions and a little bit as if propositional logic was still buried in first order logic in the form of propositions with free variables …
… but maybe this is why propositions are called propositions (like in ‘propositional logic’) after all…
Anyway, this is getting quite philosophical …