Talk:Formal system

From Wikipedia, the free encyclopedia

This article is within the scope of the following WikiProjects:

Contents

[edit] An image

I have an image I've made that I hope someone can make use of:

[[1]]

I've placed it into the public domain.

-- Lion Kimbro

I've made several attempts to down load it. Times out every time. Mind letting us in on what it is a picture of? Nahaj 00:40:44, 2005-09-08 (UTC)


"It is not assumed that the metalanguage in which proofs are studied is itself less informal than the usual habits of mathematicians suggest."

Sorry? What does this mean?
I think you could rewrite it as "It is assumed that the metalanguage in which proofs are studied is itself at most as formal as the usual habits of mathematicians suggest." But it's not clear who assumes this or why this can be assumed. So I've removed the sentence. -- Felix Wiemann 15:35, 16 August 2006 (UTC)

[edit] Formalism vs finitism

Theorems are then recognized as the possible 'last lines' of formal proofs. That's OK, but I am not sure I catch the following phrase: The point of view that this sums up all there is to mathematics is often called formalism, but is more properly referred to finitism.

In my opinion formalism in mathematics is (very roughly) intended to mean that proof means proof (at least in principle) formalizable inside a formal system. This has to do with formal systems. It has really little to do with finitism, which (roughly) is a philosophy of exixtence not of proof. Of course, the question is somewhat vague, since the terms formalism, finitism in this sense are somewhat vague (and, moreover, formalism is sometimes interpreted in the sense that existence means just a proof for existence). However I believe that, according to the conventional sense of the terms presently in use, the phrase is to be considered false, and that this point of view should be actually called formalism. —The preceding unsigned comment was added by Popopp (talk • contribs) 17:05, 29 April 2007 (UTC).

What you're describing as "formalism" is not, I think, the usual understanding of the word. I would call your version something like "epistemological formalism" (that's a phrase I just made up; please don't add it to articles unless you can find it in the literature somewhere -- which you might, because it seems natural enough).
The notion more usually called "formalism" is what might, to make the distinction, be further specified as "ontological formalism". What it says is that the objects of discourse of mathematics -- functions, real numbers, perhaps even natural numbers for the purest formalists -- do not "really exist", do not have an ontological status independent of the theories that purportedly describe them. For formalists, an assertion that makes reference to mathematical objects is to be interpreted as saying that the assertion can be proved in some understood formal system. This distinguishes them both from realists/Platonists, who interpret the assertion as making a claim about some real things (whether the assertion can be proved in a fixed system or not) and from intuitionists and finitists, who consider assertions not meeting certain rigid conditions to be simply meaningless altogether.
Finitism is again an ontological rather than epistemological position. It accepts certain things as real, and not others. Generally finitists accept the natural numbers as real, but not the completed totality of all natural numbers. Especially strict finitists may not accept even all the natural numbers as real -- for example they may consider that 10^{10^{10}} has no real existence, and is to be treated, if at all, only from a formalist standpoint. --Trovatore 06:50, 8 August 2007 (UTC)

[edit] Merger of "Axiomatic system" and "Formal system"

