Is the turnstile needed?

[Tony Häger]

Why do all statements have to begin with the turnstile  ? When I just deleted all occurrences of it in set.mm, the time to verify the proofs decreased by 1%. (In a verifier I have written myself. Metamath.exe doesn't allow it.)

[Mario Carneiro]

(1) If you have written a verifier, we would be very interested to see it - we keep a list of known verifiers at http://us.metamath.org/other.html#verifiers .

(2) The turnstile is a type code, which is required by the metamath spec. It doesn't have to be a "|-" symbol, but it does have to be a constant. In ql.mm, for example, the turnstile was considered unnecessary, so a "." is used instead in its place, and this dot is hidden in the HTML display (i.e. http://us.metamath.org/qlegif/ax-r2.html).

Mario

On Fri, Jul 14, 2017 at 4:06 PM, Tony Häger <to...@tele2.se> wrote:

Why do all statements have to begin with the turnstile  ? When I just deleted all occurrences of it in set.mm, the time to verify the proofs decreased by 1%. (In a verifier I have written myself. Metamath.exe doesn't allow it.)

--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+unsubscribe@googlegroups.com.
To post to this group, send email to meta...@googlegroups.com.
Visit this group at https://groups.google.com/group/metamath.
For more options, visit https://groups.google.com/d/optout.

[Norman Megill]

If you relax the spec so that an identifying constant (such as the turnstile) is not required to distinguish logical assertions, it is possible to prove a contradiction.  I was able to derive a fascinating example of this about 20 years ago in set.mm's prop calc, but I can't seem to locate it right now.  I'll post it if I can find it.

Norm

[Mario Carneiro]

I assume the issue is something like you can't distinguish between a derivation that a symbol string is a wff and a symbol string that is provable, so all well-formed assertions are provable by "coercion" from the wff typecode. That is, there is a one step proof of "F." by applying wfal.

Mario

--

[Tony Häger]

I don't know how usable my verifier is for someone other than me. I store everything in arrays of fixed size just large enough to handle set.mm. The input file name is currently hard coded to "..\..\metamath\set2.mm".

Do you mean you want to see it in the form of source code? It is written in Ada on a Windows PC.

[Mario Carneiro]

Sure! I don't think we have any Ada verifiers yet. You could either send the source file if it is small (and we will put it on the Metamath web site), or host it on GitHub to make it accessible.

Mario

[David A. Wheeler]

On July 16, 2017 8:00:37 AM EDT, Mario Carneiro <di....@gmail.com> wrote:
>Sure! I don't think we have any Ada verifiers yet. You could either
>send
>the source file if it is small (and we will put it on the Metamath web
>site), or host it on GitHub to make it accessible.
>
>Mario
>
>On Sat, Jul 15, 2017 at 2:40 PM, Tony Häger <to...@tele2.se> wrote:
>
>> I don't know how usable my verifier is for someone other than me. I
>store
>> everything in arrays of fixed size just large enough to handle
>set.mm.
>> The input file name is currently hard coded to
>"..\..\metamath\set2.mm".
>>
>> Do you mean you want to see it in the form of source code? It is
>written
>> in Ada on a Windows PC.

You could switch the Ada code to Unbounded strings, btw:
https://www.dwheeler.com/lovelace/s8s5.htm



--- David A.Wheeler

[Tony Häger]

Ok. I include it as a zip-file in this message. I changed it to read the database file from standard in. The main program is the file "metamath_check.adb". It doesn't always print helpful messages when errors are found. It could write just : "Failed to prove wnew:wff(s->(r->p)) Line Nr  2"

At the end it doesn't write that no errors were found. It just writes something like:

          5.899564909

 1078 416 69154 1305298 424411 71272 168925 155830

where the first line is the number of seconds it took and the second line are the total numbers of constants, variables, labels, ... and so on used.

I haven't thought much about reporting bad syntax. I more or less just assume that the syntax is right.

I compile it with GNAT GPL 2015. Do you want me to send an executable (326 kB, Windows) also?

[David A. Wheeler]

On Sun, 16 Jul 2017 20:17:41 +0200, "Tony Häger" <to...@tele2.se> wrote:
> Ok. I include it as a zip-file in this message.

Thanks for posting it!

It's more convenient to put this in a git repo, and I'd be
happy to do that. (I wrote a book on Ada, so I'm very familiar with its syntax).

However.. there's no license statement, so it's not clear what we're allowed to do.
Would you please agree to some license statement, preferably an open source software one?

If you want people to "do whatever they want with it", MIT is a common choice:
https://opensource.org/licenses/MIT

If you want to require people to redistribute their changes, GPL "2.0 or later"
is a common choice:
https://opensource.org/licenses/gpl-license

There are many other possibilities, but please make your intentions clear!

--- David A. Wheeler

[Tony Häger]

On Sun, 16 Jul 2017 15:01:54 -0400 (EDT)
"David A. Wheeler" wrote:
> It's more convenient to put this in a git repo, and I'd be
> happy to do that.

Yes, you can do that. I have never used github, so I don't know how it works.

> However.. there's no license statement, so it's not
>clear what we're allowed to do.
> Would you please agree to some license statement,
>preferably an open source software one?

I was thinking about using GPL exactly as Norman has done for Metamath. But then I couldn't determine if I would have to include the whole LICENSE.TXT in the zip-file to make it valid.

That file is about the same size as my code. It seems like unnecessary waste of space. The GPL licence text must already exist in millions of copies all over the internet.

[David A. Wheeler]

> On Sun, 16 Jul 2017 15:01:54 -0400 (EDT)
> "David A. Wheeler" wrote:
> > It's more convenient to put this in a git repo, and I'd be
> > happy to do that.
> Yes, you can do that. I have never used github, so I don't know how it
> works.

I'd be happy to do that!

On Mon, 17 Jul 2017 17:20:15 +0200, "Tony Häger" <to...@tele2.se> wrote:
> I was thinking about using GPL exactly as Norman has done for Metamath.
> But then I couldn't determine if I would have to include the

> whole LICENSE.TXT in the zip-file to make it valid.That file is about the

> same size as my code. It seems like unnecessary waste of space. The GPL
> licence text must already exist in millions of copies all over the
> internet.

Just say "license it just like metamath", and I'll do the rest.
Here's what metamath's README.txt file says:
The metamath program is copyright under the terms of the GNU GPL license
version 2 or later. See the file LICENSE.TXT in this directory.

As far as file size goes, I wouldn't worry about that, especially not in the *source* repo.
On some systems packaging will deduplicate that for installation. E.g., Debian would just
refer to </usr/share/common-licenses/>. See https://www.debian.org/legal/licenses/ and
https://www.debian.org/doc/packaging-manuals/copyright-format/1.0/#license-field

--- David A. Wheeler

[Tony Häger]

On Mon, 17 Jul 2017 14:23:29 -0400 (EDT)

"David A. Wheeler" wrote:

> Just say "license it just like metamath", and I'll do the rest.

Ok David, license it just like metamath.

>.  (I wrote a book on Ada, so I'm very familiar with its syntax).

When I first saw your name in this group, it sounded familiar. I then realized that your book: "Ada95 Lovelace tutorial" was on the CD from which I first installed GNAT on my PC at home, around 1998. At that time I only knew Ada83.

[David A. Wheeler]

> On Mon, 17 Jul 2017 14:23:29 -0400 (EDT)"David A. Wheeler" wrote:
> Just say "license it just like metamath", and I'll do the rest.

On Tue, 18 Jul 2017 14:25:03 +0200, "Tony Häger" <to...@tele2.se> wrote:
> Ok David, license it just like metamath.

Great! Will do.

> >. (I wrote a book on Ada, so I'm very familiar with its syntax).
> When I first saw your name in this group, it sounded familiar. I then
> realized that your book: "Ada95 Lovelace tutorial" was on the CD from
> which I first installed GNAT on my PC at home, around 1998. At that time
> I only knew Ada83.

That's me! I haven't updated that tutorial, but the additions to Ada are
small enough that it's still useful. Someday...!

--- David A. Wheeler

[Norman Megill]

I'll mention that I have no strong preference for the GPL licensing in metamath.exe.  At the time the "advertising clause" in BSD (since removed, I think) was slightly bothersome, and the MIT license didn't exist.  I have thought about changing it to the MIT license some day and have the following comment at the top of metamath.c:

/* Contributors:  In the future I may change the license to the MIT license
   or public domain.  Therefore any patches that are contributed should be
   free of any copyright restrictions.  Thank you. - NM */

Norm

On Tuesday, July 18, 2017 at 11:17:43 AM UTC-4, David A. Wheeler wrote:

> On Mon, 17 Jul 2017 14:23:29 -0400 (EDT)"David A. Wheeler" wrote:
> Just say "license it just like metamath", and I'll do the rest.

[David A. Wheeler]

On Sun, 16 Jul 2017 20:17:41 +0200, "Tony Häger" <to...@tele2.se> wrote:
> Ok. I include it as a zip-file in this message. I changed it to read the
> database file from standard in.

Okay! Per your request, it is now posted on GitHub, here:

https://github.com/david-a-wheeler/metamath-ada

It's now much easier for other people to download, fork, etc.

--- David A. Wheeler