On 14 Jan 2014, at 21:39, LizR wrote:
On 14 January 2014 23:01, Bruno Marchal <[email protected]> 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 [email protected].
To post to this group, send email to [email protected].
Visit this group at http://groups.google.com/group/everything-list.
For more options, visit https://groups.google.com/groups/opt_out.
