4 ms·

I see this annoying mistake everywhere, but it's important to point out in the context of computer science (more so than in mathematics) because it relates to o

by pron 8y ago

I see this annoying mistake everywhere, but it's important to point out in the context of computer science (more so than in mathematics) because it relates to one of its core components: in the context of logic and proofs, "formal" does not mean precise or mathematical (and certainly not official), but rather mechanical. A formal description is one with a precise syntax and semantics, whose truth can (at least in principle) be judged directly from its form. A formal proof is one carried out through pure syntactic (i.e., formal, in the sense of "pertaining to form") manipulation, and does not rely on any informal arguments, namely ones that do not appear in the form. As a rule of thumb, if you could replace the word "formal" with "mechanical" and your sentence would still be true, then you can use the word formal (this is the case, say, with formal software verification, which is simply mechanical software verification, or formal proofs in a proof assistant, that are mechanical proofs). So, a formal description is one that could be directly mechanically interpreted by a simple computer program as written, and a formal proof is one that could be mechanically checked. If this is not the case -- use the word "precise" (or "mathematical" if you prefer). It's both simpler and more accurate. As the description given here makes heavy use of natural language that is not easily interpretable by a computer, it is not formal, and since the proof makes use of a notion of a time machine, as well as others, not given a formal definition, it is very much informal, even if sufficiently precise to be acceptable as a mathematical proof.

mlevental 8y ago
welcome to writing? i don't understand this kind of pedantry: it is very clear from context that is not going to be a formal spec or formal proof and therefore the word formal here is being used informally... or just ya know according to its conventional understanding. did you really get to the end of article before you realized this wasn't going to be about formal proofs/specs?
- tofof 8y ago
  Did you really get to the end of the first paragraph before you decided this wasn't going to be about formal proofs/specs? "It will then formalize the Two Generals' Problem and formally prove the impossibility."
  - mlevental 8y ago
    >Did you really get to the end of the first paragraph before you decided this wasn't going to be about formal proofs/specs? yes because i have heard of the word juxtaposition >This guide will introduce the Two Generals' Problem and give an [INTUITIVE] explanation for why finding a solution to the problem is impossible. It will then formalize the Two Generals' Problem and formally prove the impossibility.
- pron 8y ago
  It's like writing "pusillanimous" when you want to say "nice" -- the chosen word is both unnecessarily fancy and wrong. I'm not aware that this has become the conventional understanding just because some people here and there make this mistake. It's fine for words to acquire new meaning, sometimes even an opposite one like in the case of "literally," but even in that case the word serves some purpose (that of emphasis). So if you tell me that the word "formal" has acquired the meaning informal, I would still ask what purpose does "formal" serve here? What's wrong with just saying proof? And yes, I did need to scroll to the section about the proof to see that the article does not, in fact, provide a formal proof. I agree that this is pedantry, but in this case the article emphasizes formalization so much that it seems like it's a central point, and yet no formalization is to be found. To me this suggests that some people may simply not know what "formal" means in this context, which is fine, but since this is an important concept in computer science, I thought it is worth pointing out.
smallnamespace 8y ago
The meaning of 'formal' really depends on the context and is a matter of degree. This is readily apparent from your identification of formal with mechanical. That immediately forces the question: which machine? > a formal description is one that could be directly mechanically interpreted by a simple computer program as written Outside of automated theorem proving and checking, very little done in math or theoretical CS actually meets the definition you gave for 'formal'. E.g. the proof of FLT is clearly not 'formal', it has not been reduced to steps that are all machine-checkable. The proof of, say, the Halting Problem as is normally given is also not formal. If you relax your definition of 'machine' to include 'humans with mathematical context following a sequence of steps', then most proofs can be 'formal', depending on how much context the proof assumes of the reader. Anyway, I think the distinction you make is useful to think about, but in this context (where the audience is mostly non-mathematicians, of which CS theorists are a variety), the better definition of formal is not mechanical, but are we attempting to abstract the problem down into a collection of fixed rules, and it's clear the author has done so. The principle of charity would ask of us to ask, 'Is there another definition of 'formal' that would be reasonable, even if it's not the definition that I am most accustomed to?'
- pron 8y ago
  > The meaning of 'formal' really depends on the context Yes, I say, "in the context of proofs." > That immediately forces the question: which machine? From Aristotle and up until Turing (exclusive) the answer was no machine, but the mechanical application of formal -- i.e., "of form" -- inference rules. That this mechanical process could actually be carried out by a machine was only realized later. Today we know what "mechanical" means, and the word is better understood than "formal" in this context, so it's easier to explain that formal just means mechanical. > Outside of automated theorem proving and checking, very little done in math or theoretical CS actually meets the definition you gave for 'formal'. That's right, but mathematicians know they're working informally. It is true that on occasion you do see a mathematician use the word formal for an informal presentation and proof, but I think that mostly happens because they hear the word from logicians and computer scientists and may not know what it means. Given that the word in this context originated together with the concept of computation, computer scientists should know better. > If you relax your definition of 'machine' to include 'humans with mathematical context following a sequence of steps', then most proofs can be 'formal', depending on how much context the proof assumes of the reader. If the derivations are not done formally then they are not formal even if a human does them. We certainly do hope that most mathematical proofs have formal counterparts, but unless you provide the formal proof, or make the relationship of your proof to a formal one obvious, then you are not providing a formal proof. > the better definition of formal is not mechanical, but are we attempting to abstract the problem down into a collection of fixed rules, and it's clear the author has done so. I don't know if it's better or not, but it is not the one that has been used for centuries. For example, in the book Formal Logic (1847) by Augustus de Morgan, he writes, "This logical truth depends upon the structure of the sentence and not upon the particular matters spoken of." In this particular case, the discussion of time machines in the construction of the proof clearly was not related to the structure (form) of the presentation but on the particular matters spoken-of, hence it is informal. See https://en.wikipedia.org/wiki/Logic#Logical_form https://en.wikipedia.org/wiki/Logic#Logical_form and https://en.wikipedia.org/wiki/Logical_form https://en.wikipedia.org/wiki/Logical_form > 'Is there another definition of 'formal' that would be reasonable, even if it's not the definition that I am most accustomed to?' I don't think it would qualify as a defintion, but clearly some people mean precise or mathematical when they say formal. This mistake is merely annoying and not serious. The reason that's annoying is that the words precise and mathematical are both more accurate and simpler/more familiar.

