> 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). >> > > The most natural way to do this in 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 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 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 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 >>>>> 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]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/0d314075-2483-4d24-8f4e-975910d6ad06n%40googlegroups.com.
