learning formal logic, feature request

[Patrick Thomas]

Hi,

I am just starting out learning formal logic and have been going through "First Order Mathematical Logic" by Angelo Margaris. I have played around with Metamath and have succeeded in using it to create simple proofs in propositional logic. I really like it, and I would like to continue to use it to check my work on the exercises in Margaris' text. In regard to this, I was wondering if it might be possible to add the conditions of metalogic used in the book's axioms, for example, "not free in", to the coded metalogic of Metamath? If it is possible, but not desirable to do so, would it be feasible to create a spinoff of Metamath to do this?

Thank you very much for your time,
Patrick

[Thierry Arnoux]

Hi Patrick,

This already exists either as $d x ph $. for "x is not free in ph", or
as the construct "F/ x ph". I suppose this shall cover your needs!

BR,
_
Thierry

[Norman Megill]

First of all, one important thing to keep in mind is a clear distinction between the actual formal system (which we also call the object system) and the metalogic that represents the formal system.  On p. 47 of Margaris, note that the formal system does not include the symbols P and Q, which are metavariables used to define formulas: "If P and Q are formulas, then (P -> Q) is a formula" etc. (p. 48).  The expression "(P -> Q)" is not itself a formula; it is an expression ranging over formulas built from the small set of symbols on p. 47.  Margaris (like most books) almost immediately abandons the object language and uses just the metalanguage for most of his development.  Even the propositional calculus "theorem" "(P -> P)" is not a theorem of the object language but a metatheorem (theorem scheme) ranging over many such theorems.

Now look at say axiom A6 on p. 49, "P -> A. v P, provided v is not free in P".  Again, this is not a statement in the formal language but a scheme ranging over many formulas in the language of p. 47.  The condition "v is not free in P" is the implicit result of an algorithm that breaks down the structure of an instance (using the symbols of p. 47) of formula P and returns "yes" if the formula satisfies the recursive definition of "not free in".  In the formal object language, there is no primitive concept of "not free in".

Metamath does not have the ability to break down an object language formula in this way.  Instead, it (i.e. set.mm) uses a logically equivalent system with much simpler rules, using only the concepts of two variables not being identical and of a variable not occurring in a formula.  The set of object language formulas generated by set.mm's axioms is exactly the same as those of Margaris's written in the language of p. 47.  Here by "generate" I mean in a mathematical sense. Metamath does not have the ability to work with actual object language formulas; we only imagine that.  Just as Margaris abandons the p. 47 formal notation almost immediately and manipulates metavariables P and Q instead, Metamath also works only with the metalanguage of logic.

Now, a problem with working with the metalanguage to prove schemes of theorems involving "not free in" and "free for" conditions is that there is a lot of implicit complexity going on behind the scenes that needs rules not part of the axiom system.  These rules can be formalized using set theory to describe the metalogic, but it isn't simple. (Tarski's 1965 paper gives a set theoretical description.)  In practice, we informally keep track of the "not free in" requirements of a particular theorems in our heads and carefully propagate them as required throughout a proof.

In set.mm's system, we also have to propagate the requirements "x and y are distinct" and "x doesn't occur in P", but they are much simpler and are built into Metamath's underlying system.

As Thierry notes, we can emulate Margaris' "not free in" notion with a logically (nearly) equivalent condition "F/ x P" which is an abbreviation for "A. x ( P -> A. x P )" (our definition df-nf).  As a special case, if variable x does not occur in P, indicated by $d x P $. we automatically have F/ x P (our theorem nfv),  As you've probably noticed, we prove most of Margaris's 19.* theorems of pp. 89-90, and you may find it instructive to compare the set.mm versions (type 'show statement 19.*' in the metamath program) with Margaris' in order to see their relationship.  If you get stuck on one of his exercises due to our slightly different concepts, post a question here and I'm sure people will be glad to answer.

I think it will be helpful to read the following sections:

http://us.metamath.org/mpegif/mmset.html#axiomnote has a more careful explanation of the above.

http://us.metamath.org/mpegif/mmset.html#traditional shows the axioms of the most common traditional textbook system (it is logically equivalent to Margaris', which is less common) and links to the (almost) logically equivalent theorems of the set.mm system.

