This article is within the scope of WikiProject Mathematics, a collaborative effort to improve the coverage of
mathematics on Wikipedia. If you would like to participate, please visit the project page, where you can join
the discussion and see a list of open tasks.MathematicsWikipedia:WikiProject MathematicsTemplate:WikiProject Mathematicsmathematics articles
This article is within the scope of WikiProject Philosophy, a collaborative effort to improve the coverage of content related to
philosophy on Wikipedia. If you would like to support the project, please visit the project page, where you can get more details on how you can help, and where you can join the general discussion about philosophy content on Wikipedia.PhilosophyWikipedia:WikiProject PhilosophyTemplate:WikiProject PhilosophyPhilosophy articles
Hey, I removed the statement "For any consistent formal system, any substitution of a tautology will also produce a tautology." earlier from this page but my edit was reverted and now the statement is back. The reason for the edit is because it's not true - it holds only for systems closed under substitution. The Logic of Public Announcements for example is not closed under substitution. [p]p is a tautology of PAL while [φ]φ is not. I don't want to start an edit/reverse war so I'm keeping the page as it is and ask someone else to remove the statement or clarify it.
You're right. It should say "closed under substitution" instead of "consistent". That paragraph is also a bit confused about whether it wants to talk about propositional logic or arbitrary formal systems. In the latter case the statement could be generalized further to substitution preserving other relations, not just tautologies. —Ruud17:05, 11 August 2012 (UTC)reply
The sentence was not merely "in need of clarification", but as the anonymous editor pointed out here and in his edit summary, factually incorrect. So, conversely, it would probably also be a good idea to correct the statement instead of reverting the removal without comment. The whole article is in a pretty sorrow state, I'll put it on my to so list. —Ruud01:14, 14 August 2012 (UTC)reply
Justification for editing the lead
Here are my justifications for my editing of the lead (in blockquote: old text, sentence by sentence):
I replaced "strings" by "expressions", since I consider a tree structure as the best way to represent a formula, in predicate logic as well as in propositional, or other logics.
In
propositional logic, a substitution instance of a
propositional formula is a second formula obtained by replacing symbols of the original formula by other formulas.
I deleted this sentence, which is now redundant.
For any
formal system that is closed under substitution, any substitution of a
tautology will also produce a tautology.
This sentence seems important; I'd like to keep it. However, I don't understand:
Is this a definition of "closure under subtitution" or a theorem about propositional logic and related systems? In the former case, a phrase like "... is called closed under substitution if ..." would be more clear. In the second case, a citation should be added (who has proven precisely which theorem where?).
What does "substitution" mean anyway in an arbitrary formal system? Although the article "
formal system" uses the notion of "formal system" in a rather narrow way, (i.e. consisting of alphabet, formulas, axioms, inference rules, thus excluding e.g. formal systems operating on values rather than on truths, such as term rewriting systems), it does not require the notion of variables and/or substitutions for something to be a formal system. - It doesn't even mention the notion of "tautology", but that could probably repaired (def.d as "inferred from axioms by rules").
On the whole I don't object to this contribution, however I have no choice but to say that it will be extremely confusing to most readers. Perhaps the more simplified explanation as it relates to propositional logic needs to come first. Also, you should know that not everything in Wikipedia is a concept. That actually is a meaningful distinction, because it tells the readers and editors what the subject matter of the article is. Please observe the "concepts in logic" category. You can reasonably expect any article in that category tree to mention the fact the the article is about the
concept (i.e. not about, for instance, the typographical symbols, etcetera.) In this case, not only is substitution a concept (which there are many), but it is one of the most fundamental concepts in logic. I do agree about "expression" over "string", and that is also consistent with the usage of terminology in the category structure (i.e. there is a category for "logical expressions", not "strings"). I also hope the statement about closure, and substitution within tautologies resulting in tautologies reappears. Good luck.
Greg Bard (
talk)
22:36, 16 June 2013 (UTC)reply
I agree to your suggestion of swapping the sections about propositonal and first-order logic, and edited the article accordingly.
Although I don't yet fully understand the meaning of the "conept" notion, I restored the respective lead sentence, being impressed by the existence of a category about logical concepts. (Concerning typographical symbols as non-concepts, I'd disagree, referring to Hofstadter's work about analogical reasoning in font design, cf. Ch.10 in D. Hofstadter, The Fluid Analogies Research Group (1995). Fluid Concepts and Creative Analogies. Basic Books., or Gary McGraw, Douglas R. Hofstadter.
"Emergent Letter Perception: Implementing the Role Hypothesis". {{
cite journal}}: Cite journal requires |journal= (
help); but maybe e.g.
Marilyn Monroe is not a concept.)
Concerning the statement about closure, I'd like to wait for a clarification, unless you insist on restoring it immediately. Its instance concerning propositional logic (which seems well understandable to me) is still contained in the respective section, anyway.
Jochen Burghardt (
talk)
07:15, 17 June 2013 (UTC)reply
You and I agree about typographical symbols. They are marks on the page, and they are ideas too. When logicians talk about symbols, and expressions, they are always talking about the ideas, unless they specifically say so. However, there are articles that deal with typographical symbols, and they talk about the history of the marks on the page. We are talking about metalogical distinctions, and want to make sure that the classification of things is clear. I am not an immediatist, so at some point in the future I', sure we will get a clarification on closure that is satisfactory. Carry on, and be well.
Greg Bard (
talk)
17:46, 17 June 2013 (UTC)reply
Refactoring of sections?
During work on the "first-order logic" section, I got the impression that the section headings do not reflect the contents distinction in the best way.
The section currently called "Propositional logic" explains the use of substitutions in propositional logic.
It even briefly explains (in the paragraph before "Tautologies") the use in first-order logic, which a reader wouldn't expect there, as long as an own section seems to be devoted to "First-order logic".
On the other hand, the section currently called "First-order logic" explains the mechanism of substitution and many algebraic properties needed for unification, resolution proving, term rewriting etc. If we are willing to accept propositional formulas as terms over the operators (or better: as meta-terms, in order not to confuse the notions of "term" and "formula"), e.g. the 1st example substitution from section "propositional logic" can be described by , using the notation from the "First-order logic" section.
To start a discussion, I suggest to refactor the article to have the following sections:
"Use in propositional logic" (to keep the most easily readable section first, as suggested by
User:Gregbard)
"Use in first-order logic" (to be composed from the first-order paragraph currently under "Propositional logic", and explanations of the -elim and -intro rule of natural deduction, we also should think about a first-order property corresponding to the one explained under "Tautologies", maybe implies if and ?)
"Formal definition" (essentially the contents of the current "First-order logic" section, extended as needed in the new "Use in propositional logic" section (meta-terms? etc.)
The following discussion is closed. Please do not modify it. Subsequent comments should be made in a new section.A summary of the conclusions reached follows.
My impression of proper Wikipedia math articles is that both informal and formal descriptions of the same concept can fit in the same article, starting with the informal description in the (Top) section. Is this a correct judgement?
HyenHks (
talk)
10:19, 13 March 2023 (UTC)reply
The discussion above is closed. Please do not modify it. Subsequent comments should be made on the appropriate discussion page. No further edits should be made to this discussion.
Typo and possible wrong order of examples?
{ x ↦ y2, y ↦ y2 } is flat, but non-linear, { x ↦ x1, y ↦ y2 } is both linear and flat, but not a renaming, since is maps both y and y2 to y2; each of these substitutions has the set {x,y} as its
The "is" should indeed be "it", thanks for noticing. Both substitutions map y to y2 (given explicitly in the braces), and y2 to y2 (since every variable outside the domain is mapped to itself). -
Jochen Burghardt (
talk)
09:29, 26 October 2023 (UTC)reply
False claim about idempotence
The article makes the claim "The substitution { x1 ↦ t1, …, xk ↦ tk } is idempotent if and only if none of the variables xi occurs in any ti."
However, the identity substitution seems to be a counterexample. I suppose it is true if x ↦ x mappings are not allowed in the substitution, but that does not appear to be made clear in the article.
MattWithTwoTees (
talk)
09:15, 4 June 2024 (UTC)reply
You are right, x↦x mappings indeed are not allowed by the cited authors. I changed the previous fix accordingly. Moreover, it should be "none of the variables xi occurs in any tj" (now fixed, too). -
Jochen Burghardt (
talk)
17:48, 5 June 2024 (UTC)reply