Glossary FDLnotes

Words and Images vs Formality

We believe that the choice of which names we attach to concepts or objects, and how expressions are presented to the senses are not normally pertinent to the Formal significance or correctness of formal artifacts (but see Bates's Point). We expect uniform renaming or alteration of notation to leave formal correctness intact.

On the other hand, our own abilities to understand formal material are often deeply tied to our habits of notation and nomenclature. Indeed they are so important that we must neither ignore these matters nor presume to be able to formalize them. Such habits may vary from person to person, from circumstance to circumstance, and from time to time. Often there is dispute over such choices of naming and notation, which need not impinge on the formalization process.

The use of abstract syntactic structure is widely understood to isolate structural features of notation pertinent to "formal" correctness. Of course there is a sense in which to write "3-4" to mean the result of subtracting three from four (instead of four from three), or to mean the sum instead of the difference, is wrong, but that is not a matter of formal correctness as intended here. When we employ formal notation in an informal context, such errors can be ruinous, and so we must have ways of avoiding them, but we take this to be a different issue from formal correctness.

Our project conceives formal structure, therefore, to be abstract. In particular we take the expressions or Texts to be essentially like parse trees of a very simple grammar, and deem it to be a separate matter how they are viewed or created or edited by humans.

Similarly, though written natural language is essential and should be included among, and intimately interwoven with, formal expression, we consider the meaning and syntax of natural language as a whole beyond the purview of the FDL project per se. As researchers succeed at formalizing parts of natural language, those parts may come to occupy more of the formal domain as those formal methods are introduced, but we must not depend upon that eventuality or put off the incorporation of informal language as mere uninterpreted text.

The independence of formal structure from notational appearance, epitomized by the use of abstract syntax trees instead of strings, eliminates much notational dispute from the formulation of formal expressions. But there remain the problems of resolving disputes and informal errors involving the names appearing as atomic components of formal structures. See Formal vs Informal, Readings, Naming Problems, and Abstract Ids & Closed Maps. IF YOU CAN SEE THIS go to

Glossary FDLnotes