Metamath uses disjoint variables instead of proper substitution as a
primitive notion, and as stated in the Metamath book, "substitution and
equality are intimately tied to each other" in Tarski's system for
first-order logic with equality. The book also claims that "the traditional
approach is also possible", so how do I encode traditional first-order
logic without equality in Metamath? I tried something like this (added to
set.mm):
$c NFQ $.
$v S S_1 S_2 v $.
${
$f setvar v $.
$f wff S $.
$a wff NFQ v S $.
$d v S $.
$a |- NFQ v S $.
$}
${
$f setvar v $.
$f wff S_1 S S_2 $.
$f |- NFQ v S $.
$d v S_1 $.
$d v S_2 $.
$a |- NFQ x S_1 S S_2 $.
$}
but this doesn't work because Metamath requires every variable to have a
typecode. There are many other stupid restrictions in Metamath, for example
that the typecode of variables are global, that label tokens may not
collide with math symbol tokens, or that dummy disjoint variable
restrictions are required. How do I encode the traditional notion of free
variables and proper substitution in Metamath? And why do these useless
restrictions exist even though they have nothing to do with proof validity?
--
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/3bbe900e-583d-47ec-96bf-58673bbd2527%40googlegroups.com.
