(As I wrote this, I realized how long it took to get my point across, so I
included a TL;DR at the end.)
Now that I have more time to get back into learning about Metamath and its
principles, I saw that the whole theory of classes can be expressed using
the wff and setvars we use. It's just much more efficient and easier to
read/understand to create that abstraction.
I also took a peek into Whitehead and Russell's Principia Mathematica, and
how everything within propositional logic could be defined in terms of the
stroke (example: ¬P = (P|P) and P -> Q = (P|(Q|Q)), and so on)
So I started to wonder, how far can we go to reach the bare minimum of
syntax needed.
In terms of propositional logic, I get it that all binary connectives can
be written in terms of the stroke, so one. But I understand Metamath's
approach to use two (negation and implication) since it's much easier to
grasp.
We do need quantifiers for predicate logic, so we need to add "for all"
into the syntax. Existence can be derived from it using negation, so that's
all needed. And since classes can be algorithmically derived from those, is
that all we need?
When it comes to atomic formulas, set theory only requires (x ∈ y).
Equality, truth, sets, arithmetic and so on all can be derived from those.
I know we can get deeper phylosophically by asking "do we include setvars
and wffs as syntax? or do we consider them some sort of metasyntax?" that I
don't really plan to get into (unless it looks like it's needed).
*TL;DR* Informally speaking, is the only syntax we necessarily need (for
any x,y variables and any φ,ψ wff) :
{ (φ | ψ), ∀x, (x ∈ y) } ?
Cause if so, that's really beautiful! If not, I'd love to know what's
missing! Thank you for reading.
--
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 [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/e7a9d008-c63a-46dc-aa28-f6162ea1ab56n%40googlegroups.com.
