> > 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 > As far as I can tell, the Metamath language has been restricted more and more over time: first "mandatory spaces between tokens", then in 2006 (according to the book) "math symbols and statement labels share namespace", and then "variable types are global" (a restriction I've never seen in any other computer language). Even C#, which disallows variable shadowing, doesn't have this. I believe that although the first restriction simplified the language greatly (by not special casing certain characters and tokens), the later restrictions complicate both the machine side (verifier development) and the human side (inputting axioms and theorems) of Metamath.
- Without the namespace restriction I could manage statements and math symbols with two list variables. With the restriction I must either check that the two namespaces do not intersect or use one list for both and annotating whether an identifier refers to a symbol or a proposition. It is supposedly added to make writing certain parsers easier, but in my opinion some other parsers are more complicated. - The "variable types are global" restriction is outright silly. The purpose of variable scoping is to declare that variables with the same name in different scopes are different variables. This also requires verifiers keep track of local variable scope and global variable types *at the same time*. Isn't it stupid? This also wreaks havoc with included files, which may declare common variable names with unrelated types, a problem exacerbated by the lack of a real module/namespace system. - The implicit disjoint variable restriction is even worse. The Metamath program developed by Norman Megill in C clearly has the ability to determine which variables are dummy. Also, "implicit" distinct variables don't even exist because they don't matter to users of the theorem (after all, you can reprove the theorem under a different name without the redundant disjoint restrictions with a short proof referencing the original theorem). Even if we assume that these restrictions make writing tools simple, the simplest solution is no code, no computer, no automation at all and letting people write and verify proofs in the informal style, which defeats the entire point of Metamath. Also repeatedly making backwards incompatible changes to a program for no good reason and without a conversion/migration tool is poor practice. We will never know how many private databases were, are and will be broken by the introduction of the restrictions. Anyway, I was trying to axiomatize the not-free predicate as follows: If a variable x does not occur in an expression S then x is not free in S. If S is a quantifier expression (of the form forall x: P, exists x: P, et cetera) then x, being quantified over is not free. If S1, S2 are arbitrary sequences of symbols, neither contains x, S is an expression in which x is not free and the sequence S1 S S2 is an expression then x is not free in S1 S S2. -- 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/13d2d19f-8864-44fa-a027-b5ffc21bf873%40googlegroups.com.
