Is the turnstile needed?

126 views
Skip to first unread message

Tony Häger

unread,
Jul 14, 2017, 3:48:21 PM7/14/17
to meta...@googlegroups.com
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

unread,
Jul 14, 2017, 4:26:20 PM7/14/17
to metamath
(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

unread,
Jul 14, 2017, 4:38:15 PM7/14/17
to Metamath
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

unread,
Jul 14, 2017, 4:47:03 PM7/14/17
to metamath
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

unread,
Jul 15, 2017, 9:40:36 AM7/15/17
to meta...@googlegroups.com
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

unread,
Jul 16, 2017, 8:00:38 AM7/16/17
to metamath
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

unread,
Jul 16, 2017, 9:06:24 AM7/16/17
to Mario Carneiro, metamath
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

unread,
Jul 16, 2017, 2:17:44 PM7/16/17
to meta...@googlegroups.com
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?
mmc.zip

David A. Wheeler

unread,
Jul 16, 2017, 3:01:55 PM7/16/17
to metamath, metamath
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

unread,
Jul 17, 2017, 11:20:19 AM7/17/17
to meta...@googlegroups.com
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

unread,
Jul 17, 2017, 2:23:30 PM7/17/17
to metamath, metamath
> 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

unread,
Jul 18, 2017, 8:25:05 AM7/18/17
to meta...@googlegroups.com
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

unread,
Jul 18, 2017, 11:17:43 AM7/18/17
to metamath, metamath
> 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

unread,
Jul 18, 2017, 11:45:56 AM7/18/17
to Metamath
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

unread,
Jul 27, 2017, 9:30:26 PM7/27/17
to metamath, metamath
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
Reply all
Reply to author
Forward
0 new messages