| Description: Extend wff definition to
include atomic formulas with the membership
predicate. This is read "𝑥 is an element of 𝑦",
"𝑥 is a
member of 𝑦", "𝑥 belongs to 𝑦",
or "𝑦 contains
𝑥". Note: The phrase "𝑦
includes 𝑥 " means "𝑥 is a
subset of 𝑦"; to use it also for 𝑥 ∈ 𝑦, as some authors
occasionally do, is poor form and causes confusion, according to George
Boolos (1992 lecture at MIT).
This syntactic construction introduces a binary non-logical predicate
symbol ∈ (stylized lowercase epsilon) into
our predicate calculus.
We will eventually use it for the membership predicate of set theory, but
that is irrelevant at this point: the predicate calculus axioms for ∈
apply to any arbitrary binary predicate symbol. "Non-logical"
means that
the predicate is presumed to have additional properties beyond the realm
of predicate calculus, although these additional properties are not
specified by predicate calculus itself but rather by the axioms of a
theory (in our case set theory) added to predicate calculus.
"Binary"
means that the predicate has two arguments.
(Instead of introducing wel 2082 as an axiomatic statement, as was done in an
older version of this database, we introduce it by "proving" a
special
case of set theory's more general wcel 2081. This lets us avoid overloading
the ∈ connective, thus preventing ambiguity
that would complicate
certain Metamath parsers. However, logically wel 2082 is
considered to be a
primitive syntax, even though here it is artificially "derived"
from
wcel 2081. Note: To see the proof steps of this
syntax proof, type "MM>
SHOW PROOF wel / ALL" in the Metamath program.) (Contributed by NM,
24-Jan-2006.) |
