→ 7 messages moved to Basic Mathematics

@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:

∀x∈S ( x=x ).
∀x∈S ( x∈S ).

What's the difference from permitting:

Given x∈S:
  ...
Given x∈S:
  ...

It's perfectly fine to permit it.

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

In that other system (and most that I see online) it permits things like this: chat.stackexchange.com/transcript/message/49124613#49124613

Where once you have a for-all statement you can remove it and replace the variable with some constant to indicate that you're taking an instance

@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!

I literally use forall elim on the next line after the header

@user525966 Paste your proof. I have no idea what you're referring to.

Wrong.

I repeat myself:

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.".

Anyway, good night!

@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 ).

(Unless ZFC is inconsistent.)