http://us.metamath.org/mpegif/mmset.html#distinct describes the distinct variable conditions that we often use instead of "not free in" and "free for".

Norm

[Patrick Thomas]

Thank you very much for your detailed response.

I think in the end I am looking for a means to write proofs in the same manner as is done in the examples given in the text, using theorems of metalogic like the deduction theorem and invoking the traditional axioms as necessary. I was imagining accomplishing this through an extension to Metamath to allow for the direct use of the traditional axioms and the creation of a translation program to expand the application of metatheorms using the algorithms given in their proofs. Perhaps this is not a good approach or not suited to the aims of Metamath? I have looked at other programs, but so far I have not found any that seem as applicable. Would you happen to know of one?

[Mario Carneiro]

Hi Patrick,

Let me give my own point of view on the subject. One thing which I think logic textbooks ignore or at least don't acknowledge to an appropriate extent is the distinction between meta and object level, particularly as it pertains to treating metatheorems as theorems. Metamath, like any other formal system, is an object language in its own right, and any metatheorems about this language will, by their very nature, not be expressible within the system. Tarski showed us that this will always be the case - "semantically closed" languages lead directly to the liar paradox.

This means that if you want to formalize metatheorems, you have to make a deliberate choice: should the formal system I am constructing be the object language, in which case the metatheorems will only be shown in every particular case (possibly helped along by automation), or should it be the metalanguage, in which metatheorems are directly expressible in generality, but the lower object language is only indirectly referenced (i.e. you have "proofs of proofs" in the object language, which may or may not lift to real proofs depending on the axioms of the metalanguage).

As should be clear, Metamath positions itself in the second camp. As a matter of fact, it is quite possible to even express the true, syntactic "x is free in ph" restriction in Metamath; it is not done simply because this requires an axiomatic extension for no obvious gain.

The deduction theorem can also be expressed in Metamath, but it requires some care in understanding the "units" in a derivation. In a Gentzen logic where you have a rule like

(|- ph => |- ps) => |- ph -> ps

(the so-called I-intro rule), which cannot be written in Metamath in this form, we must instead explicitly indicate the context of assumptions to get the "sequent" form:

Gamma, ph |- ps => Gamma |- ph -> ps

and in this form it is quite natural to express in Metamath, where now provable assertions have the form "Gamma |- ph" instead of just "|- ph". But if you write down a logical system based on this approach (as several have done), you notice that in fact you have gained nothing new by writing "Gamma |- ph" instead of just "|- ( Gamma -> ph )" - the theorems are all the same. So in set.mm we economize, and simply interpret |- ( ph -> ps ) as a deduction from context "ph" when it is convenient to do so. With this lens, the deduction theorem simply translates to the theorem http://us2.metamath.org:88/mpegif/ex.html , which is not difficult to state or prove as an "object theorem" of Metamath rather than a metatheorem over it.

Metamath's unusual combination of object language-style straightforward derivations and metalanguage interpretation gives it enough power to prove most metatheorems that are expressible in its language (this is sometimes referred to as "metalogical completeness" in the Metamath literature), which has great practical upshoots. For other metatheorems that are not so expressible, such as the provability of theorems of the form ( x = y -> P(x) = P(y) ) where P(x) is a Metamath expression containing a variable x, we can resort to the first option for handling object language formal system, and write a proof procedure for goals of this form within one of the Metamath IDEs. (This is what mmj2 does.)

Mario

--
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 metamath+unsubscribe@googlegroups.com.
To post to this group, send email to meta...@googlegroups.com.
Visit this group at https://groups.google.com/group/metamath.
For more options, visit https://groups.google.com/d/optout.

[Patrick Thomas]

"it is quite possible to even express the true, syntactic "x is free in ph" restriction in Metamath"

When you say in Metamath, do you mean in the code for the proof verifier, or in the text being verified, i.e. set.mm?

To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.

[Mario Carneiro]

On Sat, May 6, 2017 at 8:45 PM, Patrick Thomas <pthom...@gmail.com> wrote:

"it is quite possible to even express the true, syntactic "x is free in ph" restriction in Metamath"

