> 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 > <http://www.google.com/url?q=http%3A%2F%2Fus.metamath.org%2Fmpeuni%2Fmmset.html%23bib&sa=D&sntz=1&usg=AFQjCNGtCABpROstIa1WKc--H3miyHs4Iw> > > Disclaimer: I haven't pursued this any further than what is stated in > Tarski's paper. > > Norm > Which doesn't solve the actual problem: encoding *exactly* traditional first-order logic without equality in Metamath. Whether it is a "conservative extension" does not matter. Is it possible to encode traditional first-order logic without equality with no additional symbols in Metamath?
-- 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/3dfdeca1-2351-47b4-b4aa-e683395734cc%40googlegroups.com.
