|Description: Extend wff definition to
include atomic formulas with the epsilon
(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 syntactical construction introduces a binary non-logical predicate
symbol ∈ (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
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
predicate has two arguments.
(Instead of introducing wel 1437 as an axiomatic statement, as was done in an
older version of this database, we introduce it by "proving" a
case of set theory's more general wcel 1436. This lets us avoid overloading
the ∈ connective, thus preventing ambiguity
that would complicate
certain Metamath parsers. However, logically wel 1437 is
considered to be a
primitive syntax, even though here it is artificially "derived"
wcel 1436. Note: To see the proof steps of this
syntax proof, type "show
proof wel /all" in the Metamath program.) (Contributed by NM,