When you say in Metamath, do you mean in the code for the proof verifier, or in the text being verified, i.e. set.mm?

The Metamath language in its full generality is extremely flexible (sometimes too flexible), and basically every formal system I have ever seen can be encoded within it. By that I mean that *no* changes to the verifier code are needed for these encodings - one must simply provide appropriate syntax and axioms within the .mm file. Most of the time we will interested in a conventional logic which does not significantly differ from set.mm (and all of the things I mentioned fall in this category), so we can make do with perturbations to the set.mm axiom set. If you take it all out and start from scratch, the possibilities expand considerably, until we are formalizing string rewriting systems that look very little like mathematical logics, but that's getting a bit far afield.

[David A. Wheeler]

> As a
>matter of fact, it is quite possible to even express the true,
>syntactic "x
>is free in ph" restriction in Metamath; it is not done simply because
>this
>requires an axiomatic extension for no obvious gain.

I was not aware that this was even possible. What is the axiomatic extension? Matching the conventions of other texts even more precisely might be considered a gain.


Mario:
--- David A.Wheeler

[Mario Carneiro]

Basically anything with an inductive definition can be axiomatized with a few axiom (schemes) in metamath. For "x free in ph", denoted "NF x ph", we could have the following:

$d x y => $d x z => |- NF x y = z
$d x y => $d x z => |- NF x y e. z
|- NF x ph => |- NF x ps => |- NF x ( ph -> ps )
|- NF x ph => |- NF x -. ph
|- NF x A. x ph
$d x y => |- NF x ph => |- NF x A. y ph

Now there is a metatheorem stating that |- NF x ph is a theorem of this system if and only if all object language substitutions of ph and x satisfy "x is not free in ph". In particular, in the special case where ph contains only set variables and these are all disjoint (so that it is interchangeable with a single object language expression), we will have |- NF x ph if and only if x is not free in ph.

Mario

[Mario Carneiro]

Note, however, that this would not allow proving |- NF x E. x ph, because we don't have a theorem like |- ( ph <-> ps ) => |- NF x ph => |- NF x ps, and if we added this, we would get the exact same thing as F/ (because theorems are equivalent to the constant true). So we would need to introduce a new operation "<->df" used for introduction of definitions, along which NF is preserved, but avoid transferring NF along arbitrary biconditionals.

Mario

[David A. Wheeler]

On May 7, 2017 1:59:11 AM EDT, Mario Carneiro <di....@gmail.com> wrote:
>Note, however, that this would not allow proving |- NF x E. x ph,
>because
>we don't have a theorem like |- ( ph <-> ps ) => |- NF x ph => |- NF x
>ps,
>and if we added this, we would get the exact same thing as F/ (because
>theorems are equivalent to the constant true). So we would need to
>introduce a new operation "<->df" used for introduction of definitions,
>along which NF is preserved, but avoid transferring NF along arbitrary
>biconditionals.

I am sure that I do not understand all the ramifications, but "not free in" is an extremely common assertion, and having an exact representation of it might be a real advantage.


--- David A.Wheeler

[Patrick Thomas]

Searching through previous posts containing the phrase "not free in", I came upon the following statement by Norm:

"In principle, the proper way to add "not free in" would be a $nf x ph $. metamath language extension where $d now goes, but of course that can't be implemented in the present Metamath framework nor do we want to complicate the language that way." [1]

[1] https://groups.google.com/d/msg/metamath/yMgoFfmBnMQ/9I4qUCV8BgAJ

I am curious as to why it can not be implemented and the reasons not to.

[Patrick Thomas]

I think I understand the first part. You seem to be saying that we could create axioms just to deal with proving if a variable is not free in a given formula. For example, if we hypothesize that x is not free in P and Q then we can use these axioms to prove that x is not free in forall x R -> (~P -> Q). Using this approach we could state the axiom of predicate calculus that "P -> forall v P provided v is not free in P" using NF v P as a hypothesis to "P -> forall v P". To use this axiom we would have to show (using our additional axioms) that the variable we substitute for v is not free in the formula we substitute for P. Is this correct?

I'm not sure I follow what you are saying in this post. Would you mind elaborating?

