Re: question about translating to logical connectives

Hi Brando,

On Tue, 27 Nov 2018, Miranda, Brando wrote:

> This is my first time using the forum mailing list. Hope to learn to use it well! If there is a guidance of sort of questions that are appropriate feel free to share it with me, Especially for really basic questions? :)
>
> I was trying to do exercise exercise 1.3.1 of https://www.cs.ru.nl/~freek/mizar/mizman.ps.gz 9 easy steps of Mizar. I tried translating
>
> phi iff not not phi
>
> and put it in mizar and mizar threw me some errors:
>
> :: example of a comment
> environ
>  vocabularies MY_MIZAR;
> begin
> phi implies not not psi & not not psi implies phi;
> ::>*321
> ::>
> ::> 321: Predicate symbol or "is" expected
>
> I put after the environ begin clause but throws an error that isn’t too helpful. How can I check if what I am doing in that exercise I am doing correctly?

The error marker points to the 'phi' symbol and the corresponding 
error message indicates that this 'phi' is not understood as a valid 
predicate symbol. Section 1.3.2 of the tutorial provides a few examples of 
basic predicates which can be imported from the library and used to build 
formulae.

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

Best,

Adam

===========================================================================
Dept. of Programming and Formal Methods      Fax: +48(85)738-83-33
Institute of Informatics                     Tel: +48(85)738-83-06 (office)
University of Bialystok                      E-mail: [email protected]
Ciolkowskiego 1M, 15-245 Bialystok, Poland   http://math.uwb.edu.pl/~adamn/
===========================================================================