Re: The formal and informal proofs

T.B. wrote:

> Hello,
> Is a system strictly formal when each and every of its parts is made
> entirely explicit, i.e. when the computing model with which it is
> identified is a register machine? I hope I am not being a disgrace

Only dishonesty, greed, the way some people treat others here, etc. are
disgraceful.

If you are a computer programmer, think of a formal exposition (system,
theorem, proof) as "programmable specs". It gives the exact syntax and
semantics of a system which contains an infinite number of elements
(wffs, theorems, proofs.) An informal exposition is a "spec" in which
the semantics are given but the actual input and output (the syntax) is
not given. You know what they mean, but no formal representation of
the infinite number of variations is given.

System = specifications for a computer program

Formal = syntax and semantics are given

Informal = only semantics are given

C-B

> Tom

.

Relevant Pages

  • Re: man page syntax for +script
    ... The man pages for [bind] and [comm hook] both describe how you can either replace the current script or append to it, but they give slightly different syntaxes. ... But the syntax for makes it appear that the + and the script are separate arguments, and that caused me some confusion. ... you have a distorted view of what is syntax and what is semantics in Tcl. ...
    (comp.lang.tcl)
  • Re: man page syntax for +script
    ... The man pages for and both describe how you can either replace the current script or append to it, but they give slightly different syntaxes. ... But the syntax for makes it appear that the + and the script are separate arguments, and that caused me some confusion. ... The plus is a semantic definition that these two unrelated commands put on their last argument, expr has a very different semantic definition of "+". ... you have a distorted view of what is syntax and what is semantics in Tcl. ...
    (comp.lang.tcl)
  • Re: MV Keys
    ... In *practise*, you may not need to worry ... Through creative use of syntax, ... I don't envision a separate language; ... even within the given semantics. ...
    (comp.databases.theory)
  • Re: they mention various metaphors and ramble about various concerns (Re: Kuratowski Ordered Pair)
    ... it means to call x the semantics for syntax y? ... (kind of like your archaic understanding of syntax-semantics ... and i did not see much of substance in response ...
    (sci.math)
  • Re: Relative merits of Lisp-1 vs. Lisp-2?
    ... language syntax and semantics unless you think that by adding these ... clearly semantics will not. ... be handwaved away, too, layer after layer. ... Clearly there can be another projection ...
    (comp.lang.lisp)