I suggest a merger of these two pages. I recognize a formal system as a special case of an axiomatic system. There can be axiomatic systems in political philosophy or ethics (I got this from the commentary Axiomatic system#Axiomatic method) which are not in a strict formal alphabet nor use a formal logic as means to get theorems. The section Axiomatic system#Properties such very much an appropriate description of mathematical formal systems and so the merger will make this link clearer. The commentaries Axiomatic system#Axiomatic method and Formal system#Formal proofs can also be tightened up and expanded with such a merger.

Also note that I'm suggesting a merger of Axiomatization into Axiomatic system, so perhaps these two issues should be considered together. --DesolateReality 04:44, 22 July 2007 (UTC)

I designed the article formal in the Dutch Wikipedia nl:Formeel, and it seems to me that it's just the opposite as you recognize: an axiomatic system is a special case of a formal system.
In priciple a formal system can be anything based on formal or deductive principles. For example [2]: In logic a formal system is a formal language together with a deductive apparatus by which some well-formed formulas can be derived from others
It seems to me that this article is incomplete. It only refers to the meaning the term "formal system" has in mathematics. It seems to me that the other field should also be included in this article. - Mdd 12:37, 30 July 2007 (UTC)
I agree this article is incomplete. From what i see, there is no difference between a formal system and an axiomatic system. both use inference rules to deduce theorems from axioms. Can Mdd give me a distinction between these two? Also, what does Mdd think of the merger? if there is no significant distinction between these two, we might as well combine the articles. --DesolateReality 07:55, 1 August 2007 (UTC)
The article axiomatic system already states:
  • An axiomatic system that is completely described is a special kind of formal system
Other kind of formal systems are Proof calculus, Formal ethics, Logical system, Lambda calculus, Propositional calculus
The difference between a formal system and an axiomatic system is that:
  • An axiomatic system is any set of axioms.
  • A formal system consists of symbols, grammar, axioms and rules.
  • Formal systems are linked to formal language, formal methods and formal science.
Not all "formal systems" in theory and in real life are axiomatic systems. So merging both articles is not a good idea. - Mdd 18:44, 7 August 2007 (UTC)
Not only are not all formal systems axiomatic, but also not all axiomatic systems are formal. The claim about a "completely described" axiomatic system being a formal system seems to be related to Hilbert's thesis, which is not uncontroversial -- I think that claim ought to be qualified in the "axiomatic system" article. --Trovatore 20:24, 7 August 2007 (UTC)
These articles can be integrated in such a way that no article is deleted completely, but rather that the appropriate material is covered in each. Gregbard 22:28, 7 August 2007 (UTC)
Copied from the Wikipedia talk:WikiProject Logic page:
A formal system isn't necessarily an axiomatic one. The deductive apparatus of a system may consist of either transformation rules (also called rules of inference), axioms, or both. There is no need to do a complete merge in which one article completely disappears. However, the two may be integrated. This usually involves a paragraph that touches on the topic, with a link to the main article using {{main}}. I think if you look at how they organize big city articles with a section on "History of Denver" (for instance), but with a link to a whole article on "History of Denver." Some form of integration might work. Gregbard 21:50, 7 August 2007 (UTC)
There seems to be an understanding that formal systems and axiomatic systems are not the same. Now Gregbard suggests that there are more ways to integrate both articles. My question however remains, why? Merging these two concepts only complicates things. In real life the term "formal system" has much more use and meaning then the term "axiomatic system". But both items seems important enough to have an article of it's own. So why should anyone want to cover all these differences. I prefer to keep things simple. - Mdd 22:58, 7 August 2007 (UTC)

I have removed the merger tag, since there is much consensus that formal systems and axiomatic systems are distinct. --DesolateReality 05:34, 8 August 2007 (UTC)

Thanks for closing this discussion (disussions like this often just keep going on). It would be nice if some aspects of this discussion would be implemented in this article itselve. - Mdd 11:49, 8 August 2007 (UTC)

[edit] Attention from an expert on the subject

I do think this article needs an expert that improves the introduction of this article. This introduction should make more clear that the term formal systems is alos a general term used in logic, mathematics, computer science and linguistics, etc. and in what meanings - Mdd 23:39, 7 August 2007 (UTC)

Another improvement to this article can be made if instead of the current list of examples of formal systems, a written section will be dedicated to examples of formal systems? - Mdd 11:49, 8 August 2007 (UTC)

[edit] WikiProject class rating

This article was automatically assessed because at least one WikiProject had rated the article as start, and the rating on other projects was brought up to start class. BetacommandBot 04:00, 10 November 2007 (UTC)

[edit] deductive apparatus

We need more sources for the use of the term in this context. I can produce 4 or 5 sources, both before and after Hunter, which do not use it. If Hunter is the only source, it's a WP:NEO, even if over 35 years old. (What's the term for a term which was coined quite a while ago, but never caught on except in a small community including a certain editor who likes to coin terms.) — Arthur Rubin | (talk) 00:55, 18 January 2008 (UTC)

Gee Arthur, there are infinity sources that don't use all kinds of terminology. I can't believe you make so much trouble for me, and then we get rhetoric on the talk page. The Hunter source uses it, so get used to it. You are intolerant to terminology you are not already familiar with. Please entertain the possibility that you don't have every perspective on things. This term is specifically for both the axioms and any transformation rules. What would YOU call that. Since there is this term, and it is more general it should go in. Furthermore it should go in NONCONTROVERSIALLY. You are a trouble maker plain and simple Arthur. Stop it. Pontiff Greg Bard (talk) 01:11, 18 January 2008 (UTC)
Google turns up 75,000 hits. Seriously Arthur Stop Being a Trouble Maker.

Okay, its' 1100 hits for "deductive apparatus", but still. Pontiff Greg Bard (talk) 01:14, 18 January 2008 (UTC)