[Patrick Thomas]

Isn't exists v P defined as ~forall v ~P. Then since v is not free in forall v ~P it is not free in ~forall v ~P?

[Mario Carneiro]

On Sun, May 7, 2017 at 3:39 PM, Patrick Thomas <pthom...@gmail.com> wrote:

Searching through previous posts containing the phrase "not free in", I came upon the following statement by Norm:

"In principle, the proper way to add "not free in" would be a $nf x ph $. metamath language extension where $d now goes, but of course that can't be implemented in the present Metamath framework nor do we want to complicate the language that way." [1]

[1] https://groups.google.com/d/msg/metamath/yMgoFfmBnMQ/9I4qUCV8BgAJ

I am curious as to why it can not be implemented and the reasons not to.

It occurs to me that the fact that NF *is* implementable in Metamath may not not widely known, because it has never been a specific point of discussion (and we feel we have a workaround that better achieves our other objectives of parsimony, etc.).

I believe the sense in which $nf "can't be implemented in the present Metamath framework" is simply that it doesn't fit in the Metamath specification as written, which would mean changing all the verifiers and a lot more community pushback. It might be more common in other languages to tweak with the foundations on an ongoing basis, but Metamath has a much more rigid specification and a community that expects this rigidity, partly because it is already so flexible in the actual formal languages it can implement. (That's not to say that it's absolutely beyond question, but you will see much more resistance to changes to the base Metamath spec than you would get in, say, the Coq community) We instead use a "language-within-a-language" approach to making variant notations and idioms *within* the base framework (for example, modifying the axioms of set.mm) to express what we can.

I'm curious to see whether Norm is aware of the aforementioned trick to represent NF as a provable assertion with limited proof rules (note that "NF x ph" as I defined it is not a wff, so it can't be proven by the usual methods of propositional logic - you *must* use the inductive NF builders, which is how you get the sharp result about provability).

To address the second part of your question (reasons not to), the answer is simple: we already have a "not free" predicate which does everything we need in every practical scenario. One can replace the metalogical assertion "x is not free in ph" with the hypothesis |- F/ x ph and you will get all the same theorems as Margaris. (You will also get a few more, in particular theorem nfth, but NF implies F/, and any metatheorem containing NF as a hypothesis asserting provability of something is still a theorem if you replace NF with F/, so *within the logic* it is impossible to distinguish the two.) Another way to put it is that F/ x ph is the strongest propositional function satisfying NF x ph -> F/ x ph, where by propositional function I mean that its truth value depends only on the value of ph(x), rather than on its syntactic form. (For example, "ph(x) is valid, i.e. true for all values of x" is a propositional function, but "ph(x) contains an even number of occurrences of x" is not.)

On Sun, May 7, 2017 at 6:03 PM, Patrick Thomas <pthom...@gmail.com> wrote:

I think I understand the first part. You seem to be saying that we could create axioms just to deal with proving if a variable is not free in a given formula. For example, if we hypothesize that x is not free in P and Q then we can use these axioms to prove that x is not free in forall x R -> (~P -> Q). Using this approach we could state the axiom of predicate calculus that "P -> forall v P provided v is not free in P" using NF v P as a hypothesis to "P -> forall v P". To use this axiom we would have to show (using our additional axioms) that the variable we substitute for v is not free in the formula we substitute for P. Is this correct?

 

Yes, that's correct. We can also use a proof procedure to fulfill these goals (in metamath IDEs) due to their formulaic nature.

On Saturday, May 6, 2017 at 10:59:12 PM UTC-7, Mario Carneiro wrote:

Note, however, that this would not allow proving |- NF x E. x ph, because we don't have a theorem like |- ( ph <-> ps ) => |- NF x ph => |- NF x ps, and if we added this, we would get the exact same thing as F/ (because theorems are equivalent to the constant true). So we would need to introduce a new operation "<->df" used for introduction of definitions, along which NF is preserved, but avoid transferring NF along arbitrary biconditionals.

I'm not sure I follow what you are saying in this post. Would you mind elaborating?

Isn't exists v P defined as ~forall v ~P. Then since v is not free in forall v ~P it is not free in ~forall v ~P?

