Talk:Substitution instance

Problems

I saw this article a while back, and hoped it would be improved. It has numerous issues, the main one of which is that very few formal systems directly include the rule:

A new expression (a proposition) may be entered on a line of a derivation if it is a substitution instance of a previous line of the derivation, or of an axiom of the system.

This is not a rule of common Hilbert-style systems, which have only modus ponens as an inference rule, nor a rule of sequent/tableau systems, nor a rule of natural deduction systems. It may be provable as a metatheorem in some systems, but the text here misrepresents things. Similarly, the claim

This is how new lines are introduced in an axiomatic system.

misrepresents things.

A more minor issue is that it doesn't make sense to talk about one variable being a substitution instance of another variable; only for one expression to be a substitution instance of another expression.

I may get time to work on this at some point. — Carl (CBM · talk) 04:32, 15 January 2008 (UTC)

Perhaps adding the word "some" so that it says "some axiomatic systems." would suffice?

It does make sense to talk about the expression represented by the metalinguistic variable being a substitution instance of the expression represented by another. That is what a metalinguistic variable is. That may need to be clarified better, but that won't take much. Pontiff Greg Bard (talk) 04:44, 15 January 2008 (UTC)

If a metalinguistic variable is a variable, then it can't be a substitution instance of another variable. The formulas can be substitution instances of other formulas, however. This is like saying, Φ - which is wrong. What's true is that if n is an integer variable, the value of n is even if that value is divisible by two. It's a type error to confuse the two.

As for the axiomatic systems, after thought I believe the real issue is that substitution instances only make sense for propositional logic, not for arbitrary axiomatic systems. I don't even know that there is a sensible definition of a "substitution instance" of a first order formula. — Carl (CBM · talk) 15:18, 16 January 2008 (UTC)

A metalinguistic variable is treated as if it is metalanguage talking about object language. The phrase 'Φ' is the name of the formula Φ. The formula that 'Φ' stands for is Φ. This is exactly how examples like the one you give are dealt with so as to be clear. Please read Use-mention distinction. I think you can imagine 'Φ' standing for the formula (A=A) like the example, and 'Ψ' standing for (A=A)=(A=A). Clearly Ψ is a substitution instance of Φ. It's not 'Ψ' that is a substitution instance of 'Φ'. Be well, Pontiff Greg Bard (talk) 16:41, 17 January 2008 (UTC)

Strike that. You have an example from math where you have a variable and a value for it. I am talking about a metalinguistic variable which is a part of the metalanguage. Your n is a part of the object language that you jump into to deal with math. By and large, I am guessing that you skirt the use-mention issue when you write about math, etc. However, there are areas where it needs to be clear. There are also times in the text when it will be clear without the use of quotes so it is not used:

"→ stands for implication"

If you understand the use-mention distinction YOU know that its really supposed to be:

"'→' stands for implication"

However, we should come to some understanding in standards for notation. We should either use it, or make some statement that we will be skirting the issue at times.

Pontiff Greg Bard (talk) 17:00, 17 January 2008 (UTC)

Right - the use of quotes as a sort of semantic standin for use/mention is not common in the fields (like mathematics) where substitution instances would be considered. Rather, what would be common is to simply say "Let Φ and Ψ be formulas"; there is no need to refer to the variables themselves. However, once you have referred to them as variables, rather than formulas, you are bound to treat them as variables, not formulas for the rest of the sentence.

You seem to be proposing that sentences like this make sense:

If 'F' is a metavariable ranging over cities then F has a population.

The ordinary, simple, clear way of saying that is simply, "If F is a city, F has a population." — Carl (CBM · talk) 17:05, 17 January 2008 (UTC)

You may be comparing this with sentences like

If 'Chicago' is the name of a city then Chicago has a population.

That is of course fine. The issue is with

If 'Chicago' is a variable ranging over cities, then Chicago has a population.

which I find somewhat different. — Carl (CBM · talk) 17:32, 17 January 2008 (UTC)