I found some other usages in respectable sources, even if not reliable. It should go in, but as a secondary term, as everyone knows what "axioms" and "rules of inference" are. As for google:
"deductive apparatus" 1170
"rules of inference" 68700
"rules of inference" axiom 36100
— Arthur Rubin | (talk) 01:17, 18 January 2008 (UTC)
Perhaps this revision will be acceptable. — Arthur Rubin | (talk) 01:24, 18 January 2008 (UTC)
"Deductive apparatus" is not the same thing as "rules of inference." "Deductive apparatus" is not the same thing as "axioms." The "deductive apparatus" refers to the whole system used whether it is axioms, rules of inference, or both. Again I ask what term you use for that. The revision as you have proposed is incorrect.
"...consists of a formal language and a set of inference rules, used to derive..."
Only it doesn't necessarily have to have "a set of inference rules" at all DOES IT? You can just use axioms alone. So this wording IS better. You're proposal is clearly worse. It makes a good clarification. Pontiff Greg Bard (talk) 01:57, 18 January 2008 (UTC)
But "axioms" ("postulates", etc.) and/or "rules of inference" or "inference rules" are what are actually used in the bulk of the literature. What we should have is a clarification of what used to be there, and then an additional sentence that the system as a whole is called the "deductive apparatus". You may work on the last part, but I must insist that "deductive apparatus" be secondary, per WP:UNDUE. — Arthur Rubin | (talk) 02:00, 18 January 2008 (UTC)


I don't know what you mean by secondary, since its in the lede. Everything looks all right content wise as far as I'm concerned. However, Arthur, you having been stemming so hard on my edits that you have not seen fit to work on the real problem with this paragraph. All those parentheses are terrible form. Leave me alone Arthur. Pontiff Greg Bard (talk) 02:07, 18 January 2008 (UTC)
I'm looking at it again and I'm just going to put it back to the way it was originally. The deductive apparatus is not secondary at all. It is what turns a formal language into a formal system. That's sine-qua-non Arthur. Stop being a trouble maker. Pontiff Greg Bard (talk) 02:13, 18 January 2008 (UTC)
The term deductive apparatus is not commonly used. If it appears in the lead at all, it should be defined within this article before use. I think this falls under the "principle of least surprise.".
Alternatively, deductive apparatus should be merged into this article, in which case it would make marginal sense to include in the lead. — Arthur Rubin | (talk) 02:23, 18 January 2008 (UTC)
I am open-minded to a merge that preserves the material. I just don't see why it would be necessary? I think there is potential for some nice examples, etc. in an article on its own. I think apart from how familiar and comfortable the phrase is to you... the concept itself is of note. The article is an opportunity to elucidate on some other topics as well. Don't merge anything yet please. Pontiff Greg Bard (talk) 03:51, 18 January 2008 (UTC)
On further consideration, the more appropriate move would be to merge deductive apparatus with Formal grammar, and reword the first line: "In formal logic, a formal system (also called a logical calculus) consists of a formal language and a formal grammar (also called a deductive apparatus). The formal grammar may consist of a set of inference rules or a set of axioms, or have both." Only I'm not sure this is how you use the term formal grammar. They seem to be the same concept. However deductive apparatus seems more precisely correct for this article quite frankly. The deductive apparatus is a sine-qua-non for the formal system. It is the one thing that both the axioms and transformation rules participate in, so it helps make clear what their role is. So, you will have to explain the need to de-emphasize it. If you are not familiar with the term, that has no bearing on its appropriateness. The meaning of the concept itself tells us how significant it is. As the article stands now, Arthur has removed, with his rewording, the idea that a deductive apparatus consists only of the axioms and transformation rules and no other things. He has also made the wording aesthetically lame by setting it off in its own sentence, as if it is an aside. I'm pretty sure that is the effect he was going for. Formal language + deductive apparatus = formal system. Formal system - deductive apparatus = Formal language. You really are denying the reader a chance to understand the concept in favor of fulfilling some rigid view. It would really seem to be a key concept here. Perhaps some material from articles axiom and rules of inference should be merged into deductive apparatus instead. Does anyone think the fact that it is a metalogical (or at least logical) concept has anything to do with the desire to de-emphasize it? That would be more evidence of my thesis that Wikipedia articles are math-centric to the detriment of the logic aspects of them. Pontiff Greg Bard (talk) 23:13, 19 January 2008 (UTC)
Your argument only applies to Wikipedia if deductive aparatus is commonly used in the appropriate field, which is mathematical logic, even if it were the best term. (I also don't see how a system with only axioms, and not inference rules, because a formal system. It's a theory (mathematical logic).) — Arthur Rubin | (talk) 23:43, 19 January 2008 (UTC)
So you are making sure the Wikipedia is the lowest common denominator. Gee, thanks for attention to that. Yeah we shouldn't go beyond the common in any article, huh, Arthur? I guess we don't need to look beyond that. It looks like you think that your perspective and the perspective of mathematicians are the only ones that matter. You really should learn to work interdisciplianarily rather than always restrict the subject matter to certain areas you feel comfortable with. That's being a fundamentalist, which is terrible.
Say listen, um, here's a question for you. As a mathematician, what do you think about the fact that a "A formal system is a formal language with a deductive apparatus." I mean what does that mean to you?
In an attempt to respond to the last garbled note, I do not remember off hand exactly, how a formal language with just axioms and no rule of transformation gets off the ground. However, I believe it may have something to do with another article whose guts you probably also can't stand: substitution instance. Pontiff Greg Bard (talk) 00:16, 20 January 2008 (UTC)
In Wikipedia articles on some topic we should use terminology that is commonly accepted and commonly understood in the area to which the topic pertains, and avoid neologisms. Using commonly accepted terminology is not the same as reducing things to the lowest common denominator. While "deductive apparatus" is not exactly a neologism, it is sufficiently rarely used that its meaning may need to be explained even to accomplished students of formal systems, simply because they may never have encountered the term. Is there any handbook of logic using that term?  --Lambiam 02:54, 20 January 2008 (UTC)
As for "A formal system is a formal language with a deductive apparatus", it looks like defining "formal system" in terms of the previously defined terms "formal language" and "deductive apparatus". None the terms make much sense in "natural language". — Arthur Rubin | (talk) 18:23, 20 January 2008 (UTC)
Traditionally axioms and inference rules are usually mentioned separately for historical reasons, but an axiom schema is essentially a special case of an inference rule, namely one with zero premises. This is touched upon in the article Rule of inference: "If the premise set is empty, then the conclusion is said to be a theorem or axiom of the logic."  --Lambiam 09:35, 18 January 2008 (UTC)

