Re: Plain logical reasoning in Mizar

[Freek Wiedijk <freek@cs.kun.nl>]

Markus:

>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.

>I've failed to duplicate this in actual Mizar.  The system seems to
>require any predicate to be defined in advance.

I don't know whether schemes allow one to do this.  I suppose so.  Did
you try that?

What I did myself, when I wanted to show someone what Mizar's reasoning
syntax looked like, was to prove (on a very low level) things like:

  x \in A implies x \in A
  x \in A & x \in B implies x \in B & x \in A
  etc.

(x, A, B being set; for "\in" read some DOS-ascii character.)  Then,
before presenting it to him, I deleted the "x \in" everywhere.  So I was
cheating a little bit.  He was impressed by the readability of the proofs,
though :-)

Freek