Re: [mizar] question about translating to logical connectives

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

Hi Brando and Adam,

>> begin
>> phi implies not not psi & not not psi implies phi;
>> ::>*321

If you write something like this, Mizar won't know what "phi"
and "psi" is.  Mizar does not have variables for statements.

You can prove this as a scheme, but then you'll need to
write phi[] and psi[] I think, and I haven't written Mizar
in a decade or so, so I don't remember exactly what schemes
look like anymore.  Also schemes have not been treated at
this part of the tutorial yet, so the exercise certainly
didn't want you to do anything like that.  But if you want
to _check_ second order formulas like this in Mizar, you'll
need something like schemes.

Alternatively, you can just define "fake" phi's and psi's,
so you can write somethign like this directly without the
brackets.  But then you need to put the symbols "phi" and
"psi" in your vocabulary my_mizar.voc, as

Rphi
Rpsi

and give them arbitrary definions like

definition
  pred phi means not contradiction;
end;

etc.  In that case you don't need a scheme, and you _can_
write a line like the one you were writing, but you are not
really proving something about arbitrary phi and psi then.

Also, what you write seems a mixture of the first and the
second formula from the exercise?  Also, I don't remember
what the priorities of logical operators in Mizar are,
but won't this be parsed as

  phi implies ((not not psi & not not psi) implies phi)

?

>I guess that Freek intended this kind of exercise to be
>"contemplated" rather than directly checked with Mizar.

Yes, I was writing "logical notation", so I was imagining
writing the result on paper or in latex.  The answer to
the first line would be something like (using latex):

  \phi \iff \neg\neg\phi

In fact, I had answers for some of the exercises when I
wrote this, although I don't remember whether this one was
one of those.  If you look at the tex source of this document
(not too closely, the latex is horrible), you might be able
to see that.

Freek