[edit] What is a logical system?

Does The Cambridge Dictionary of Philosophy give a definition of the notions logical system, logistic system, and simply logic? There is an apparent contradiction between the lede:

  • logical system (or logic) = formal system

and the subsection "Logical system":

  • logical system (or logic) = formal system + semantics.

 --Lambiam 23:31, 6 May 2008 (UTC)

It looks like we have discovered that some use different terminology. We should make it clear that some apparently use that term for different things. The one under the logical system section needs a source, perhaps it is an error. Pontiff Greg Bard (talk) 00:55, 7 May 2008 (UTC)
Does The Cambridge Dictionary of Philosophy give a definition of these notions?  --Lambiam 18:19, 8 May 2008 (UTC)
The CDoP has entries are follows:
  • No entry at all for "formal system"
  • Under "logical system" it says see Formal semantics, Logistic system.
  • Under "logistic system" there is an entry describing a formal language together with a deductive apparatus. It also says in the entry that this is "what many today would call a "logic."
I find the term "logistic system" archaic myself, but whatever.
Perhaps the section titled logical system can be corrected by replacing formal system with formal language, or the entire section can be deleted... as long as the whole thing about interpretations, soundness and completeness is elsewhere covered. Be well, Pontiff Greg Bard (talk) 19:45, 8 May 2008 (UTC)
I got rid of that section..., changed the order of the related subjects. I think this reflects the order of increasing complexity, one being based on concepts from the previous. I also created the section on interpretations. I hope this kind of helps to frame things. Pontiff Greg Bard (talk) 20:08, 8 May 2008 (UTC)

The way in which the term "logic" (as a count noun) is actually used by logicians, it usually includes a semantics for the formal language. Just check the many articles about particular kinds of logics on Wikipedia: most have a section "Semantics" on the same footing as the section "Syntax". Statements such as that Gödel proved that first-order logic is complete, which can be found everywhere, are meaningless unless the logic has a semantics. Our article Soundness also presupposes that a logical system has a semantics. This is not surprising; a logic without a semantics is utterly useless: what good does it do to anyone to learn that the uninterpretable sequence of symbols "*^^^^^^^^^(^" is a theorem, but "*^^^^^^^^(^^" is not?  --Lambiam 10:58, 9 May 2008 (UTC)

[edit] x02111

What Unicode symbol is that, and why should it be used in the article? — Arthur Rubin (talk) 22:21, 21 May 2008 (UTC)

I agree there's no need for it; TeX can be used if there is a real need for it, and TeX math is much more accessible. — Carl (CBM · talk) 22:23, 21 May 2008 (UTC)
I'm sorry Arthur, it just was the closest thing I could find. Thanks for correcting it. Be well, Pontiff Greg Bard (talk) 04:29, 22 May 2008 (UTC)

[edit] Ordered quadruple

"An interpreted formal system can be defined as the ordered quadruple <α,\mathcal{I},\mathcal{D}d,\mathcal{D}>." Shouldn't it be stated what the components of the quadruple represent, such as ", in which α is an alphabet, ..."? From the remainder of the section I could not deduce what kind of entities the components represent and what constraints exist among them.  --Lambiam 17:15, 23 May 2008 (UTC)

You are correct. I have inserted the definitions. Sorry it took so long. Pontiff Greg Bard (talk) 22:57, 25 May 2008 (UTC)