Plain logical reasoning in Mizar

[Markus Wenzel <wenzelm@informatik.tu-muenchen.de>]

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.

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.


	Markus

-------------------------------------------------------------------
Institut für Informatik, TU München, http://www.in.tum.de/~wenzelm/
--- <>< -----------------------------------------------------------