In Metamath, definitions are just axioms with a certain form, asserting the biconditional of two propositions (where one side involves a new syntax construction). In set.mm, exists is defined as follows:

wex $a wff E. x ph $.

df-ex $a |- ( E. x ph <-> -. A. x -. ph )

The first axiom states that "E. x ph" is a valid wff expression whenever x is a set variable and ph is a wff expression. (This is called a "syntax axiom".) The second axiom is the "definition", and asserts that the wff "E. x ph <-> -. A. x -. ph" is provable, where "<->" has its usual meaning as the biconditional propositional connective. (In fact, even the biconditional is a definition, but we can't use it to introduce itself - you might find df-bi interesting to see how we circumvent this.) If we didn't have the second axiom, "E. x ph" would still be usable where wffs are expected, we just wouldn't know anything about its "value".

The critical difference between NF and F/ has to do with how they handle equivalent propositions. NF is not closed under equivalence of expressions, but F/ is. That is, |- ( ph <-> ps ) implies |- ( F/ x ph <-> F/ x ps ) but not |- ( NF x ph <-> NF x ps ). If we had the latter, we could deduce from |- ( x = x <-> y = y ) to |- ( NF x x = x <-> NF x y = y ), show that x is not free in y = y, and thus deduce that x is not free in x = x. This is exactly where F/ diverges from "not free" in the conventional sense - we are comfortable asserting |- F/ x x = x because the dependence on x is inessential, since we can swap it out for an equivalent proposition that doesn't have an x in it.

If we want to say that we are allowed to deduce |- NF x E. x ph from |- NF x -. A. x -. ph, because this is the "definition" of E., but not allow transferring |- NF x y = y to |- NF x x = x, we need a way of distinguishing these two cases. One way to do so is to introduce a new primitive operation "<->df", which asserts that this is a definitional equality, not merely an equivalence of expressions. (This is a very common technique in intentional type theory.) It would have the following axioms:

|- ( ph <->df ps ) => |- ( ph <-> ps )
|- ( ph <->df ps ) => |- NF x ps => NF x ph

In particular, <->df is not symmetric, and there is no way to prove a definitional equality, so the only definitional equalities will be coming from the axioms, and you can only deduce the not-free constructors from definiens to definiendum.

You might also notice that $d x ph is a syntactic constraint, not a propositional function, and you may wonder if the claims I have made for NF cannot also be applied for $d. Why not have a provable assertion |- DV x ph or |- DV x y which has the same meaning as $d x ph or $d x y? We would need to introduce a lot of axioms, one for every syntax constructor, saying something like

|- DV x y => |- DV x ph => DV x E. y ph

but it could be done. As a matter of fact, for two set variables DV x y turns out to be a propositional function, and is equivalent to the wff "-. A. x x = y", which you will sometimes find referred to as a "distinctor".

Norm investigated exactly this possibility a while back, and he ran into problems with the buildup of distinctor assumptions. I have a different way to phrase the problem. There is a rule in Metamath, built right into the foundations, that says that for any finite collection of variables, and for any type, there is a variable of that type that is ($d) distinct from all of them. This implies that the supply of object variables that the metavariables range over is infinite, which accords with most presentations of logic. (The actual place where this rule is invoked is the fact that any additional variables introduced in a proof (dummy variables), together with any $d pairs they participate in, are forgotten outside the confines of that proof.) Without this rule, one is saddled with a potential paucity of variables in the object language - the theorems being asserted look like "if there are at least five different variables v_0,...,v_4, then A. x A. y ph implies A. y A. x ph" or some such.

Unfortunately, there is a sense in which Norm's problem is provably impossible to overcome. If the language had no $d's, then all substitutions would be valid. If |- ph(x) has a proof with intermediate steps mentioning the variable y, then by substituting y for x uniformly throughout the proof we get a proof of |- ph(x) which does not mention y, so all dummy variables are eliminable, and no proof can depend on them essentially. Since we know that some theorems cannot be proven without dummy variables (this is due to Andreka IIRC), this hypothetical system cannot suffice for FOL.

Mario

[Norman Megill]

On Sunday, May 7, 2017 at 6:54:39 PM UTC-4, Mario Carneiro wrote:

On Sun, May 7, 2017 at 3:39 PM, Patrick Thomas wrote:

Searching through previous posts containing the phrase "not free in", I came upon the following statement by Norm:

"In principle, the proper way to add "not free in" would be a $nf x ph $. metamath language extension where $d now goes, but of course that can't be implemented in the present Metamath framework nor do we want to complicate the language that way." [1]

[1] https://groups.google.com/d/msg/metamath/yMgoFfmBnMQ/9I4qUCV8BgAJ

I am curious as to why it can not be implemented and the reasons not to.

It occurs to me that the fact that NF *is* implementable in Metamath may not not widely known, because it has never been a specific point of discussion (and we feel we have a workaround that better achieves our other objectives of parsimony, etc.).

Mario is correct.  I didn't think of his method of introducing NF with new axioms.  I'm not infallible. :)   I also agree with Mario that our present F/ is essentially a stronger version of NF;  whenever NF is true, so is F/.   To me F/ has many advantages over NF:  no axioms are needed to introduce F/, no new primitive concepts are needed, and F/ is an ordinary wff that can be manipulated with any of the theorems we already have for wffs.

