It seems you are asking several things, let's back up a little. It might help if you explain a little more what your application is, and why equality is not desirable, since you have to go through some hoops to eliminate it and still have a complete FOL. In most systems of practical interest, you're going to be adding in equality axioms anyway, so usually there's no reason not to include it from the start.
But aside from that, with or without equality, if you are asking for a system that has primitive notions of free variable and proper substitution exactly as stated in textbooks, it can be done in Metamath with a significantly more complex foundation (discussed in the Google Group thread I'm linking to below) that offers no advantages. These notions are usually stated informally in English as side conditions in textbooks and accompanied in the text with verbal descriptions of the algorithms to check that a variable is free etc. Tarski's paper I mentioned, on pp. 63-67, shows how to formalize these informal notions of the traditional system. Their significant complexity, when formalized, led him to the simplified system that we use. Keep in mind that both our (Tarski's) and the traditional system are expressed with axiom schemes. Each scheme represents (can be instantiated with) an infinite number of actual axioms (the object language). The important thing is that both Tarski's system and the traditional system generate exactly the same set of object language axioms. This is discussed here, which also shows the traditional schemes and how we can approximate them in in Tarski's system: http://us.metamath.org/mpeuni/mmset.html#traditional As for understanding axiom schemes vs. the object language axioms, this might be helpful: http://us.metamath.org/mpeuni/mmset.html#axiomnote The 2017 thread starting below is somewhat long, but I think it addresses some of the things you are asking and might be worth reading or at least skimming through in its entirety: "learning formal logic, feature request" https://groups.google.com/d/msg/metamath/hOo18rTwUBM/dASE79_qAAAJ --- As for the language restrictions you mention: > the typecode of variables are global This was recently added to the spec at the request of Mario Carneiro I believe, but I can't locate the message right now, perhaps he can refresh my memory. All of our databases did that anyway so it had no effect on any existing work. > label tokens may not collide with math symbol tokens I agree this is somewhat silly, but at least one and perhaps two writers of early verifiers requested this because they used a single name space to make parsing faster or something. It seems relatively harmless since a violation can be detected and fixed instantly. If in the future there is a pressing need not to have it, the requirement can always be dropped (at the expense of those verifiers), but once dropped we can never go back without possibly having to fix multiple databases. > dummy disjoint variable restrictions are required This has been debated off and on and is discussed here: http://us.metamath.org/mpeuni/mmset.html#dvnote2 Essentially it simplifies the language slightly and makes it more transparent (no hidden implicit distinct variables). Norm On Sunday, October 20, 2019 at 8:44:20 PM UTC-4, Brian Nguyen wrote: > > > 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/c5d945ce-6961-4ca6-a17b-d81936a05d67%40googlegroups.com.