The use of metalinguistic variables is a different issue than the issue of using notation for the use-mention distinction. The thing to understand is that Φ is part of the metalanguage (see? its right here in this sentence that way). It is not a formula of the formal language you are talking about. It's just like the English we are using.

Say listen, I see you have just changed it back. You have made it false again. Pontiff Greg Bard (talk) 17:44, 17 January 2008 (UTC)

If we are going to have it your way, then the removal of the single quotes from the first one makes it correct (as I have just done). You see that we can avoid all of that cluttered language by leaving them in however. Pontiff Greg Bard (talk) 17:47, 17 January 2008 (UTC)

It is quite fascinating to see the muddled mess that proper use of use-mention distinction and metalinguistic variables avoid. My goodness. Carl please look into it further. Be well, Pontiff Greg Bard (talk) 17:55, 17 January 2008 (UTC)

Somehow, the math community manages to do abstract algebra and mathematical analysis, full of variables, without needing to worry about use vs. mention. This is because there is really little benefit to saying "Let 'n' be a metavariable ranging over natural numbers" vs. "Let n be a natural number." I just looked up substitution of propositional formulas in Kleene (1967) and Enderton (2001). Neither author felt it necessary to distinguish use and mention. Both said things like "If φ is a formula". Can you explain why you think that the issue of metavariable vs. variable is important to the reader's understanding of the concept of substitution instances? — Carl (CBM · talk) 18:01, 17 January 2008 (UTC)

Carl, it always seems to me that the math community is always very narrow about the way they do things. People understand things differently than each other. The average person isn't going to get into Kleene or Enderton OR COME CLOSE. The use of quotes for use-mention distinction enables us to make a rigorous distinction and is reachable to the average person. I am absolutley astonished at what I go through on this Wikipedia. I think a lot of this material is reachabe to the average person, but certainly not if mathematicians write it. I'm sorry Carl, but this is ridiculous. These articles aren't for the math community they are for a general audience. Pontiff Greg Bard (talk) 18:13, 17 January 2008 (UTC)

There's no need for polemics. I think a general audience is much more likely to have seen elementary algebra problems that say things like "Suppose Farmer Joe has x bushels of wheat." than problems that say "Suppose that 'x' is a metavariable ranging over bushels of wheat, so that Farmer Joe has x bushels." What I am asking is how the use/mention distinction at all clarifies what is going on with this particular concept, substitution instances. I don't see that it does; can you explain its relevance? If a reader doesn't already realize that the variables could be considered metavariables, how does it help them to point it out in a simple situation such as this? — Carl (CBM · talk) 19:59, 17 January 2008 (UTC)

Use v mention notation

Greathouse. Thanks for your attention to this article. However, you have just turned those sentences false. Please see Use-mention distinction. The use of single quotes indicates that it is a mention. The absence of them indicates a use. Therefore your clarification actually kinda of screws things up. It was correct as it was. There is a much bigger format issue here that we should get straight in Wikipedia:WikiProject Logic/Standards for notation Pontiff Greg Bard (talk) 15:58, 17 January 2008 (UTC)

P.S. Just to be open-minded, we could just leave in your wording, and use single quotes around those metalinguistic variables everytime. However that defeats the purpose. They are supposed to stand for (and be understood as) phrases of the metalanguage. Without the quotes they are being used in an object language. This is an important distinction, and should be checked throughout the all the logic (and math perhaps) articles. Be well, Pontiff Greg Bard (talk) 16:03, 17 January 2008 (UTC)

revert

I have reverted it back to the last version I know is correct. All the tinkering with the quotes and variables have made a big mess. Please. This is correct. Please look into use mention thoroughly. Pontiff Greg Bard (talk) 18:02, 17 January 2008 (UTC)

Edits

I expanded the article some. Substitution instances are considered in the context of propositional logic (they don't make sense for arbitrary first order formulas, nor formulas of arbitrary formal systems). I added a couple references and the relationship between tautologies and substitution instances.

I still don't see the need to use the term "metalinguistic variable", and unless a good justification can be presented I think that sentence can be rephrased more succinctly. — Carl (CBM · talk) 14:24, 19 January 2008 (UTC)