Re: Plain logical reasoning in Mizar

[Andrzej Trybulec <trybulec@wwwserve.cs.shinshu-u.ac.jp>]

Markus Wenzel wrote:
> 
> Is it possible to do plain logical reasoning in Mizar?  For example,
> derive basic propositional tautologies such as A --> A, A & B --> B & A,
> etc.

Propositional tautologies are not very interesting in Mizar, because
they are obvious (if they are not too large). The same goes for
Mizar-MSE.

> Predicates with zero arguments seem to do the trick in Mizar-MSE:
> 
> I: A[] implies A[]
>     proof
>       assume a: A[];
>       thus A[] by a;
>    end;
> 
> I've failed to duplicate this in actual Mizar.  The system seems to
> require any predicate to be defined in advance.

This is true, almost. You may use the absolute permissiveness, then this
requirement is void.

E.g.

definition
 assume contradiction;
 pred P means
:P_def: not contradiction;
end;

the definitional theorem put at the label P_def is then

  "contradiction implies (P iff not contradiction)"

So it cannot be used at all. The syntax looks crazy, but the meaning
is not so. The P_def definition means that in an incosistent theory
predicate P means VERUM (or FALSUM or whatever) and is has no meaning in
a consistent theory (the domain of the definition is empty).

Similarly you can introduce predicates with positive number of
arguments.

definition let x,y be Any;
 assume contradiction;
  pred P2 x,y means contradiction;
end;

It is not worth to put a label before the definiens, you cannot refer
usefully to it.

Once again, "assume contradiction" does not mean that we want the theory
be incosistent, it means that only in an inconsistent theory the
predicate has a meaning (supposing we may assign to it any meaning in an
incosistent theory). The classical quantifier calculus is consistent, so
...

Syntax:

the only thing to do is to create a vocabulary file, e.g. LANGUAGE.VOC
and to put on it the predicate symbols that you want. May even better
just write a file LANGUAGE.MIZ in which you introduce all predicates
that you want and then you have tool to do logic tautologies:

  environ vocabulary LANGUAGE;
   constructors LANGUAGE;
   notation LANGUAGE;
  begin
   :: now you can use your predicates, but only logical tautologies
   :: can be proved