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 workinformally.You don't consider Newton's "Law of Gravitation" to be a formaltheory?

`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 andmass 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" towhat 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 getsomething like Newton's law of gravitation rather than a load ofhand 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.