Laws of Form in metamath
110 views
Skip to first unread message
naip moro
Dec 22, 2016, 3:36:20 PM12/22/16
to metamath-forum
Hello,
This is afield from the usual concerns of this forum, but some
of you may be interested in a metamath derivation of 'Laws of Form'
described at http://naipmoro.github.io/lofmm/
It is an example of a non-trivial system that is essentially
based on the empty substitution.
Regards,
naipmoro
This is afield from the usual concerns of this forum, but some
of you may be interested in a metamath derivation of 'Laws of Form'
described at http://naipmoro.github.io/lofmm/
It is an example of a non-trivial system that is essentially
based on the empty substitution.
Regards,
naipmoro
Mázsa Péter
Dec 22, 2016, 3:50:04 PM12/22/16
to metamath
FYI:
Hi! I am mmj2 v2.4.1 as of 26-Jan-2016.
Visit https://github.com/digama0/mmj2/ or
http://code.google.com/p/metamath-mmj2/
for support or bug reports.
[...]
I-UT-0015 **** Processing RunParmFile Command #1 = LoadFile,set.mm
E-LA-0101 Theorem trans: compressed proof contains invalid statement label, not found in Statement Table. Label position within the compressed proof's parentheses = 1. Statement label = sym
E-LA-0101 Theorem eucr: compressed proof contains invalid statement label, not found in Statement Table. Label position within the compressed proof's parentheses = 1. Statement label = sym
E-LA-0101 Theorem subr: compressed proof contains invalid statement label, not found in Statement Table. Label position within the compressed proof's parentheses = 1. Statement label = juxt
E-LA-0101 Theorem subst: compressed proof contains invalid statement label, not found in Statement Table. Label position within the compressed proof's parentheses = 1. Statement label = juxt
E-LA-0101 Theorem subb1: compressed proof contains invalid statement label, not found in Statement Table. Label position within the compressed proof's parentheses = 1. Statement label = juxt
E-LA-0101 Theorem subb3: compressed proof contains invalid statement label, not found in Statement Table. Label position within the compressed proof's parentheses = 1. Statement label = juxt
E-LA-0101 Theorem rep: compressed proof contains invalid statement label, not found in Statement Table. Label position within the compressed proof's parentheses = 1. Statement label = juxt
E-LA-0101 Theorem repbx: compressed proof contains invalid statement label, not found in Statement Table. Label position within the compressed proof's parentheses = 1. Statement label = juxt
E-LA-0101 Theorem ins: compressed proof contains invalid statement label, not found in Statement Table. Label position within the compressed proof's parentheses = 1. Statement label = juxt
E-LA-0101 Theorem cmmx: compressed proof contains invalid statement label, not found in Statement Table. Label position within the compressed proof's parentheses = 1. Statement label = juxt
E-LA-0101 Theorem cmmbx: compressed proof contains invalid statement label, not found in Statement Table. Label position within the compressed proof's parentheses = 1. Statement label = juxt
E-LA-0101 Theorem quadbx: compressed proof contains invalid statement label, not found in Statement Table. Label position within the compressed proof's parentheses = 1. Statement label = juxt
E-LA-0101 Theorem c1.0: compressed proof contains invalid statement label, not found in Statement Table. Label position within the compressed proof's parentheses = 1. Statement label = encl
E-LA-0101 Theorem c2.0: compressed proof contains invalid statement label, not found in Statement Table. Label position within the compressed proof's parentheses = 1. Statement label = encl
E-LA-0101 Theorem c3.0: compressed proof contains invalid statement label, not found in Statement Table. Label position within the compressed proof's parentheses = 1. Statement label = encl
E-LA-0101 Theorem c5.0: compressed proof contains invalid statement label, not found in Statement Table. Label position within the compressed proof's parentheses = 1. Statement label = encl
E-LA-0101 Theorem c4.0: compressed proof contains invalid statement label, not found in Statement Table. Label position within the compressed proof's parentheses = 1. Statement label = encl
E-LA-0101 Theorem c7.0: compressed proof contains invalid statement label, not found in Statement Table. Label position within the compressed proof's parentheses = 1. Statement label = juxt
E-LA-0101 Theorem c8.0: compressed proof contains invalid statement label, not found in Statement Table. Label position within the compressed proof's parentheses = 1. Statement label = encl
E-LA-0101 Theorem c9.0: compressed proof contains invalid statement label, not found in Statement Table. Label position within the compressed proof's parentheses = 1. Statement label = encl
E-LA-0101 Theorem lem1.1: compressed proof contains invalid statement label, not found in Statement Table. Label position within the compressed proof's parentheses = 1. Statement label = encl
E-LA-0101 Theorem c1.1: compressed proof contains invalid statement label, not found in Statement Table. Label position within the compressed proof's parentheses = 1. Statement label = void
E-LA-0101 Theorem i2.1: compressed proof contains invalid statement label, not found in Statement Table. Label position within the compressed proof's parentheses = 1. Statement label = void
E-LA-0101 Theorem j1.1: compressed proof contains invalid statement label, not found in Statement Table. Label position within the compressed proof's parentheses = 1. Statement label = encl
E-LA-0101 Theorem c4.1: compressed proof contains invalid statement label, not found in Statement Table. Label position within the compressed proof's parentheses = 1. Statement label = encl
E-LA-0101 Theorem c4cor.1: compressed proof contains invalid statement label, not found in Statement Table. Label position within the compressed proof's parentheses = 1. Statement label = encl
E-LA-0101 Theorem c6cor.1: compressed proof contains invalid statement label, not found in Statement Table. Label position within the compressed proof's parentheses = 1. Statement label = juxt
E-LA-0101 Theorem c7.1: compressed proof contains invalid statement label, not found in Statement Table. Label position within the compressed proof's parentheses = 1. Statement label = juxt
E-LA-0101 Theorem j2.1: compressed proof contains invalid statement label, not found in Statement Table. Label position within the compressed proof's parentheses = 1. Statement label = encl
E-LA-0101 Theorem lem2.2: compressed proof contains invalid statement label, not found in Statement Table. Label position within the compressed proof's parentheses = 1. Statement label = encl
E-LA-0101 Theorem b3.2: compressed proof contains invalid statement label, not found in Statement Table. Label position within the compressed proof's parentheses = 1. Statement label = void
E-LA-0101 Theorem c1.2: compressed proof contains invalid statement label, not found in Statement Table. Label position within the compressed proof's parentheses = 1. Statement label = encl
E-LA-0101 Theorem j1.2: compressed proof contains invalid statement label, not found in Statement Table. Label position within the compressed proof's parentheses = 1. Statement label = encl
E-LA-0101 Theorem lem3.2: compressed proof contains invalid statement label, not found in Statement Table. Label position within the compressed proof's parentheses = 1. Statement label = encl
E-LA-0101 Theorem c5.2: compressed proof contains invalid statement label, not found in Statement Table. Label position within the compressed proof's parentheses = 1. Statement label = encl
E-LA-0101 Theorem j1.3: compressed proof contains invalid statement label, not found in Statement Table. Label position within the compressed proof's parentheses = 1. Statement label = tq
E-LA-0101 Theorem c1.3: compressed proof contains invalid statement label, not found in Statement Table. Label position within the compressed proof's parentheses = 1. Statement label = encl
E-LA-0101 Theorem c6.3: compressed proof contains invalid statement label, not found in Statement Table. Label position within the compressed proof's parentheses = 1. Statement label = encl
E-LA-0012 Declared symbol is duplicate of other variable or constant, sym = ( Source Id: set.mm Line: 510610 Column: 21
E-LA-0018 Variable symbol = p is already active in scope. Source Id: set.mm Line: 510613 Column: 27
E-LA-0005 Constant on statement not previously declared. Type = form Source Id: set.mm Line: 510616 Column: 18
E-LA-0005 Constant on statement not previously declared. Type = form Source Id: set.mm Line: 510617 Column: 18
E-LA-0039 Statement label duplicates a symbol id. This is prohibited according to the Metamath.pdf spec change of 24-June-2006. Stmt label = tr Source Id: set.mm Line: 510618 Column: 18
E-LA-0005 Constant on statement not previously declared. Type = form Source Id: set.mm Line: 510619 Column: 18
E-LA-0005 Constant on statement not previously declared. Type = form Source Id: set.mm Line: 510620 Column: 18
E-LA-0005 Constant on statement not previously declared. Type = form Source Id: set.mm Line: 510621 Column: 18
E-LA-0005 Constant on statement not previously declared. Type = form Source Id: set.mm Line: 510622 Column: 18
E-LA-0005 Constant on statement not previously declared. Type = form Source Id: set.mm Line: 510623 Column: 18
E-LA-0005 Constant on statement not previously declared. Type = form Source Id: set.mm Line: 510624 Column: 18
E-LA-0005 Constant on statement not previously declared. Type = form Source Id: set.mm Line: 510625 Column: 18
E-LA-0005 Constant on statement not previously declared. Type = form Source Id: set.mm Line: 510643 Column: 18
E-LA-0005 Constant on statement not previously declared. Type = form Source Id: set.mm Line: 510646 Column: 24
E-LA-0005 Constant on statement not previously declared. Type = form Source Id: set.mm Line: 510649 Column: 22
E-LA-0010 Label on statement already used -- a duplicate. Label = id Source Id: set.mm Line: 510705 Column: 26
E-LA-0039 Statement label duplicates a symbol id. This is prohibited according to the Metamath.pdf spec change of 24-June-2006. Stmt label = sym Source Id: set.mm Line: 510712 Column: 30
E-LA-0039 Statement label duplicates a symbol id. This is prohibited according to the Metamath.pdf spec change of 24-June-2006. Stmt label = substr Source Id: set.mm Line: 510760 Column: 11
E-LA-0010 Label on statement already used -- a duplicate. Label = quad Source Id: set.mm Line: 510804 Column: 57
E-IO-0024 Invalid character in proof step. Token read = eucr) Source Id: set.mm Line: 510964 Column: 73
I-UT-0015 **** Processing RunParmFile Command #2 = VerifyProof,*
mmj.pa.MMJException: A-UT-0200 Step LoadFile: Cannot complete current RunParmFile request because either, a) the previous LoadFile RunParm processing detected errors in the input Metamath file; or b) a LoadFile RunParm must be input before the current RunParmFile line.
Review previous error messages to find the error.
java.lang.IllegalArgumentException: mmj.pa.MMJException: A-UT-0200 Step LoadFile: Cannot complete current RunParmFile request because either, a) the previous LoadFile RunParm processing detected errors in the input Metamath file; or b) a LoadFile RunParm must be input before the current RunParmFile line.
Review previous error messages to find the error.
at mmj.util.Boss.error(Boss.java:755)
at mmj.util.Boss.error(Boss.java:746)
at mmj.util.Boss.error(Boss.java:740)
at mmj.util.LogicalSystemBoss.getLogicalSystem(LogicalSystemBoss.java:164)
at mmj.util.VerifyProofBoss.doVerifyProof(VerifyProofBoss.java:110)
at mmj.util.Boss.lambda$putCommand$0(Boss.java:107)
at mmj.util.Boss.doRunParmCommand(Boss.java:121)
at mmj.util.BatchFramework.executeRunParmCommand(BatchFramework.java:281)
at mmj.util.BatchFramework.runIt(BatchFramework.java:223)
at mmj.util.BatchMMJ2.main(BatchMMJ2.java:53)
Caused by: mmj.pa.MMJException: A-UT-0200 Step LoadFile: Cannot complete current RunParmFile request because either, a) the previous LoadFile RunParm processing detected errors in the input Metamath file; or b) a LoadFile RunParm must be input before the current RunParmFile line.
Review previous error messages to find the error.
... 9 more
mmj.pa.MMJException: A-UT-0200 Step LoadFile: Cannot complete current RunParmFile request because either, a) the previous LoadFile RunParm processing detected errors in the input Metamath file; or b) a LoadFile RunParm must be input before the current RunParmFile line.
Review previous error messages to find the error.
logout
Saving session...
...copying shared history...
...saving history...truncating history files...
...completed.
[Process completed]
Hi! I am mmj2 v2.4.1 as of 26-Jan-2016.
Visit https://github.com/digama0/mmj2/ or
http://code.google.com/p/metamath-mmj2/
for support or bug reports.
[...]
I-UT-0015 **** Processing RunParmFile Command #1 = LoadFile,set.mm
E-LA-0101 Theorem trans: compressed proof contains invalid statement label, not found in Statement Table. Label position within the compressed proof's parentheses = 1. Statement label = sym
E-LA-0101 Theorem eucr: compressed proof contains invalid statement label, not found in Statement Table. Label position within the compressed proof's parentheses = 1. Statement label = sym
E-LA-0101 Theorem subr: compressed proof contains invalid statement label, not found in Statement Table. Label position within the compressed proof's parentheses = 1. Statement label = juxt
E-LA-0101 Theorem subst: compressed proof contains invalid statement label, not found in Statement Table. Label position within the compressed proof's parentheses = 1. Statement label = juxt
E-LA-0101 Theorem subb1: compressed proof contains invalid statement label, not found in Statement Table. Label position within the compressed proof's parentheses = 1. Statement label = juxt
E-LA-0101 Theorem subb3: compressed proof contains invalid statement label, not found in Statement Table. Label position within the compressed proof's parentheses = 1. Statement label = juxt
E-LA-0101 Theorem rep: compressed proof contains invalid statement label, not found in Statement Table. Label position within the compressed proof's parentheses = 1. Statement label = juxt
E-LA-0101 Theorem repbx: compressed proof contains invalid statement label, not found in Statement Table. Label position within the compressed proof's parentheses = 1. Statement label = juxt
E-LA-0101 Theorem ins: compressed proof contains invalid statement label, not found in Statement Table. Label position within the compressed proof's parentheses = 1. Statement label = juxt
E-LA-0101 Theorem cmmx: compressed proof contains invalid statement label, not found in Statement Table. Label position within the compressed proof's parentheses = 1. Statement label = juxt
E-LA-0101 Theorem cmmbx: compressed proof contains invalid statement label, not found in Statement Table. Label position within the compressed proof's parentheses = 1. Statement label = juxt
E-LA-0101 Theorem quadbx: compressed proof contains invalid statement label, not found in Statement Table. Label position within the compressed proof's parentheses = 1. Statement label = juxt
E-LA-0101 Theorem c1.0: compressed proof contains invalid statement label, not found in Statement Table. Label position within the compressed proof's parentheses = 1. Statement label = encl
E-LA-0101 Theorem c2.0: compressed proof contains invalid statement label, not found in Statement Table. Label position within the compressed proof's parentheses = 1. Statement label = encl
E-LA-0101 Theorem c3.0: compressed proof contains invalid statement label, not found in Statement Table. Label position within the compressed proof's parentheses = 1. Statement label = encl
E-LA-0101 Theorem c5.0: compressed proof contains invalid statement label, not found in Statement Table. Label position within the compressed proof's parentheses = 1. Statement label = encl
E-LA-0101 Theorem c4.0: compressed proof contains invalid statement label, not found in Statement Table. Label position within the compressed proof's parentheses = 1. Statement label = encl
E-LA-0101 Theorem c7.0: compressed proof contains invalid statement label, not found in Statement Table. Label position within the compressed proof's parentheses = 1. Statement label = juxt
E-LA-0101 Theorem c8.0: compressed proof contains invalid statement label, not found in Statement Table. Label position within the compressed proof's parentheses = 1. Statement label = encl
E-LA-0101 Theorem c9.0: compressed proof contains invalid statement label, not found in Statement Table. Label position within the compressed proof's parentheses = 1. Statement label = encl
E-LA-0101 Theorem lem1.1: compressed proof contains invalid statement label, not found in Statement Table. Label position within the compressed proof's parentheses = 1. Statement label = encl
E-LA-0101 Theorem c1.1: compressed proof contains invalid statement label, not found in Statement Table. Label position within the compressed proof's parentheses = 1. Statement label = void
E-LA-0101 Theorem i2.1: compressed proof contains invalid statement label, not found in Statement Table. Label position within the compressed proof's parentheses = 1. Statement label = void
E-LA-0101 Theorem j1.1: compressed proof contains invalid statement label, not found in Statement Table. Label position within the compressed proof's parentheses = 1. Statement label = encl
E-LA-0101 Theorem c4.1: compressed proof contains invalid statement label, not found in Statement Table. Label position within the compressed proof's parentheses = 1. Statement label = encl
E-LA-0101 Theorem c4cor.1: compressed proof contains invalid statement label, not found in Statement Table. Label position within the compressed proof's parentheses = 1. Statement label = encl
E-LA-0101 Theorem c6cor.1: compressed proof contains invalid statement label, not found in Statement Table. Label position within the compressed proof's parentheses = 1. Statement label = juxt
E-LA-0101 Theorem c7.1: compressed proof contains invalid statement label, not found in Statement Table. Label position within the compressed proof's parentheses = 1. Statement label = juxt
E-LA-0101 Theorem j2.1: compressed proof contains invalid statement label, not found in Statement Table. Label position within the compressed proof's parentheses = 1. Statement label = encl
E-LA-0101 Theorem lem2.2: compressed proof contains invalid statement label, not found in Statement Table. Label position within the compressed proof's parentheses = 1. Statement label = encl
E-LA-0101 Theorem b3.2: compressed proof contains invalid statement label, not found in Statement Table. Label position within the compressed proof's parentheses = 1. Statement label = void
E-LA-0101 Theorem c1.2: compressed proof contains invalid statement label, not found in Statement Table. Label position within the compressed proof's parentheses = 1. Statement label = encl
E-LA-0101 Theorem j1.2: compressed proof contains invalid statement label, not found in Statement Table. Label position within the compressed proof's parentheses = 1. Statement label = encl
E-LA-0101 Theorem lem3.2: compressed proof contains invalid statement label, not found in Statement Table. Label position within the compressed proof's parentheses = 1. Statement label = encl
E-LA-0101 Theorem c5.2: compressed proof contains invalid statement label, not found in Statement Table. Label position within the compressed proof's parentheses = 1. Statement label = encl
E-LA-0101 Theorem j1.3: compressed proof contains invalid statement label, not found in Statement Table. Label position within the compressed proof's parentheses = 1. Statement label = tq
E-LA-0101 Theorem c1.3: compressed proof contains invalid statement label, not found in Statement Table. Label position within the compressed proof's parentheses = 1. Statement label = encl
E-LA-0101 Theorem c6.3: compressed proof contains invalid statement label, not found in Statement Table. Label position within the compressed proof's parentheses = 1. Statement label = encl
E-LA-0012 Declared symbol is duplicate of other variable or constant, sym = ( Source Id: set.mm Line: 510610 Column: 21
E-LA-0018 Variable symbol = p is already active in scope. Source Id: set.mm Line: 510613 Column: 27
E-LA-0005 Constant on statement not previously declared. Type = form Source Id: set.mm Line: 510616 Column: 18
E-LA-0005 Constant on statement not previously declared. Type = form Source Id: set.mm Line: 510617 Column: 18
E-LA-0039 Statement label duplicates a symbol id. This is prohibited according to the Metamath.pdf spec change of 24-June-2006. Stmt label = tr Source Id: set.mm Line: 510618 Column: 18
E-LA-0005 Constant on statement not previously declared. Type = form Source Id: set.mm Line: 510619 Column: 18
E-LA-0005 Constant on statement not previously declared. Type = form Source Id: set.mm Line: 510620 Column: 18
E-LA-0005 Constant on statement not previously declared. Type = form Source Id: set.mm Line: 510621 Column: 18
E-LA-0005 Constant on statement not previously declared. Type = form Source Id: set.mm Line: 510622 Column: 18
E-LA-0005 Constant on statement not previously declared. Type = form Source Id: set.mm Line: 510623 Column: 18
E-LA-0005 Constant on statement not previously declared. Type = form Source Id: set.mm Line: 510624 Column: 18
E-LA-0005 Constant on statement not previously declared. Type = form Source Id: set.mm Line: 510625 Column: 18
E-LA-0005 Constant on statement not previously declared. Type = form Source Id: set.mm Line: 510643 Column: 18
E-LA-0005 Constant on statement not previously declared. Type = form Source Id: set.mm Line: 510646 Column: 24
E-LA-0005 Constant on statement not previously declared. Type = form Source Id: set.mm Line: 510649 Column: 22
E-LA-0010 Label on statement already used -- a duplicate. Label = id Source Id: set.mm Line: 510705 Column: 26
E-LA-0039 Statement label duplicates a symbol id. This is prohibited according to the Metamath.pdf spec change of 24-June-2006. Stmt label = sym Source Id: set.mm Line: 510712 Column: 30
E-LA-0039 Statement label duplicates a symbol id. This is prohibited according to the Metamath.pdf spec change of 24-June-2006. Stmt label = substr Source Id: set.mm Line: 510760 Column: 11
E-LA-0010 Label on statement already used -- a duplicate. Label = quad Source Id: set.mm Line: 510804 Column: 57
E-IO-0024 Invalid character in proof step. Token read = eucr) Source Id: set.mm Line: 510964 Column: 73
I-UT-0015 **** Processing RunParmFile Command #2 = VerifyProof,*
mmj.pa.MMJException: A-UT-0200 Step LoadFile: Cannot complete current RunParmFile request because either, a) the previous LoadFile RunParm processing detected errors in the input Metamath file; or b) a LoadFile RunParm must be input before the current RunParmFile line.
Review previous error messages to find the error.
java.lang.IllegalArgumentException: mmj.pa.MMJException: A-UT-0200 Step LoadFile: Cannot complete current RunParmFile request because either, a) the previous LoadFile RunParm processing detected errors in the input Metamath file; or b) a LoadFile RunParm must be input before the current RunParmFile line.
Review previous error messages to find the error.
at mmj.util.Boss.error(Boss.java:755)
at mmj.util.Boss.error(Boss.java:746)
at mmj.util.Boss.error(Boss.java:740)
at mmj.util.LogicalSystemBoss.getLogicalSystem(LogicalSystemBoss.java:164)
at mmj.util.VerifyProofBoss.doVerifyProof(VerifyProofBoss.java:110)
at mmj.util.Boss.lambda$putCommand$0(Boss.java:107)
at mmj.util.Boss.doRunParmCommand(Boss.java:121)
at mmj.util.BatchFramework.executeRunParmCommand(BatchFramework.java:281)
at mmj.util.BatchFramework.runIt(BatchFramework.java:223)
at mmj.util.BatchMMJ2.main(BatchMMJ2.java:53)
Caused by: mmj.pa.MMJException: A-UT-0200 Step LoadFile: Cannot complete current RunParmFile request because either, a) the previous LoadFile RunParm processing detected errors in the input Metamath file; or b) a LoadFile RunParm must be input before the current RunParmFile line.
Review previous error messages to find the error.
... 9 more
mmj.pa.MMJException: A-UT-0200 Step LoadFile: Cannot complete current RunParmFile request because either, a) the previous LoadFile RunParm processing detected errors in the input Metamath file; or b) a LoadFile RunParm must be input before the current RunParmFile line.
Review previous error messages to find the error.
logout
Saving session...
...copying shared history...
...saving history...truncating history files...
...completed.
[Process completed]
--
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.
Mario Carneiro
Dec 22, 2016, 5:01:51 PM12/22/16
to metamath
Many of those look like problems with mmj2, not with lof.mm. However the eucr) in a proof is definitely no longer valid, although metamath supports it from older days when spaces were optional. Also, the second half of the errors are from set.mm, which will not work if you try to read it after all these conflicting definitions from lof.mm. Perhaps you tried to load both files in the same session?
Norman Megill
Dec 22, 2016, 5:46:05 PM12/22/16
to Metamath
If I recall from toying with this a few years ago (although not in Metamath), some of these proofs aren't easy, so good job! Up to now miu.mm has been the only example of a Metamath database using empty substitution, so your lof.mm provides a second.
Briefly, for the uninitiated, (p) means "not p", and pq can be interpreted as either "p and q" or "p or q".
One theorem that a correspondent at the time was struggling with (I didn't try it myself) was the LoF version of the associativity of biconditional (http://us.metamath.org/mpegif/biass.html in standard prop calc), where p <-> q is defined as (((p)q)(p(q))). I don't know if he completed it. Have you tried that?
Does your proof that a Robbins algebra is a Boolean algebra follow Kauffman's?
http://homepages.math.uic.edu/~kauffman/Robbins.htm
Sadly, Spencer-Brown (the creator of LoF) passed away in August at the age of 93.
Norm
Briefly, for the uninitiated, (p) means "not p", and pq can be interpreted as either "p and q" or "p or q".
One theorem that a correspondent at the time was struggling with (I didn't try it myself) was the LoF version of the associativity of biconditional (http://us.metamath.org/mpegif/biass.html in standard prop calc), where p <-> q is defined as (((p)q)(p(q))). I don't know if he completed it. Have you tried that?
Does your proof that a Robbins algebra is a Boolean algebra follow Kauffman's?
http://homepages.math.uic.edu/~kauffman/Robbins.htm
Sadly, Spencer-Brown (the creator of LoF) passed away in August at the age of 93.
Norm
naip moro
Dec 22, 2016, 6:38:20 PM12/22/16
to metamath-forum
Thanks. I wondered if there was anything besides miu that used the empty substitution. My proof of Robbins = Boolean is much simpler than Kauffman's, since it accepts the existence of the void element (a form of cheating). Kauffman basically reinterpreted and simplified the original computer proof, which is a much more difficult task. If by associativity of biconditional you mean showing that (p <-> q) <-> r is the same as p <-> (q <-> r), that should be extremely simple, I'll look into it (associativity doesn't really exist in LoF).
Judging from Mario's reply, am I to understand that the latest version of metamath can't read lof.mm? I was puzzled by the claim that using eucr in a proof was no longer valid.--
Norman Megill
Dec 22, 2016, 7:13:15 PM12/22/16
to Metamath
On Thursday, December 22, 2016 at 6:38:20 PM UTC-5, naipmoro wrote:
Judging from Mario's reply, am I to understand that the latest version of metamath can't read lof.mm? I was puzzled by the claim that using eucr in a proof was no longer valid.
The latest version of metamath.exe reads and verifies it fine. Unlike the older version described in the Metamath book, it now automatically detects that the system uses empty substitution, so the command 'set empty_substitution on' is no longer needed to use the proof assistant.
Norm
Mázsa Péter
Dec 22, 2016, 7:41:58 PM12/22/16
to metamath
Yes I did. This is about my personal preferences, not necessarily
important but maybe worth to consider. I read that MM verified lof.mm
and decided to concatenate it to the end of set.mm, switched on
soundness check with the result below. I know that some .mm-s are
intended to be separate bodies of work, but even they won't be part of
another .mm, it may be useful if we are able to merge them if possible
(i.e., if they are conservative extensions of another main .mm, e.g.
of set.mm), even without any hassle (i.e., by concatenation) when
needed. This can be a reason of merged soundness checks and compatible
definitions.
>>> To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.
important but maybe worth to consider. I read that MM verified lof.mm
and decided to concatenate it to the end of set.mm, switched on
soundness check with the result below. I know that some .mm-s are
intended to be separate bodies of work, but even they won't be part of
another .mm, it may be useful if we are able to merge them if possible
(i.e., if they are conservative extensions of another main .mm, e.g.
of set.mm), even without any hassle (i.e., by concatenation) when
needed. This can be a reason of merged soundness checks and compatible
definitions.
>>> 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.
>>
>>
>> --
>> 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+u...@googlegroups.com.
>>> Visit this group at https://groups.google.com/group/metamath.
>>> For more options, visit https://groups.google.com/d/optout.
>>
>>
>> --
>> You received this message because you are subscribed to the Google Groups "Metamath" group.
>> 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.
>
>
> --
> 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+u...@googlegroups.com.
>> Visit this group at https://groups.google.com/group/metamath.
>> For more options, visit https://groups.google.com/d/optout.
>
>
> --
> You received this message because you are subscribed to the Google Groups "Metamath" group.
David A. Wheeler
Dec 22, 2016, 8:07:09 PM12/22/16
to meta...@googlegroups.com, naip moro
--- David A.Wheeler
Mario Carneiro
Dec 22, 2016, 8:35:42 PM12/22/16
to metamath
Mario Carneiro
Dec 22, 2016, 8:41:12 PM12/22/16
to metamath
(Ignore the previous empty email.)
On Thu, Dec 22, 2016 at 6:38 PM, naip moro <naip...@gmail.com> wrote:
Judging from Mario's reply, am I to understand that the latest version of metamath can't read lof.mm? I was puzzled by the claim that using eucr in a proof was no longer valid.
It's not that metamath can't read lof.mm, but rather that the specification has since been tightened up in a few ways, which are still allowed by metamath.exe but are technically incorrect. This explains why metamath.exe will be able to read your file but other independent verifiers such as mmj2 may not. I would encourage you to make your file conform with the spec, so that all verifiers, not just metamath.exe, will be able to make sense of it.
As for eucr, it's not that "eucr" is not valid, but rather "eucr)", that is, eucr with no space separating it from the end of the label list. A space or newline is required at that location per the spec, so it should read "eucr )".
Mario
Norman Megill
Dec 22, 2016, 8:51:29 PM12/22/16
to Metamath
On Thursday, December 22, 2016 at 5:01:51 PM UTC-5, Mario Carneiro wrote:
Many of those look like problems with mmj2, not with lof.mm. However the eucr) in a proof is definitely no longer valid, although metamath supports it from older days when spaces were optional.
This should have caused metamath.exe to produce a warning or error message. I overlooked this when putting in the space enforcement and will fix it for the next version.
In the meantime, 'save proof */compressed' will clean up any such problems.
Norm
Mario Carneiro
Dec 22, 2016, 8:52:51 PM12/22/16
to metamath
On Thu, Dec 22, 2016 at 7:41 PM, Mázsa Péter <pe...@mazsa.com> wrote:
On Thu, Dec 22, 2016 at 11:01 PM, Mario Carneiro <di....@gmail.com> wrote:
>
> Many of those look like problems with mmj2, not with lof.mm. However the eucr) in a proof is definitely no longer valid, although metamath supports it from older days when spaces were optional. Also, the second half of the errors are from set.mm, which will not work if you try to read it after all these conflicting definitions from lof.mm. Perhaps you tried to load both files in the same session?
Yes I did. This is about my personal preferences, not necessarily
important but maybe worth to consider. I read that MM verified lof.mm
and decided to concatenate it to the end of set.mm, switched on
soundness check with the result below. I know that some .mm-s are
intended to be separate bodies of work, but even they won't be part of
another .mm, it may be useful if we are able to merge them if possible
(i.e., if they are conservative extensions of another main .mm, e.g.
of set.mm), even without any hassle (i.e., by concatenation) when
needed. This can be a reason of merged soundness checks and compatible
definitions.
This is a reasonable desire, but there are certain things that we know will be inconsistent with set.mm. In particular, "wff ( ph )" and "wff" (empty wff) are both going to cause ambiguity and possibly inconsistency in set.mm. Since lof.mm works with a different typecode, namely "form", this might be okay; it just means that the two databases will exist independently. However, you won't be able to use single letters as form variables, because they are set variables in set.mm. You also have to remove or ignore the repeated $c commands for constants, and get around the duplicati of theorems and tokens in set.mm with theorems or tokens in lof.mm. Long story short, appending databases generally doesn't work unless the databases were designed with this in mind.
The rule "form x y" is actually ambiguous with itself in lof.mm, even without set.mm getting involved. This means that it is not an unambiguous formal system, so certain features of mmj2 (anything that depends on grammar parsing) will not work. Even though or/and is associative, so this "shouldn't matter", it allows you to do certain magical manipulations with the string representation that you can't with a tree representation, by reinterpreting the string's parse tree in the middle of a proof.
naip moro
Dec 22, 2016, 10:09:15 PM12/22/16
to metamath-forum
I fixed the 'eucr)' problem. I certainly hope that all verifiers can read my file. However, you also wrote in another message:
You are pointing to (what seems to me) a fundamental feature that allows lof.mm to succeed. I do not know metamath well enough to imagine a work-around.
Regards,On Thu, Dec 22, 2016 at 8:41 PM, Mario Carneiro <di....@gmail.com> wrote:
It's not that metamath can't read lof.mm, but rather that the specification has since been tightened up in a few ways, which are still allowed by metamath.exe but are technically incorrect. This explains why metamath.exe will be able to read your file but other independent verifiers such as mmj2 may not. I would encourage you to make your file conform with the spec, so that all verifiers, not just metamath.exe, will be able to make sense of it.As for eucr, it's not that "eucr" is not valid, but rather "eucr)", that is, eucr with no space separating it from the end of the label list. A space or newline is required at that location per the spec, so it should read "eucr )".Mario
--
Mario Carneiro
Dec 22, 2016, 11:03:26 PM12/22/16
to metamath
On Thu, Dec 22, 2016 at 10:09 PM, naip moro <naip...@gmail.com> wrote:
I fixed the 'eucr)' problem. I certainly hope that all verifiers can read my file. However, you also wrote in another message:You are pointing to (what seems to me) a fundamental feature that allows lof.mm to succeed. I do not know metamath well enough to imagine a work-around.
"The rule "form x y" is actually ambiguous with itself in lof.mm, even without set.mm getting involved. This means that it is not an unambiguous formal system, so certain features of mmj2 (anything that depends on grammar parsing) will not work."
Usually, in standard logical frameworks, 'and' and 'or' are binary operations, which are iterated to get n-ary conjunction or disjunction. That is, in a logic textbook you might find
A /\ B /\ C /\ D
but this will generally be recognized as a convenient shorthand for ((A /\ B) /\ C) /\ D or something like this, so that the associativity is well-defined. In metamath and other string systems, it is possible to stay formally ambiguous about the associativity, so that one could apply commutativity twice to get
A /\ B /\ C = B /\ C /\ A = C /\ A /\ B
which is not possible in a tree representation without at least one intermediate application of associativity (since the left equality requires interpreting the central expression as (B /\ C) /\ A and the right needs B /\ (C /\ A)).
It may very well be the case that this is to you a strength of the system, that this string manipulation is exactly what you want from metamath. In this case, metamath will continue to support you, but some of the advanced work that requires unambiguous parsing will not be applicable.
If instead you wish to salvage unambiguity from the system, you must craft the parsing rules so that everything is parsed correctly and unambiguously, according to a context-free grammar. The standard way to get lists in a CFG is through an extra typecode, for the item type. Before:
F -> <empty> | F F | ( F )
after:
F -> <empty> | F A
A -> ( F )
This will force left-associative interpretations of all strings. In order to get other bracketings (which you would previously get for free), you can either introduce another bracket which acts as the identity:
F -> <empty> | F A
A -> ( F ) | [ F ]or use double negation ( ( F ) ) to get an atom out of a formula. Thus "x y z" is interpreted as (x \/ y) \/ z, while "x ( ( y z ) )" or "x [ y z ]" is treated as "x \/ (y \/ z)" (or more precisely "x \/ -. -. (y \/ z)" which is equivalent). In metamath notation:
$c ( ) = |- form atom $.
$v p q A $.
tp $f form p $.
tq $f form q $.
aA $f atom A $.
$( Empty space is a form. $)
void $a form $.
$( If p is a form, then (p) is an atom. $)
encl $a atom ( p ) $.
$( If p is a form and A is an atom, then p A is a form. $)
juxt $a form p A $.
$( Optional: a second enclosure primitive $)
encl2 $a atom [ p ] $.
$c ( ) = |- form atom $.
$v p q A $.
tp $f form p $.
tq $f form q $.
aA $f atom A $.
$( Empty space is a form. $)
void $a form $.
$( If p is a form, then (p) is an atom. $)
encl $a atom ( p ) $.
$( If p is a form and A is an atom, then p A is a form. $)
juxt $a form p A $.
$( Optional: a second enclosure primitive $)
encl2 $a atom [ p ] $.
Mario
Mázsa Péter
Dec 22, 2016, 11:51:33 PM12/22/16
to metamath
On Fri, Dec 23, 2016 at 2:52 AM, Mario Carneiro <di....@gmail.com> wrote:
>
> On Thu, Dec 22, 2016 at 7:41 PM, Mázsa Péter <pe...@mazsa.com> wrote:
>> This can be a reason of merged soundness checks and compatible
>> definitions.
>
>
> On Thu, Dec 22, 2016 at 7:41 PM, Mázsa Péter <pe...@mazsa.com> wrote:
>> This can be a reason of merged soundness checks and compatible
>> definitions.
>
> Long story short,
> appending databases generally doesn't work unless the databases were
> designed with this in mind.
Exactly. And because lof.mm was designed with the priority in mind to
> appending databases generally doesn't work unless the databases were
> designed with this in mind.
reinterpret the book, including its formalism, in metamath, which is a
great object in itself, it must be in a .mm different from set.mm. All
what I say is that I like clean interpretations in set.mm like of
Łukasiewicz and of Aristotle both with original notations seem to be
quite strange from here. But that would be another project with
another benefits: sorry that I used the (concatenation soundness)
requirement of a different (however closely related) project to this
one without due reflection.
naip moro
Dec 23, 2016, 11:41:02 AM12/23/16
to metamath-forum
Thank you for pointing me in the right direction. If I can retain the lucidity of the present system (by which I mean keeping the theorems unchanged), I may try to reformulate it.
Based as it is on systematic ambiguity, LoF is more akin to poetry than to logic, and I was surprised that metamath allowed me to formalize it without any fuss. I do consider that a strength of metamath.--
Norman Megill
Dec 24, 2016, 11:08:51 AM12/24/16
to Metamath
Philip Meguire sent me the following message:
> Attached is my LoF-style demonstration of the associativity of the biconditional.
> The discussion in the thread whose link you kindly sent me, does not mention Ingo Dahn's (1998, Journal of Algebra) rework of McCune's 1997 proof that Robbins <==> Boolean. I have translated that rework into the notation of LoF, and am able to state the proof in 2 single spaced A4 pages.
I have attached both PDFs.
> Attached is my LoF-style demonstration of the associativity of the biconditional.
> The discussion in the thread whose link you kindly sent me, does not mention Ingo Dahn's (1998, Journal of Algebra) rework of McCune's 1997 proof that Robbins <==> Boolean. I have translated that rework into the notation of LoF, and am able to state the proof in 2 single spaced A4 pages.
I have attached both PDFs.
On Friday, December 23, 2016 at 11:41:02 AM UTC-5, naipmoro wrote:
Thank you for pointing me in the right direction. If I can retain the lucidity of the present system (by which I mean keeping the theorems unchanged), I may try to reformulate it.Based as it is on systematic ambiguity, LoF is more akin to poetry than to logic, and I was surprised that metamath allowed me to formalize it without any fuss. I do consider that a strength of metamath.
Indeed, LoF seems as much a work of philosophy as of mathematics. The Wikipedia pages are interesting to read:
https://en.wikipedia.org/wiki/Laws_of_Form
https://en.wikipedia.org/wiki/G._Spencer-Brown
In the long term, a future version of the Metamath language (and/or its tools) might be more tame in what it will tolerate; for example, it may not accept systems with ambiguous grammar. But that will probably be a long time coming, and in the meantime feel welcome to exploit its somewhat wild nature. Perhaps the present language would continue in its own direction to accommodate such systems, who knows. In any case, Mario has done an extensive and rigorous analysis of the present language, including ambiguous grammars, in his "Models for Metamath" :
https://arxiv.org/abs/1601.07699
Norm
naip moro
Dec 24, 2016, 5:58:06 PM12/24/16
to metamath-forum
Yeah, proving the associativity of the biconditional in LoF is easy,
proving it in metamath's LoF is the chore. Still working on it, but
holidays intervene! I hope I didn't misrepresent my posting as an
authoritative summary of the literature; it's just an initial foray,
a sigh of relief that I actually got as far as I did.
Btw, I've been looking for that Meguire book, but it's out-of-print and
impossible to find.
Regards,proving it in metamath's LoF is the chore. Still working on it, but
holidays intervene! I hope I didn't misrepresent my posting as an
authoritative summary of the literature; it's just an initial foray,
a sigh of relief that I actually got as far as I did.
Btw, I've been looking for that Meguire book, but it's out-of-print and
impossible to find.
--
naip moro
Dec 30, 2016, 2:54:02 PM12/30/16
to metamath-forum
Hello,
I've appended a 'topics section' to the end of lof.mm, where I briefly discuss the associativity of logical connectives and prove the associativity of the biconditional.https://naipmoro.github.io/lofmm/
https://github.com/naipmoro/lofmm/blob/master/lof.mm
On Thu, Dec 22, 2016 at 5:46 PM, Norman Megill <n...@alum.mit.edu> wrote:
One theorem that a correspondent at the time was struggling with (I didn't try it myself) was the LoF version of the associativity of biconditional (http://us.metamath.org/mpegif/biass.html in standard prop calc), where p <-> q is defined as (((p)q)(p(q))). I don't know if he completed it. Have you tried that?
--
Reply all
Reply to author
Forward
0 new messages