by pron 8y ago

mlevental 8y ago

welcome to writing? i don't understand this kind of pedantry: it is very clear from context that is not going to be a formal spec or formal proof and therefore the word formal here is being used informally... or just ya know according to its conventional understanding. did you really get to the end of article before you realized this wasn't going to be about formal proofs/specs?

tofof 8y ago
Did you really get to the end of the first paragraph before you decided this wasn't going to be about formal proofs/specs? "It will then formalize the Two Generals' Problem and formally prove the impossibility."
- mlevental 8y ago
  >Did you really get to the end of the first paragraph before you decided this wasn't going to be about formal proofs/specs? yes because i have heard of the word juxtaposition >This guide will introduce the Two Generals' Problem and give an [INTUITIVE] explanation for why finding a solution to the problem is impossible. It will then formalize the Two Generals' Problem and formally prove the impossibility.
pron 8y ago
It's like writing "pusillanimous" when you want to say "nice" -- the chosen word is both unnecessarily fancy and wrong. I'm not aware that this has become the conventional understanding just because some people here and there make this mistake. It's fine for words to acquire new meaning, sometimes even an opposite one like in the case of "literally," but even in that case the word serves some purpose (that of emphasis). So if you tell me that the word "formal" has acquired the meaning informal, I would still ask what purpose does "formal" serve here? What's wrong with just saying proof? And yes, I did need to scroll to the section about the proof to see that the article does not, in fact, provide a formal proof. I agree that this is pedantry, but in this case the article emphasizes formalization so much that it seems like it's a central point, and yet no formalization is to be found. To me this suggests that some people may simply not know what "formal" means in this context, which is fine, but since this is an important concept in computer science, I thought it is worth pointing out.

smallnamespace 8y ago

The meaning of 'formal' really depends on the context and is a matter of degree. This is readily apparent from your identification of formal with mechanical. That immediately forces the question: which machine? > a formal description is one that could be directly mechanically interpreted by a simple computer program as written Outside of automated theorem proving and checking, very little done in math or theoretical CS actually meets the definition you gave for 'formal'. E.g. the proof of FLT is clearly not 'formal', it has not been reduced to steps that are all machine-checkable. The proof of, say, the Halting Problem as is normally given is also not formal. If you relax your definition of 'machine' to include 'humans with mathematical context following a sequence of steps', then most proofs can be 'formal', depending on how much context the proof assumes of the reader. Anyway, I think the distinction you make is useful to think about, but in this context (where the audience is mostly non-mathematicians, of which CS theorists are a variety), the better definition of formal is not mechanical, but are we attempting to abstract the problem down into a collection of fixed rules, and it's clear the author has done so. The principle of charity would ask of us to ask, 'Is there another definition of 'formal' that would be reasonable, even if it's not the definition that I am most accustomed to?'

pron 8y ago
> The meaning of 'formal' really depends on the context Yes, I say, "in the context of proofs." > That immediately forces the question: which machine? From Aristotle and up until Turing (exclusive) the answer was no machine, but the mechanical application of formal -- i.e., "of form" -- inference rules. That this mechanical process could actually be carried out by a machine was only realized later. Today we know what "mechanical" means, and the word is better understood than "formal" in this context, so it's easier to explain that formal just means mechanical. > Outside of automated theorem proving and checking, very little done in math or theoretical CS actually meets the definition you gave for 'formal'. That's right, but mathematicians know they're working informally. It is true that on occasion you do see a mathematician use the word formal for an informal presentation and proof, but I think that mostly happens because they hear the word from logicians and computer scientists and may not know what it means. Given that the word in this context originated together with the concept of computation, computer scientists should know better. > If you relax your definition of 'machine' to include 'humans with mathematical context following a sequence of steps', then most proofs can be 'formal', depending on how much context the proof assumes of the reader. If the derivations are not done formally then they are not formal even if a human does them. We certainly do hope that most mathematical proofs have formal counterparts, but unless you provide the formal proof, or make the relationship of your proof to a formal one obvious, then you are not providing a formal proof. > the better definition of formal is not mechanical, but are we attempting to abstract the problem down into a collection of fixed rules, and it's clear the author has done so. I don't know if it's better or not, but it is not the one that has been used for centuries. For example, in the book Formal Logic (1847) by Augustus de Morgan, he writes, "This logical truth depends upon the structure of the sentence and not upon the particular matters spoken of." In this particular case, the discussion of time machines in the construction of the proof clearly was not related to the structure (form) of the presentation but on the particular matters spoken-of, hence it is informal. See https://en.wikipedia.org/wiki/Logic#Logical_form https://en.wikipedia.org/wiki/Logic#Logical_form and https://en.wikipedia.org/wiki/Logical_form https://en.wikipedia.org/wiki/Logical_form > 'Is there another definition of 'formal' that would be reasonable, even if it's not the definition that I am most accustomed to?' I don't think it would qualify as a defintion, but clearly some people mean precise or mathematical when they say formal. This mistake is merely annoying and not serious. The reason that's annoying is that the words precise and mathematical are both more accurate and simpler/more familiar.