Since we're on this topic, another notion that is also needed traditionally is "free for" that is present in two of the axioms for FOL+equality:

http://us.metamath.org/mpegif/mmset.html#traditional

We emulate this using proper substitution.  Unlike F/ vs. NF, our proper substitution does give us an exact logical equivalent when "free for" is true, and it also works in cases where "free for" is not true.

Mario, how would you go about defining the exact notion of "free for" in Metamath?  In Hirst and Hirst's "A Primer for Logic and Proof" p. 49, "A term t is free for a variable x in the formula P if x does not occur free within the scope of a quantifier on a variable in t."  They spend 3 pages explaining it and giving examples, suggesting it is something beginners may find confusing.

Norm

[Norman Megill]

On Saturday, May 6, 2017 at 8:26:59 PM UTC-4, Mario Carneiro wrote:
[...]

Metamath's unusual combination of object language-style straightforward derivations and metalanguage interpretation gives it enough power to prove most metatheorems that are expressible in its language (this is sometimes referred to as "metalogical completeness" in the Metamath literature), which has great practical upshoots. For other metatheorems that are not so expressible, such as the provability of theorems of the form ( x = y -> P(x) = P(y) ) where P(x) is a Metamath expression containing a variable x, we can resort to the first option for handling object language formal system, and write a proof procedure for goals of this form within one of the Metamath IDEs. (This is what mmj2 does.)

I would claim that the set.mm FOL+equality axioms are able to prove all (not most) FOL+equality metatheorems that are expressible in its language.  "Its language" means formulas built with ->, -., A., containing set and wff metavariables (the latter having no arguments as in "phi(x)", although "[x/y]phi" is fine), and $d conditions. Do you doubt this or know of such a metatheorem that is not provable?

Norm

[Patrick Thomas]

Is "free for" related to the condition on axiom 5 of Margaris: forall v P -> P(t/v) provided P admits t for v? That is, this axiom could equivalently be stated with the condition "provided t is free for v in P"?

[Mario Carneiro]

No, I just couldn't remember the exact conditions of the theorem, and I didn't want to overreach.

On Sun, May 7, 2017 at 8:16 PM, Norman Megill <n...@alum.mit.edu> wrote:

Mario, how would you go about defining the exact notion of "free for" in Metamath?  In Hirst and Hirst's "A Primer for Logic and Proof" p. 49, "A term t is free for a variable x in the formula P if x does not occur free within the scope of a quantifier on a variable in t."  They spend 3 pages explaining it and giving examples, suggesting it is something beginners may find confusing.

