Re: Plain logical reasoning in Mizar

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

Grzegorz Bancerek wrote:
> 
> On Sat, 13 Nov 1999, Freek Wiedijk wrote:
> 
> > Markus:
> >
> > >Is it possible to do plain logical reasoning in Mizar?  For example,
...
> > I don't know whether schemes allow one to do this.  I suppose so.  Did
> > you try that?
> 
> Of course, you may do it by scheme:
> 
> sch1 {A[]}:
>  A[] implies A[]
> proof
>  assume A[];
>  hence A[];
> end;

The problem is that if you want to do the first order logic you are
restricted to one scheme. This A[] predicate is a second order variable
so when you use schemes to justify schemes actually you develop what's
the name? invariant logic?
Anyway, you develop something that Grzegorczyk proposed to call the 1.5
order logic. On QED Workshop II, if I recall, the common opinion was
that the order is rather 1.1 or even 1.01.

Andrzej