So this leads to
$ ./pmGenerator -c -n -s CpCCqCprCCNrCCNstqCsr --parse
DDD11DDD11D11DDDDD111111DDDDD111111,DDD1DDDDDD1DDD11DD1D111DDDDD1111111DDDDD111111111D111,DDDDD1D111DDDDD111111DDD11DDD1D111DDDDD111111DDDDD1111111,DDDDD1DDD11DDD11D11DDDDD111111DDDDD1111111DDDD11DDD1DDD11DD11DDD1D111DDDDD111111DDDDD1DDD11DD1D111DDDDD1111111DDDDD11111111D11DDD11DDD1D111DDDDD1111111DDD1DDDD11D1DD1DDD1DDDDD111111D1111DDDDD111111DDD11D1DDDDD111111DDDDD111111DDD1D1DDDDDD1DDD11DD1D111DDDDD1111111DDDDD1111111111DDDDD111111DDDDD11111111DDD1DDDDD1D111DDDDD111111DDD11DDD1D111DDDDD111111DDDDD111111DDD11DDD1111DDD11DDD1DDD1DDD11D11DDDDD111111111DDDDD1111111D1DDD11DDD11D11DDDDD111111DDDDD111111DDDD11D11DDDDD111111DD1DDD1DDDDDD1DDD11DD1D111DDDDD1111111DDDDD111111111D1111
-s -n -o data/w2-tmp.txt
[...]
$ ./pmGenerator --transform data/w2-tmp.txt -f -n -t CpCqp,Cpp,CpCNpq,CCNppp -j
-1 -s CpCCNqCCNrsCNqCCNCCNtCCNuvNpCutwNCxCCyCxzCCNzCCNabyCazCrq,CpCqCrCsCtq -p
-2 -d
CpCCqCprCCNrCCNstqCsr = 1
[0] CpCCNqCCNrsCNqCCNCCNtCCNuvNpCutwNCxCCyCxzCCNzCCNabyCazCrq = DDDDD111111
[1] Cpp = DDD11DDD11D11[0][0]
[2] CpCqCrCsCtq = DDDDD1DDD11DD1D111[0]1[0]11
[3] CpCqp = DDD1D[2]1D111
[4] CpCNpq = DDDDD1D111[0]DDD11DDD1D111[0][0]1
[5] CCNppp =
DDDDD1[1]1DDDD11DDD1DDD11DD11DDD1D111[0][2]D11DDD11DDD1D111[0]1DDD1DDDD11D1DD1DDD1[0]D1111[0]DDD11D1[0][0]DDD1D1D[2]11[0][0]11DDD1DDDDD1D111[0]DDD11DDD1D111[0][0]DDD11DDD1111DDD11DDD1DDD1DDD11D11[0]111[0]1D1[1]DDDD11D11[0]DD1[3]1
as a new compact solution, with debug output
There are 35 steps towards Cpp / C0.0 (index 8).
There are 53 steps towards CpCqp / C0C1.0 (index 12).
There are 57 steps towards CpCNpq / C0CN0.1 (index 14).
There are 535 steps towards CCNppp / CCN0.0.0 (index 15).
________________________________
Von: Discher, Samiro
Gesendet: Donnerstag, 13. Juni 2024 20:14:01
An: Metamath
Betreff: AW: [Metamath] Re: Shortest possible axiom for propositional calculus
Correction:
Sorry, I messed up the part after
$ ./pmGenerator --transform data/w2.txt -f -n -t CpCqp,Cpp,CpCNpq,CCNppp -j -1
-e
which should of course use your proof instead of the old one, and
$ ./pmGenerator --transform data/w2-tmp.txt -f -n -t CpCqp,Cpp,CpCNpq,CCNppp -j
-1 -s
CpCCNqCCNrsCNqCCNCCNtCCNuvNpCutwNCxCCyCxzCCNzCCNabyCazCrq,CpCqCrCsCtq,CpCqCrp
________________________________
Von: Discher, Samiro
Gesendet: Donnerstag, 13. Juni 2024 20:07:33
An: Metamath
Betreff: AW: [Metamath] Re: Shortest possible axiom for propositional calculus
Yes, this is a w2: L2: 781↦535 improvement, congratulations!
Using
$ ./pmGenerator -c -n -s CpCCqCprCCNrCCNstqCsr --parse
DDDDD1DDD11DDD11D11DDDDD111111DDDDD1111111DDDD11DDD1DDD11DD11DDD1D111DDDDD111111DDDDD1DDD11DD1D111DDDDD1111111DDDDD11111111D11DDD11DDD1D111DDDDD1111111DDD1DDDD11D1DD1DDD1DDDDD111111D1111DDDDD111111DDD11D1DDDDD111111DDDDD111111DDD1D1DDDDDD1DDD11DD1D111DDDDD1111111DDDDD1111111111DDDDD111111DDDDD11111111DDD1DDDDD1D111DDDDD111111DDD11DDD1D111DDDDD111111DDDDD111111DDD11DDD1111DDD11DDD1DDD1DDD11D11DDDDD111111111DDDDD1111111D1DDD11DDD11D11DDDDD111111DDDDD111111DDDD11D11DDDDD111111DD1DDD1DDDDDD1DDD11DD1D111DDDDD1111111DDDDD111111111D1111
-s -n -o data/tmp.txt
$ ./pmGenerator --transform data/tmp.txt -f -n -t CpCqp,Cpp,CpCNpq,CCNppp -p -2
-d
reveals that CpCNpq is not part of the proof, so via combining the outputs of
$ ./pmGenerator --transform data/tmp.txt -f -n -t CpCqp,Cpp,CCNppp -j -1 -e
$ ./pmGenerator --transform data/w2.txt -f -n -t CpCqp,Cpp,CpCNpq,CCNppp -j -1
-e
this results in
$ ./pmGenerator -c -n -s CpCCqCprCCNrCCNstqCsr --parse
DDD11DDD11D11DDDDD111111DDDDD111111,DDD1DDDDDD1DDD11DD1D111DDDDD1111111DDDDD111111111D111,DDDDD1D111DDDDD111111DDD11DDD1D111DDDDD111111DDDDD1111111,DDDDD1DDD11DDD11D11DDDDD111111DDDDD1111111DDDD11DDD1DDD11DD11DDD1D111DDDDD111111DDDDD1DDD11DD1D111DDDDD1111111DDDDD11111111D11DDD11DDD1D111DDDDD1111111DDD1DDDD11D1DD1DDD1DDDDD111111D1111DDDDD111111DDD11D1DDDDD111111DDDDD111111DDD1D1DDDDDD1DDD11DD1D111DDDDD1111111DDDDD1111111111DDDDD111111DDDDD11111DDDDD1111111DDDD11DDD11DD11DDD1D111DDDDD111111DDDDD1DDD11DD1D111DDDDD1111111DDDDD11111111DDD1DDD11D1DDD11DDD1D111DDDDD1111111DDD11DDD1DDD1DD1D111111DDDDD1111111DDD1DDD1DDD1DDD1DDDDD111111D1111DDDDD1111111DDDDD1111111DDDDD111111DDDDD11111DDDDD1111111DDD1DDDDD1D111DDDDD111111DDD11DDD1D111DDDDD111111DDDDD111111DDD11DDD1111DDD11DDD1DDD1DDD11D11DDDDD111111111DDDDD1111111D1DDD11DDD11D11DDDDD111111DDDDD111111DDDD11D11DDDDD111111DD1DDD1DDDDDD1DDD11DD1D111DDDDD1111111DDDDD111111111D1111
-s -n -o data/w2-tmp.txt
i.e.
CpCCqCprCCNrCCNstqCsr = 1
[0] CCpCCqCCrCqsCCNsCCNturCtsvCCNvCCNwxpCwv = D11
[1]
CCNCCNCpqCCNrsCtCCuCCvCuwCCNwCCNxyvCxwqCrCpqCCNzaCNqCCNpbtCzCCNCpqCCNrsCtCCuCCvCuwCCNwCCNxyvCxwqCrCpq
= DD1[0]1
[2] CpCCNCCNqCCNrsCNqCCNtuNpCrqCCNvwtCvCCNqCCNrsCNqCCNtuNpCrq = DD[0]11
[3]
CCNCCNpCCNqrCNpCCNstNCuCCvCuwCCNwCCNxyvCxwCqpCCNzasCzCCNpCCNqrCNpCCNstNCuCCvCuwCCNwCCNxyvCxwCqp
= D[2]1
[4] CpCCNqCCNrsCNqCCNCCNtCCNuvNpCutwNCxCCyCxzCCNzCCNabyCazCrq = D[3]1
[5] CCpCCqCCNrCCNstCNrCCNCCNuCCNvwNqCvuxNCyCCzCyaCCNaCCNbczCbaCsrdCCNdCCNefpCed
= D1[4]
[6] CCCpCCqCprCCNrCCNstqCsruCvu = DD[0][0][4]
[7] CCCNpqrCCNCpsCCNtuCrCCvCCwCvxCCNxCCNyzwCyxsCtCps = D[1][4]
[8] CpCCNqCCNrsCNqCCNCtpuNCvCCwCvxCCNxCCNyzwCyxCrq = D[3][4]
[9] CCNCpCqrCCNstCCNquCNrCCNCvCCwCvxCCNxCCNyzwCyxaNpCsCpCqr = D[0][7]
[10] CCNCCNpCCNqrsCqpCCNtuCCNCvCCwCvxCCNxCCNyzwCyxaNsCtCCNpCCNqrsCqp =
DD1DD[5][0]11
[11] CpCqCCCNCrCCsCrtCCNtCCNuvsCutwNqx = D[9]1
[12] Cpp = DD[0][6][4]
[13] CCpCCqqrCCNrCCNstpCsr = D1[12]
[14] CpCqCrCsCtq = DDDDD1DD[0][1][4]1[4]11
[15] CCpCCqCrCsCtquCCNuCCNvwpCvu = D1D[14]1
[16] CpCqp = DD[15][0]1
[17] CCNCpqCCNrsCCtCupCCvCCwCvxCCNxCCNyzwCyxqCrCpq = D[7]D[9][4]
[18] CpCNpq = D[17]1
[19] CpCqCrp = DD[0][9][14]
[20] CCNppp =
DDDD[13]1DDD[0]DDD1[19][0][11]DDD1DDD[0]D1[10][4]DD[0][5][4]DDD1[15]1[4][8]1DDD[0][19]DDD1DD[0]D1[11]DD[0]DDD1DDD1[1]111[4]1DDD1DDD1D[10][4]1[4]1[4][8]1DDD1D[17]DD[0][2]DD[0]DDD1DDD1[6]111[4]1[13]D[6]DD1[16]1
combined for CpCqp,Cpp,CpCNpq,CCNppp, which can be written via
$ ./findCompactSummary data/w2-tmp.txt CpCqp,Cpp,CpCNpq,CCNppp
as
$ ./pmGenerator --transform data/w2.txt -f -n -t CpCqp,Cpp,CpCNpq,CCNppp -j -1
-s CpCCNqCCNrsCNqCCNCCNtCCNuvNpCutwNCxCCyCxzCCNzCCNabyCazCrq,CpCqCrCsCtq,CpCqCrp
CpCCqCprCCNrCCNstqCsr = 1
[0] CpCCNqCCNrsCNqCCNCCNtCCNuvNpCutwNCxCCyCxzCCNzCCNabyCazCrq = DDDDD111111
[1] Cpp = DDD11DDD11D11[0][0]
[2] CpCqCrCsCtq = DDDDD1DDD11DD1D111[0]1[0]11
[3] CpCqp = DDD1D[2]1D111
[4] CpCNpq = DDDDD1D111[0]DDD11DDD1D111[0][0]1
[5] CpCqCrp = DDD11DD11DDD1D111[0][2]
[6] CCNppp =
DDDDD1[1]1DDDD11DDD1[5]D11DDD11DDD1D111[0]1DDD1DDDD11D1DD1DDD1[0]D1111[0]DDD11D1[0][0]DDD1D1D[2]11[0]DDDDD11111[0]1DDDD11[5]DDD1DDD11D1DDD11DDD1D111[0]1DDD11DDD1DDD1DD1D111111[0]1DDD1DDD1DDD1DDD1[0]D1111[0]1[0]1[0]DDDDD11111[0]1DDD1DDDDD1D111[0]DDD11DDD1D111[0][0]DDD11DDD1111DDD11DDD1DDD1DDD11D11[0]111[0]1D1[1]DDDD11D11[0]DD1[3]1
in a more compact way.
Could you post your solution (and what you did, if you like) as a new answer in
https://github.com/xamidi/pmGenerator/discussions/2?
Thank you for your contribution. :-)
________________________________
Von: [email protected] <[email protected]> im Auftrag von Gino
Giotto <[email protected]>
Gesendet: Donnerstag, 13. Juni 2024 19:39:30
An: Metamath
Betreff: Re: [Metamath] Re: Shortest possible axiom for propositional calculus
I think I found a shorter proof of Łukasiewicz's second axiom (L2) from
Walsh's second axiom (w2):
Statement of L2: CCNppp
My proof of L2:
DDDDD1DDD11DDD11D11DDDDD111111DDDDD1111111DDDD11DDD1DDD11DD11DDD1D111DDDDD111111DDDDD1DDD11DD1D111DDDDD1111111DDDDD11111111D11DDD11DDD1D111DDDDD1111111DDD1DDDD11D1DD1DDD1DDDDD111111D1111DDDDD111111DDD11D1DDDDD111111DDDDD111111DDD1D1DDDDDD1DDD11DD1D111DDDDD1111111DDDDD1111111111DDDDD111111DDDDD11111111DDD1DDDDD1D111DDDDD111111DDD11DDD1D111DDDDD111111DDDDD111111DDD11DDD1111DDD11DDD1DDD1DDD11D11DDDDD111111111DDDDD1111111D1DDD11DDD11D11DDDDD111111DDDDD111111DDDD11D11DDDDD111111DD1DDD1DDDDDD1DDD11DD1D111DDDDD1111111DDDDD111111111D1111
I verified this finding with the command:
pmGenerator -c -n -s CpCCqCprCCNrCCNstqCsr --parse
DDDDD1DDD11DDD11D11DDDDD111111DDDDD1111111DDDD11DDD1DDD11DD11DDD1D111DDDDD111111DDDDD1DDD11DD1D111DDDDD1111111DDDDD11111111D11DDD11DDD1D111DDDDD1111111DDD1DDDD11D1DD1DDD1DDDDD111111D1111DDDDD111111DDD11D1DDDDD111111DDDDD111111DDD1D1DDDDDD1DDD11DD1D111DDDDD1111111DDDDD1111111111DDDDD111111DDDDD11111111DDD1DDDDD1D111DDDDD111111DDD11DDD1D111DDDDD111111DDDDD111111DDD11DDD1111DDD11DDD1DDD1DDD11D11DDDDD111111111DDDDD1111111D1DDD11DDD11D11DDDDD111111DDDDD111111DDDD11D11DDDDD111111DD1DDD1DDDDDD1DDD11DD1D111DDDDD1111111DDDDD111111111D1111
-b -n -o L2.txt
Which generates a text file called "L2.txt" containing the output string: "1.
CCNppp"
If I understand correctly, the output string should be the statement generated
by the provided proof, written in Polish notation. The table on
https://github.com/xamidi/pmGenerator/discussions/2 reports that the shortest
known proof of L2 from w2 is 781 steps long, while my proof is 535 steps long,
so, if everything checks out, mine would be shorter.
@xamidi Does this seem correct to you?
The difficulty of Walsh's second axiom (w2) is rated as "horrible - 10/10" on
pmGenerator Github page, so this would be a nice result :-)
Il giorno sabato 8 giugno 2024 alle 12:17:41 UTC+2 Gino Giotto ha scritto:
> I'll took some care
*I'll take*
Il giorno sabato 8 giugno 2024 alle 11:43:16 UTC+2 Gino Giotto ha scritto:
> Estimated from w5's data
> table<https://xamidi.github.io/pmGenerator/README.html#walshs-5th-axiom-1-basis-ccpqcccrcstcqcnsnpcps-top1000-cardinalities-sample-info>,
> you would have to generate files with a combined size of around 404054704152
> * 2.37^((63-55)/2) bytes, which are approx. 12.75 TB in order to cover all
> proofs up to lenght 63, which would ensure the 65-step proof is minimal.
Nope, ok, definitely I should have looked at those data in the first place (you
have a nice detailed documentation btw). I'll took some care to look at what
seems promising. At the moment, this is really just an excuse to get a better
hand at pmGenerator options and functionalities (basically the same thing I did
for metamath).
Il giorno sabato 8 giugno 2024 alle 08:43:08 UTC+2 [email protected]
ha scritto:
> I could confirm that the current known proof is the shortest possible
Finding a shorter proof may still be possible if you're lucky, but proving it
to be minimal is very unlikely, unless you have massive amounts of resources at
your hands:
Estimated from w5's data
table<https://xamidi.github.io/pmGenerator/README.html#walshs-5th-axiom-1-basis-ccpqcccrcstcqcnsnpcps-top1000-cardinalities-sample-info>,
you would have to generate files with a combined size of around 404054704152 *
2.37^((63-55)/2) bytes, which are approx. 12.75 TB in order to cover all proofs
up to lenght 63, which would ensure the 65-step proof is minimal.
Moreover, the final step alone would require pmGenerator around
2173.65*(2173.65 / 759.14)^4 ≈ 146103.49 core-h (i.e. around 16.67 years
CPU-time) and 759.14*(759.14/320.89)^4 ≈ 23778.51 GiB of RAM, assuming that the
exponential growth factors do not increase (which they probably do, so it most
likely is even worse).
As you can see from w5's behavioral
graph<https://xamidi.github.io/pmGenerator/svg/plot/w5-bgraph.svg>, most
formulas quickly generated in w5 are insanely long, but this leads to making
filtering really easy, which led to the short proofs of w5 at
https://github.com/xamidi/pmGenerator/discussions/2#challenge-proofs without
too much effort. This also means that w5's conclusions seem to be nicely
distributed over the whole range of formulas. But since its known proofs are so
small already, you have to be lucky to still find improvements, and minimal
proofs might use very long formulas. So I'm not sure w5 is a good choice.
Regardless of what you'll choose in the end, I wish you good luck and much
success!
[email protected] schrieb am Samstag, 8. Juni 2024 um 03:29:28 UTC+2:
> I am looking forward to your findings. Which system(s) are you looking into?
For now I'll keep doing something simple, just to get more confidence with the
tool. In the discussion https://github.com/xamidi/pmGenerator/discussions/2 I
read that it should be easy to handle Walsh's fift axiom
https://xamidi.github.io/pmGenerator/svg/walsh5th.svg, so I think I'll try to
minimize the proof of "id" from it (since I also read that you exhausted the
search up to 55 steps, but the shortest proof that you know of id is 65 steps,
this means that even if I don't find anything, I could confirm that the current
known proof is the shortest possible, which is interesting information).
My computer is relatively mediocre, but it's not the first time I stress it to
do long running math related computations (like minimizing
set.mm<http://set.mm> proofs, reducing
axioms in set.mm<http://set.mm> or excluding a composite number in GIMPS
https://www.mersenne.org/).
> Ok, I might now understand what Gino was about. This is a great
> clarification!
It was helpful for me as well to understand what Wolfram really meant.
Il giorno sabato 8 giugno 2024 alle 00:21:46 UTC+2 [email protected]
ha scritto:
> but instead allowed
> resolution<https://en.wikipedia.org/wiki/Resolution_(logic)> to occur
Oops, resolution and paramodulation, as noted on Otter's wiki
article<https://en.wikipedia.org/wiki/Otter_(theorem_prover)>.
> The axiomatization I provided, based on wolfram's axiom, is complete for
> Boolean algebra already. [...] To be clear, this axiom system will not be
> able to prove all theorems in propositional logic: it is quite obviously
> restricted to theorems of the form |- ( ph <-> ps ) [...]
Ok, I might now understand what Gino was about. This is a great clarification!
I'd like to add that as long as the operators of a system are functionally
complete and it proves all theorems over those formulas, the system implicitly
proves all theorems in propositional logic, which can be taken as aliases, just
like pmproofs.txt<https://us.metamath.org/mmsolitaire/pmproofs.txt> does it —
e.g. to prove *1.2:"((P v P) -> P)", one actually proves "((~ P -> P) -> P)".
For Boolean algebra over {⊼}, this could be solved by using something like
x⊼(x⊼x)=f(ψ) as an alias for each propositional formula ψ, where f converts any
propositional formula over any desired operators into a corresponding formula
in terms of ⊼, e.g. f(⊤)= x⊼(x⊼x), f(a∨b)=(a⊼a)⊼(b⊼b), etc.
Metamath avoids implicit aliases by using "definitions" which are in fact
axioms, since they introduce further symbols into the object language for
convenience. Minimalistic deductive systems do not do this.
> By the way, this is unrelated, but I know you are the person that created
> https://github.com/xamidi/pmGenerator/tree/1.2.0 [...]
I should probably also note that version 1.2.0 was released 3 months ago, and
https://github.com/xamidi/pmGenerator links to the current version (e.g. I
recently added some nice graphical overviews to the readme file).
[email protected] schrieb am Freitag, 7. Juni 2024 um 23:12:54 UTC+2:
On Fri, Jun 7, 2024 at 6:07 PM Discher, Samiro <[email protected]>
wrote:
If you are asking for technical details, sorry but I do not care enough about
"Boolean algebra" to work these out. I think it is a complicated mess that has
no pure logical character whatsoever (which is also why I think we would need
several rules only to encode what "=" does). In particular, I think it is very
hard and may even be impossible to provide an "elegant" axiomatization that
doesn't need to combine a bunch of rules for what in Boolean algebra is
considered a single step.
The axiomatization I provided, based on wolfram's axiom, is complete for
Boolean algebra already. That's exactly the point. I think you can be slightly
more minimalistic and use euc instead of trans, as follows:
${ euc.1 $e |- p = q $. euc.2 $e |- p = r $.
euc $a |- q = r $. $}
${ naeq.1 $e |- p = q $. naeq.2 $e |- r = s $.
naeq $a |- ( p r ) = ( q s ) $. $}
ax $a |- ( ( ( p q ) r ) ( p ( ( p r ) p ) ) ) = r $.
refl $p |- p = p $=
( tna ax euc ) AABABZAEBBAAAAACZFD $.
${ symm.1 $e |- p = q $.
symm $p |- q = p $=
( refl euc ) ABACADE $. $}
${ trans.1 $e |- p = q $. trans.2 $e |- q = r $.
trans $p |- p = r $=
( symm euc ) BACABDFEG $. $}
What it means to be "complete for boolean algebra" here is that metamath can
prove |- ( ph <-> ps ) iff the above axiomatization can prove |- p = q, where p
and q are the encodings of ph and ps as NAND formulas respectively.
> Can you tell me how would you formalize Wolfram's axiom in Metamath without
> equality? (So that I can be sure we are on the same page).
"<->" / "=" is an equivalence relation, so reflexivity, transitivity and
symmetry of it must be covered by rules.
(https://en.wikipedia.org/wiki/Equivalence_relation#Definition)
Essentially, I would look at what Wolfram's system is able to do and introduce
rules until they (in combination) can do everything that is required.
Then also provide the axiom, and you're done.
I understood Mario's approach as doing just that, except that he provided a
fundamental axiomatization, not one merely proven on top of another system
(like set.mm<http://set.mm>).
The most natural way to do this in set.mm<http://set.mm> would be to simply
take the equivalents of the above axioms as pseudo-axioms in a section, namely
{bicomi,bitri} | bitr3i, nanbi12i, and wolfram (i.e. the axiom you get by
transcribing 'ax' above using wnan and wbi).
To be clear, this axiom system will not be able to prove all theorems in
propositional logic: it is quite obviously restricted to theorems of the form
|- ( ph <-> ps ), and it is also language-restricted to only use formulas in
terms of NAND unless you add some definitions. But we would say that
propositional logic is a conservative extension of equational boolean algebra,
since all the theorems in the image of the translation are provable iff they
are provable in the equational logic.
If you wanted to stick something minimal on top of this system to make it
complete for propositional logic, I would suggest adding some definitions to
the source language:
* !p = p | p
* p /\ q = !(p | q)
* p -> q = p | !q
* p \/ q = !p -> q
* 1 = p \/ !p
and then using the inference rule |- ( ph <-> T. ) ==> |- ph to allow
interpreting proofs of the form |- p = 1 as playing the role of |- p (which is
not otherwise well formed in equational logic). You can also add the following
definition:
* (p <-> q) = (p -> q) /\ (q -> p)
but then you will want to prove |- (p <-> q) = 1 <==> |- p = q to ensure
conservativity (since the translation makes <-> and = the same thing and thus
implicitly implies that these two are equivalent).
________________________________
Von: [email protected] <[email protected]> im Auftrag von Gino
Giotto <[email protected]>
Gesendet: Freitag, 7. Juni 2024 17:51:14
An: Metamath
Betreff: Re: [Metamath] Re: Shortest possible axiom for propositional calculus
Can you tell me how would you formalize Wolfram's axiom in Metamath without
equality? (So that I can be sure we are on the same page).
Il giorno venerdì 7 giugno 2024 alle 17:15:25 UTC+2 [email protected]
ha scritto:
> Note that simply replacing the "=" with "<->" will lead you to an incomplete
> system, because you have no way to derive a propositional statement where the
> "<->" is not present.
Using "<->" was what I proposed. I cannot follow your statement. When you have
multiple rules that can do everything that is semantically defined by Boolean
algebra, you sure can derive everything that semantically follows. The question
is, why you wouldn't be able to define the required rules in Metamath (and
prove them in set.mm<http://set.mm> based on only propositional primitives).
> the axioms in Mario's formalization would not provide all properties that you
> need to know the full behaviour of the classical biconditional operator
Which in set.mm<http://set.mm> is meaningless. All you need is to derive
whichever rules are required (in Metamath such is called "Theorem" with an
"Hypothesis"), but based on ax-1, ax-2, ax-3, ax-mp, df-bi, and df-nan (which
includes df-an). How can this not be possible? If it is not, there must be a
lack of expressiveness in the Metamath language, or Wolfram's "=" must do
something that is not true for "<->". Since the propositional calculus is
complete.
________________________________
Von: [email protected] <[email protected]> im Auftrag von Gino
Giotto <[email protected]>
Gesendet: Freitag, 7. Juni 2024 16:53:19
An: Metamath
Betreff: Re: [Metamath] Re: Shortest possible axiom for propositional calculus
> Why not? What features are used by Wolfram's rules that cannot be described
> in Metamath language? Shouldn't propositional logic alone suffice (as I
> mentioned earlier), let alone ZFC?
I am referring to the chapter called "Other axiomatizations related to
classical propositional calculus", which appears before the properties about
equality (and set theory) are introduced. To formalize Wolfram's system into
that chapter, you have to find a way to eliminate/translate the equality
inference rules (which I don't think it's possible).
Note that simply replacing the "=" with "<->" will lead you to an incomplete
system, because you have no way to derive a propositional statement where the
"<->" is not present. The tautology "|- ( ph -/\ ( ph -/\ ( ph -/\ ( ph -/\
ph ) ) ) )" is not derivable for example. However, if you keep the "=" as a
foreign symbol from classical propositional calculus then you can derive an
equivalent formulation as "|- ( ph -/\ ( ph -/\ ( ph -/\ ( ph -/\ ph ) ) ) )
= T." ("true" can be defined in terms of NAND).
you might say that replacing "=" with "<->" would allow to derive "|- ( ph
-/\ ( ph -/\ ( ph -/\ ( ph -/\ ph ) ) ) ) <-> T." anyway, but the axioms in
Mario's formalization would not provide all properties that you need to know
the full behaviour of the classical biconditional operator.
In Wolfram's system the biconditional can be added with a conservative
definition "|- ( ph <-> ps ) = ( ( ( ph -/\ ph ) -/\ ( ps -/\ ps ) ) -/\ ( ph
-/\ ps ) )" and statements like "|- ( ps <-> ph ) = ( ph <-> ps )" are
derivable without issues. But what happens if I add a definition of
biconditional when the symbol "<->" was already used in the system? Then I can
now rewrite any biconditional into NAND operations, and eventually derive
expressions that do not contain any biconditional. This was impossible before,
therefore I didn't add a definition, I added an axiom, so my original axiomatic
system was not sufficient to properly describe classical propositional calculus.
Il giorno venerdì 7 giugno 2024 alle 10:21:14 UTC+2 [email protected]
ha scritto:
> So, we can't even formalize it in set.mm<http://set.mm> chapter about
> alternative axiom systems for propositional calculus at all.
Why not? What features are used by Wolfram's rules that cannot be described in
Metamath language? Shouldn't propositional logic alone suffice (as I mentioned
earlier), let alone ZFC?
[email protected] schrieb am Freitag, 7. Juni 2024 um 02:19:20 UTC+2:
I could not have wished for a better answer. He does actually assume inferences
about equality. So, we can't even formalize it in set.mm<http://set.mm> chapter
about alternative axiom systems for propositional calculus at all.
Il giorno venerdì 7 giugno 2024 alle 00:54:27 UTC+2 [email protected] ha scritto:
On Thu, Jun 6, 2024 at 11:07 AM Gino Giotto <[email protected]> wrote:
So this is the linked single NAND axiom for propositional calculus by Stephen
Wolfram:
((p·q)·r)·(p·((p·r)·p))=r
My question is: how would this translate into Metamath?
To answer this question directly, here's a metamath axiomatization of wolfram's
axiom system and a proof of step 1:
$c term wff |- = ( ) $.
$v p q r s ph $.
tp $f term p $.
tq $f term q $.
tr $f term r $.
ts $f term s $.
wph $f wff ph $.
weq $a wff p = q $. $( equality $)
tna $a term ( p q ) $. $( nand $)
${ symm.1 $e |- p = q $.
symm $a |- q = p $. $}
${ trans.1 $e |- p = q $. trans.2 $e |- q = r $.
trans $a |- p = r $. $}
${ naeq.1 $e |- p = q $. naeq.2 $e |- r = s $.
naeq $a |- ( p r ) = ( q s ) $. $}
ax $a |- ( ( ( p q ) r ) ( p ( ( p r ) p ) ) ) = r $.
refl $p |- p = p $=
( tna ax symm trans ) AAABABZAFBBZAGAAAACZDHE $.
step1 $p |- ( p ( ( p q ) p ) ) = ( q ( ( p r ) ( ( ( p r ) ( p ( ( p q ) p ) )
) ( p r ) ) ) ) $=
( tna ax symm refl naeq trans ) AABDADDZACDZBDJDZKKJDKDDZDZBMDNJKBJEFLBMMACBE
MGHI $.
--
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 [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/fdfa1b17-a73c-41e7-b857-9af877a638c9n%40googlegroups.com<https://groups.google.com/d/msgid/metamath/fdfa1b17-a73c-41e7-b857-9af877a638c9n%40googlegroups.com?utm_medium=email&utm_source=footer>.
--
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 [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/56b4641b-2f9a-4786-a04f-d5ec0d63f137n%40googlegroups.com<https://groups.google.com/d/msgid/metamath/56b4641b-2f9a-4786-a04f-d5ec0d63f137n%40googlegroups.com?utm_medium=email&utm_source=footer>.
--
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 [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/e754e9f197134a08b7b74774cd8173f4%40rwth-aachen.de<https://groups.google.com/d/msgid/metamath/e754e9f197134a08b7b74774cd8173f4%40rwth-aachen.de?utm_medium=email&utm_source=footer>.
--
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
[email protected]<mailto:[email protected]>.
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/b61d2655-3593-4c33-85a8-036d1239e3c1n%40googlegroups.com<https://groups.google.com/d/msgid/metamath/b61d2655-3593-4c33-85a8-036d1239e3c1n%40googlegroups.com?utm_medium=email&utm_source=footer>.
--
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 [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/3822401fd1844635a3b5a228702092ab%40rwth-aachen.de.
