@user525966 No, just look at the actual ∀-elim rule instead of using what you think the rule is. The rule requires that you have deduced "E∈S" and "∀x∈S ( P(x) )" earlier before you can deduce "P(E)". So at no point does the rule let you construct or label a new object!
@user525966 This is indeed permitted by the rules and is fine. After all, in the same context you already can write:
Problem is I still have absolutely no idea what that means -- I don't know what all "E" can look like, or what all "P(E)" can look like, or how this differs necessarily from "P(x)" and so on
@user525966 As I said before, if you use different systems when you haven't even mastered a single one, you run the serious risk of getting yourself confused. It seems to have been the case here.
@user525966 Note that you're wrong about the other system as well.
At the risk of confusing you, let me just correct the claim about the other system. You can substitute any well-formed term, not just a variable, and definitely not just a constant-symbol.
In my system, you are not permitted to substitute "E" unless you have previously proven "E∈S". If you haven't then you can't. This is one reason you cannot anyhow substitute variables, because it must already occur in a previous line!
In my system, you are not permitted to substitute "E" unless you have previously proven "E∈S". If you haven't then you can't. This is one reason you cannot anyhow substitute variables, because it must already occur in a previous line!
might be a difference of system but every other system I have come across permits this
I don't like blindly using things I don't understand / I have no idea what E in S means or why it's needed, or how this is meant to convolve with the other conditions -- if you say it's a term and not just a variable or constant symbol, and so on, that honestly confuses me more
like nothing about it makes sense to me and I don't see what it's trying to do or what it's permitting
unfortunately I do have to get to sleep, good night!
@user525966 It's intuitive, but I noticed that you always make such errors because you keep misinterpreting things in my system due to other systems. If you were to stick to my system alone, you wouldn't have this problem now. In particular, "∀x∈S ( P(x) )" literally states "for every x in S, x satisfies P". So of course if you have this forall-statement you can only claim "P(E)" if E in S.
From "Every human is a living creature." you obviously cannot deduce "My pencil is a living creature.".
@LeakyNun For every finite subset of ZFC, you can write down its conjunction explicitly, and ZFC can prove that that conjunction has a model. ZFC cannot prove ( for every finite subset S of ZFC, S has a model ).
