Question on Theorem rspc about distinct variables

[bil...@gmail.com]

Theorem rspc has the allowed substitution hint ps(x).

Is this correct? Doesn't the hypothesis rspc.1 say that x does not depend on x?

[Thierry Arnoux]

The goal of rspc.2 is to state that `ps` is the same as `ph`, with all instances of `x` replaced by `A.

So logically there should not be any instance of `x` remaining in `ps`.

There are two ways to state this constraint:

• the first way is using the "distinct variable conditions", which is used in `~ rspcv`
• the second way is using a "not free" hypothesis, which is indeed what `rspc.1` is for.

On the website page, the "allowed substitution hint" lists all substitutions which are not forbidden in the first way, by a "distinct variable conditions".

It is a facility which is built automatically, but does not take the "not free hypotheses" into account, therefore the name "hint".

So you're right to point out that that in this case, while it's not disallowed by distinct variable conditions, it's actually disallowed by the not free hypothesis `rspc.1`

BR,
_
Thierry

On 01/03/2025 17:11, bil...@gmail.com wrote:

Theorem rspc has the allowed substitution hint ps(x).

Is this correct? Doesn't the hypothesis rspc.1 say that x does not depend on x?

--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/metamath/c8a236ac-28c6-4d04-a221-f2a556ee8819n%40googlegroups.com.

[Glauco]

In the following example, x can appear in ps. However, since it is bounded (see step 1), this does not pose an issue.

1::nfrab1            |- F/_ x { x e. RR | x < 5 }
2:1:nfel2           |- F/ x A e. { x e. RR | x < 5 }
3::eleq1            |- ( x = A -> ( x e. { x e. RR | x < 5 } <-> A e. { x e. RR | x < 5 } ) )
qed:2,3:rspc       |- ( A e. V -> ( A. x e. V x e. { x e. RR | x < 5 } -> A e. { x e. RR | x < 5 } ) )

$= ( cv c5 clt wbr cr crab wcel nfrab1 nfel2 eleq1 rspc ) ADZOEFGZAHIZJBQJABCAB
   QPAHKLOBQMN $.

$d A x
$d V x