On 14 Jan 2014, at 21:39, LizR wrote:

On 14 January 2014 23:01, Bruno Marchal <marc...@ulb.ac.be> wrote:

Physicists have not yet formal theory. Like all scientists they work informally.

You don't consider Newton's "Law of Gravitation" to be a formal theory?


No, but I understand what you mean by that. So I was agreeing with your remark on Edgar's post.



How much more formal can you get than defining space and time and mass and force then relating them all with


?

By given explicitly the alphabet, the grammar, the axioms, and the rule of inference.

Nobody does that, except when we programmed a computer or build a machine. The relation above is an informal description of a relation between measurable quantities. It is not a formal theory in the sense of the logicians.

Nobody work in formal theories, except quite exceptionally Russell and Whitehead, in Principia Mathematica. Gödel did not have to read it at all, to refute their project of formalization of the whole of math (Hilbert's "nightmare").

Logicians does not work in formal theories (unless you look at them at the comp substitution level assuming they are machines: that would be formal, but of course that is out of the question). Logicians formalize theories, to reason *on* them, not *in* them. But their proofs on the formal systems are done informally, like all proofs in math.





I'm guessing you mean something different by a "formal theory" to what I would understand by that phrase.

I am aware that only professional logicians make that difference, which is indeed crucial for the logical matter.




When I ask Edgar for a formal theory I'd be delighted to get something like Newton's law of gravitation rather than a load of hand waving verbiage.

Sure, me too. Do you understand the nuance I brought? That is crucial to just understand what the field of mathematical logic is all about. It simple: to be formal = to build a machine (virtual or real) which can answer the questions. To formalize newton, you will need to give the alphabet (the symbols you allow). This will include the logical connectors, for example, and the "=" symbol, and the quantifiers. You will need a grammar telling you which formula are well-formed. Then you have to give all the axiom you need, like the one I gave for propositional calculus ( like (A->(B->A)), (A->(B->C)) -> ((A-> B) -> (A->C)) etc. (you remember? I asked to prove (A->A) from them, on the FOAR list, I think). You will need to give the math axioms, presented in that way. The inference rules (without which you can just do nothing with the axioms). Like the rule that you can derive B from A->B and A.
Etc.

There is no formal proofs in the literature, except in figures, to illustrate what the meta-mathematicians (mathematical logicians) works on.

Now, you can consider the RNA transcription from DNA, and the synthesis of a protein as a formal thing, and in that sense, the basic reality is quite formal. But science is and will ever be informal, even logic. Gödel's incompleteness proof is informal, but it applies *on* the existence or non existence of formal proofs in formal theories.

Now, all mathematicians are comforted by their (usually correct) beliefs that their proofs could easily been formalized in ZF, but they never do that, for good reason. Formal proofs are long, tedious to read, non intelligible and full of bugs, like programs and machines.

Bruno


http://iridia.ulb.ac.be/~marchal/



--
You received this message because you are subscribed to the Google Groups 
"Everything List" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to everything-list+unsubscr...@googlegroups.com.
To post to this group, send email to everything-list@googlegroups.com.
Visit this group at http://groups.google.com/group/everything-list.
For more options, visit https://groups.google.com/groups/opt_out.

Reply via email to