Tarski's paper "A Simplified Formalization of Predicate Logic with Identity" shows how to do this on p. 78, last 2 paragraphs.
Essentially he assumes that there is at least one binary predicate (say e.) and defines a pseudo-equality x ~ y as A. z ( ( x e. z <-> y e. z ) /\ ( z e. x <-> z e. y ) ). He then adds additional axioms for x ~ y, see paper for details. A link to the paper is provided in the Tarski entry of the bibliography at http://us.metamath.org/mpeuni/mmset.html#bib Disclaimer: I haven't pursued this any further than what is stated in Tarski's paper. Norm On Sunday, October 20, 2019 at 1:31:01 PM UTC-4, Brian Nguyen wrote: > > 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/82bbe677-091f-416f-b2c6-2da8104a7387%40googlegroups.com.
