Re: rigorous and formal proof

[Andrzej Trybulec <trybulec@math.uwb.edu.pl>]

On Thu, 3 Dec 1998, Roman Matuszewski wrote:

> 
> This below is the answer of Claus Zinn for my question concerning
> difference between "rigorous" and "formal" proof.

> The difference between 'rigorous and 'formal' proofs is not that easy,
> I guess. It may even be they that the english usage for these terms refer
> to the same. One attempt would be:


Some years ago Leszek Szczerba proposed clear, albeit practical, distinction
between "forma" and "rigorous" proofs. If I recall:

The proof is "formal", if one is able (or "one see how") to expand it
to prmitive rules.

The proof is "rigorous", if one is certain that steps are correct, no 
gaps  or omissions, however breaking to primitive rules may cause some
work.

Then the proofs in Baby Mizar (Mizar-MSE) are "formal" at least for 
exprerienced users, proofs in PC Mizar are only rigorous.

Leszek, am I correct ?

Andrzej Trybulec