(Note that in set.mm, this only makes sense in the extension of FOL + classes, since it involves terms and substitution of a term for a variable.) I found a semi-formal definition of this notion in terms of "free for" (https://math.stackexchange.com/a/134732/50776):

A term 'A' is free for 'x' in 'ph' (let's denote this "|- FF [ A / x ] ph") if for every subterm of the form 'A. y ps' in ph, if y is free in A, then x is not free in ps.

As such, we could define it by induction on ph (where NF is defined inductively as it was before, with the obvious extension to "NF y A"):

|- NF x ph => |- FF [ A / x ] ph
|- FF [ A / x ] ph => |- FF [ A / x ] -. ph
|- FF [ A / x ] ph => |- FF [ A / x ] ps => |- FF [ A / x ] ( ph -> ps )
$d x y => |- NF y A => |- FF [ A / x ] ph => |- FF [ A / x ] A. y ph

The disjunction in the original definition (either y is not free in A or x is not free in ps) is handled here by the two possible proof methods for |- FF [ A / x ] A. y ph:

|- NF y A => |- FF [ A / x ] ph => |- FF [ A / x ] A. y ph
-or-
|- NF x A. y ph => |- FF [ A / x ] A. y ph

where in the second case we can use $d x y => |- NF x ph => |- NF x A. y ph.

On Mon, May 8, 2017 at 1:13 AM, Patrick Thomas <pthom...@gmail.com> wrote:

Is "free for" related to the condition on axiom 5 of Margaris: forall v P -> P(t/v) provided P admits t for v? That is, this axiom could equivalently be stated with the condition "provided t is free for v in P"?

Yes, that appears to be alternate wording for the same thing.

At this point I ought to point out what the set.mm equivalent to "free for" is. I could point at a4sbc, which on the surface looks very similar, but there isn't really any substitution going on there - the definition [. A / x ]. ph is essentially just a promise to resolve the substitution eventually - it still contains "ph", with 'x' still present, as a subterm. Instead, I think the best place to point to see how it works is theorem cla4gf:

|- F/ x A => |- F/ x ps => |- ( x = A -> ( ph <-> ps ) ) => |- ( A e. V -> ( A. x ph -> ps ) )

The metatheorem that makes this work is the fact that if ph(x) is a wff with free variable x, then the substituted term ph(A) is out there somewhere (even if it's not easily definable from ph), and although we can't just construct it, we "know it when we see it" - the hypotheses of this theorem can only be satisfied by the real substitution ps := ph(A) (or a wff equivalent to it). So we let the user (of the theorem) supply the correct substituted term instead, and we only have to check that it works.

So where is all the magic of the standard FOL "free for" definition hiding? In the equality theorems:

albid $p |- F/ x ph => |- ( ph -> ( ps <-> ch ) ) => |- ( ph -> ( A. x ps <-> A. x ch ) )

If we were trying to sneak past a quantifier in proving, say, FF [ y / x ] A. y x = y (which doesn't hold because the y in the substitution will get captured by the forall), the Metamath equivalent would be attempting to prove

|- ( x = y -> ( A. y x = y <-> A. y y = y ) ).

If we apply albid, we would get the proof obligation F/ y x = y, which is not provable. Of course, since this is a provable statement instead of a syntactic rule, we could try alternate methods to prove the goal, but in this case the statement is false so that's not going to work. On the other hand, it is this freedom to find alternate proofs that allows us to do alpha-renaming - for example, with a better choice of substitution, we could instead prove

|- ( x = y -> ( A. y x = y <-> A. z y = z ) ).

which we can do:

1. eqeq2 |- ( y = z -> ( x = y <-> x = z ) )
2:1. cbvalv |- ( A. y x = y <-> A. z x = z )
3. eqeq1 |- ( x = y -> ( x = z <-> y = z ) )
4:3. albidv |- ( x = y -> ( A. z x = z <-> A. z y = z ) )
5:2,4. syl5bb |- ( x = y -> ( A. y x = y <-> A. z y = z ) )

Mario

[David A. Wheeler]

> On Sun, May 7, 2017 at 8:16 PM, Norman Megill <n...@alum.mit.edu> wrote:
> > Mario, how would you go about defining the exact notion of "free for" in
> > Metamath? In Hirst and Hirst's "A Primer for Logic and Proof" p. 49, "A
> > term t is free for a variable x in the formula P if x does not occur free
> > within the scope of a quantifier on a variable in t." They spend 3 pages
> > explaining it and giving examples, suggesting it is something beginners may
> > find confusing.
> >

On Mon, 8 May 2017 01:49:05 -0400, Mario Carneiro <di....@gmail.com> wrote:
> (Note that in set.mm, this only makes sense in the extension of FOL +
> classes, since it involves terms and substitution of a term for a
> variable.) I found a semi-formal definition of this notion in terms of
> "free for" (https://math.stackexchange.com/a/134732/50776):
>
> A term 'A' is free for 'x' in 'ph' (let's denote this "|- FF [ A / x ] ph")
> if for every subterm of the form 'A. y ps' in ph, if y is free in A, then x
> is not free in ps.
>
> As such, we could define it by induction on ph (where NF is defined

> inductively as it was before, with the obvious extension to "NF y A"): ...

I think it would be a big improvement if set.mm included
a more traditional definition of "free for" as used in typical texts.
Even if it wasn't used much, it would show
that it's possible (and therefore is a choice of style, not a tool limitation).
Also, it'd then be possible to formally prove various relationships between
"kinds of freedom" - which might be interesting in its own right.
I don't know if this is the "right" way to do it, but it sounds interesting...!

--- David A. Wheeler

[Patrick Thomas]

I also like this idea, along with "not free in".

[Patrick Thomas]

Why are x and y required to be distinct in the last axiom: "$d x y => |- NF x ph => |- NF x A. y ph"?

[Mario Carneiro]

On Mon, May 8, 2017 at 11:30 PM, Patrick Thomas <pthom...@gmail.com> wrote:

Why are x and y required to be distinct in the last axiom: "$d x y => |- NF x ph => |- NF x A. y ph"?

This is a matter of taste, I think. The advantage of "unbundled" theorems is that they have a straightforward interpretation using the naive reading in FOL: if you see "NF x A. y ph" you will want to think of x and y as different variables, with "NF x A. x ph" handled separately. You may or may not also want to have *unique* proofs of these theorems, corresponding to the fact that the expressions are freely generated by the inductive generators, in which case you would want exactly one of the axioms to apply in any particular instance.

There are no provided methods for bundling the axioms, so I think that "|- NF x ph => |- NF x A. y ph" will not itself be provable even though all ground substitutions of it will be (since "|- NF x ph => |- NF x A. x ph" is provable by ignoring the hypothesis and applying the axiom "|- NF x A. x ph"), so this would be a logically complete but not metalogically complete set of axioms.

If you prefer bundled theorems to unbundled, then you would instead want to take |- NF x ph => |- NF x A. y ph as an axiom, since it is simpler to state and is still valid.

On Mon, May 8, 2017 at 6:27 PM, David A. Wheeler <dwhe...@dwheeler.com> wrote:

I think it would be a big improvement if set.mm included
a more traditional definition of "free for" as used in typical texts.
Even if it wasn't used much, it would show
that it's possible (and therefore is a choice of style, not a tool limitation).
Also, it'd then be possible to formally prove various relationships between
"kinds of freedom" - which might be interesting in its own right.
I don't know if this is the "right" way to do it, but it sounds interesting...!

I'm torn on this. Firstly, any axiomatic extensions should definitely be relegated to a mathbox, because we don't want to reference these axioms in real proofs. Secondly, because of the "shallow embedding" of this notion within the system, Metamath will actually not be able to prove any properties about NF. The *only* thing it can do is prove that certain wffs satisfy NF when they are not free. It's not even possible to prove that x is free in a wff containing free x - the fact that |- NF x ph is unprovable is a metatheorem of the system. This is the downside of encoding facts at the top level, where there are no available methods of reasoning.

The actual appropriate place for such a development is at the "deep embedding" level, in which set.mm defines the concepts of formal logic - what is a language, what is a wff, what is a model for that language, etc. Here we are well within the framework of ZFC set theory, and a wff is a certain kind of string of symbols, a model is a set with certain properties, and so on. At this level, Metamath is acting as the metalanguage to directly observe an object language, and it can state and prove metatheorems about that language. This will feel much more like the metalevel reasoning you will find in the average logic textbook (which doesn't spend much time on deriving actual theorems of the system under study).

Mario