One (sort of nit picky) point: what you say below (which looks correct)
is for set.mm
For iset.mm, there are four propositional logic primitives, both "for
all" and "there exists" as primitives, and the same as set.mm for x ∈ y
(the axioms of set theory are somewhat different, but "Equality, truth,
sets, arithmetic and so on all can be derived from those" still holds).
As for what a minimal syntax for iset.mm would be, according to
Alexander V. Kuznetsov (as cited at
https://en.wikipedia.org/wiki/Intuitionistic_logic#Non-interdefinability_of_operators
) there is a single-operator analogue to the stroke (for propositional
logic). I'm not aware of anything more minimal than what we have now for
predicate logic or set theory.
On 7/3/21 12:24 AM, Gustavo Gonçalves wrote:
(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]
<mailto:[email protected]>.
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/e7a9d008-c63a-46dc-aa28-f6162ea1ab56n%40googlegroups.com
<https://groups.google.com/d/msgid/metamath/e7a9d008-c63a-46dc-aa28-f6162ea1ab56n%40googlegroups.com?utm_medium=email&utm_source=footer>.
--
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/f763b31c-8d5c-3288-d226-d4aefab0a418%40panix.com.
