4 ms·

One of these questions I never dared to ask; What does formal mean in the area of mathematics? Is it like finalizing a formula / proof?

by prox 7y ago

kragen 7y ago
I'm not the ideal person to ask, never having published a novel mathematical result and not having particularly deep knowledge of math, but I understand "formal" in this context to mean "mechanical". A formal manipulation of symbols is, as I understand it, one that you can carry out without attaching any meaning to the symbols you are manipulating. This is not the same thing as "rigorous", because it's entirely possible for a formal manipulation to be unsound (with respect to some theory). For example, suppose you want to prove that a left multiplicative identity is also a right identity; that is, ∀x: 1·x = x ⇒ ∀x: x·1 = x. You can apply commutativity and rearrange the symbols to get a proof — that's a purely formal technique, and it's correct and rigorous for, say, complex-number multiplication. But if you're thinking of some other multiplication operations, like that of square matrices of some size, or of quaternions, that's not a rigorous proof, because those multiplication operations aren't commutative. (But in those cases it turns out to be a correct theorem anyway, because they are associative.) Compiling a program is another operation that is formal but rarely rigorous. The hope of using proof assistants in math is that by formalizing our reasoning, we can also make it more rigorous, with the aid of computers and a great deal of cleverness. Most mathematicians are not yet convinced.
- prox 7y ago
  Thanks for sharing your thoughts, so if I get it right, you give me a formula that has been formalized, and I just punch in the right numbers for the variables and get the answer. The less rigorously the arrangement (and proofed) , the more likely the outcome is wrong though the syntax (symbol manipulation) is correct. Hope that sums it up in my understanding :)
- lonelappde 7y ago
  That's not quite right. Rigor means not hand-waving about things that a skeptic might doubt, not skipping corner cases, etc. Formal means doing things like a computer -- strictly symbolic analysis that doesn't claim to do the impossible task accurately map back to our informal ideas of what things mean. Formality is across a chasm -- it's the most accurate kind of math we can do, but it can't be trusted to say that a formal proof about say complex numbers actually applies to what you are thinking about when you day "complex numbers". As is said, "It is impossible to pass from the informal by purely formal means." Here's a better explanation: https://www.quora.com/What-is-difference-between-rigorous-and-formal-mathematics https://www.quora.com/What-is-difference-between-rigorous-an...
  - prox 7y ago
    Thank you, that clears it up further. I recently saw the movie “the man who knew infinity” and so it got me thinking about this meta questions.
  - kragen 7y ago
    This is in accordance with my understanding, but since you seem to think I was saying something different, I think your expression of it is clearer than mine was.
deleted 7y ago
[deleted]
logicchains 7y ago
If you're using a proof assistant, you can't just write something like "X clearly follows from Y" or "Z is left as an exercise to the reader": you have to specify every step, even if they're steps a human reader would easily figure out themselves.
- robinzfc 7y ago
  What logicchains says above is true in some sense but of course it depends on the degree of automation a given theorem proving environment provides. In Isabelle a proof may consist of the keyword "using" followed by a list o 9-10 theorems and it may be accepted if the list is complete (in some sense).
  - logicchains 7y ago
    That's definitely true, but unfortunately I think the set of things "left to the reader" is way larger than the set of things Isabelle can figure out by itself, even with Sledgehammer.
- lonelappde 7y ago
  Of course you can! You can put any axioms (a claim that a conjecture is true is an axiom) you want in a proof assistant. What you cannot do is not say those things but still rely on them in your proof.

One of these questions I never dared to ask; What does formal mean in the area of mathematics? Is it like finalizing a formula / proof?

by prox 7y ago

One of these questions I never dared to ask; What does formal mean in the area of mathematics? Is it like finalizing a formula / proof?

kragen 7y ago

I'm not the ideal person to ask, never having published a novel mathematical result and not having particularly deep knowledge of math, but I understand "formal" in this context to mean "mechanical". A formal manipulation of symbols is, as I understand it, one that you can carry out without attaching any meaning to the symbols you are manipulating. This is not the same thing as "rigorous", because it's entirely possible for a formal manipulation to be unsound (with respect to some theory). For example, suppose you want to prove that a left multiplicative identity is also a right identity; that is, ∀x: 1·x = x ⇒ ∀x: x·1 = x. You can apply commutativity and rearrange the symbols to get a proof — that's a purely formal technique, and it's correct and rigorous for, say, complex-number multiplication. But if you're thinking of some other multiplication operations, like that of square matrices of some size, or of quaternions, that's not a rigorous proof, because those multiplication operations aren't commutative. (But in those cases it turns out to be a correct theorem anyway, because they are associative.) Compiling a program is another operation that is formal but rarely rigorous. The hope of using proof assistants in math is that by formalizing our reasoning, we can also make it more rigorous, with the aid of computers and a great deal of cleverness. Most mathematicians are not yet convinced.

prox 7y ago
Thanks for sharing your thoughts, so if I get it right, you give me a formula that has been formalized, and I just punch in the right numbers for the variables and get the answer. The less rigorously the arrangement (and proofed) , the more likely the outcome is wrong though the syntax (symbol manipulation) is correct. Hope that sums it up in my understanding :)
lonelappde 7y ago
That's not quite right. Rigor means not hand-waving about things that a skeptic might doubt, not skipping corner cases, etc. Formal means doing things like a computer -- strictly symbolic analysis that doesn't claim to do the impossible task accurately map back to our informal ideas of what things mean. Formality is across a chasm -- it's the most accurate kind of math we can do, but it can't be trusted to say that a formal proof about say complex numbers actually applies to what you are thinking about when you day "complex numbers". As is said, "It is impossible to pass from the informal by purely formal means." Here's a better explanation: https://www.quora.com/What-is-difference-between-rigorous-and-formal-mathematics https://www.quora.com/What-is-difference-between-rigorous-an...
- prox 7y ago
  Thank you, that clears it up further. I recently saw the movie “the man who knew infinity” and so it got me thinking about this meta questions.
- kragen 7y ago
  This is in accordance with my understanding, but since you seem to think I was saying something different, I think your expression of it is clearer than mine was.

deleted 7y ago

[deleted]

logicchains 7y ago

If you're using a proof assistant, you can't just write something like "X clearly follows from Y" or "Z is left as an exercise to the reader": you have to specify every step, even if they're steps a human reader would easily figure out themselves.

robinzfc 7y ago
What logicchains says above is true in some sense but of course it depends on the degree of automation a given theorem proving environment provides. In Isabelle a proof may consist of the keyword "using" followed by a list o 9-10 theorems and it may be accepted if the list is complete (in some sense).
- logicchains 7y ago
  That's definitely true, but unfortunately I think the set of things "left to the reader" is way larger than the set of things Isabelle can figure out by itself, even with Sledgehammer.
lonelappde 7y ago
Of course you can! You can put any axioms (a claim that a conjecture is true is an axiom) you want in a proof assistant. What you cannot do is not say those things but still rely on them in your proof.