Alex:  "We need to formalize our scientific theories to use computers to their full potential."   

I agree, but the formalization is ALWAYS context dependent.  The engineering motto is fundamental:

ALL THEORIES ARE WRONG, BUT SOME ARE USEFUL.

That is true about formalization.  It's only precise for subjects that can be expressed  in finite bit strings.  For 99.9% of all the information we get every second of our lives, vagueness is inescapable.  We must deal with it by informal methods of approximations.  Any formal statement is FALSE in general, but it may be useful when the limitations are made explicit.
 
In your note below, you mention computer models.  But any model for a digital computer has already assumed a mapping to bit strings. But an engineering model must recognize the complexity and CONTINUITY of the world.

Natural languages are very flexible and much more expressive than any model for a digital computer.  If you ignore that flexibility, you destroy their power and your formalization is guaranteed to be FALSE .

A translation of a natural language to a formal language may SOMETIMES be necessary.  But different applications will require different ways of translating the same NLs,   As the engineers will agree, any formal specification can only be made in the context of and with the knowledge about the specific application.

John

From: "Alex Shkotin" <alex.shkotin@gmail.com>

John,


Let's split a formalization in two steps.

I) structural representation of knowledge. Here, instead of a sequence of words, we get a structure (aka syntactic). It can even be just nonsense like

"Гло́кая ку́здра ште́ко б удлану́ла бо́кра и курдя́чит бокрёнка" see

Proposal for structural representation of English sentences see, for formal languages here.

II) structural knowledge processing. What kind of "logic" i.e. a rule of knowledge processing we use in this or that science, engineering or everyday life?

We should ask these particular scientists, engineers or citizens.

How to formalize their rules of knowledge processing is our task here. These rules are far from Modus Ponens.

Some rules we use to solve simple tasks about ugraphs pointed out here.


It should be also mentioned that there is an initial step usually not included in formalization: formal, mathematical representation of physical bodies and processes.

We usually call them computer models.  3D-twins are the most famous.

We apply our formalized knowledge to 3D twins using a computer to gain useful insights into real things and processes.


It's a good idea to separate language and logic. In many cases, we know the language of our opponent, but we don't know her rules for processing knowledge.

So we have a first-order LANGUAGE (actually a family of languages, but let's take one) and a set of first-order logics.


We need to formalize our scientific theories to use computers to their full potential.


Alex