Why must we introduce b and c in 4.1 and 4.2 (as Assumptions for Conditional Proof)? Why not only one Constant? Why any at all?
To derive the conclusion, two universal quantifiers must be introduced. The rule of Universal Introduction requires a subproof that begins with the assumption of an arbitrary term, and concludes with a derivation about that term.
To derive ∀x∀y P(x,y)
from a set of premises, assume two arbitrary terms that do not occur free within any premise, say b, c
, and derive P(b,c)
, then discharge those assumptions.
Intuitively, how does ∃y expand and so universalise itself into ∀y?
It doesn't. They are different y
. What the proof is saying is:
∃y∀x (x=y)
is the premise. That is a promise that "There is something that is equal to everything".
- Let us use the label
a
for this thing that we are promised exists.
- Thus
∀x (x=a)
, which says "Anything equals a
"
- Let us take two arbitrary things
b
and c
.
- Since anything equals
a
, therefore b
does. b=a
.
- Since anything equals
a
, therefore c
does. c=a
.
- Well, since
b=a
and c=a
, therefore they equal each other. c=b
[by the rule of equality elimination]
- Since
c
is arbitrary, then we are saying "anything equals b
", that is ∀x (x=b)
- Since
b
is arbitrary, then we are saying ∀z ∀x (x=z)
. Well actually, we can use any symbol not already in ∀x (x=b)
, so we may also reuse y
and conclude ∀y ∀x (x=y)
.