It was supposed to be ⊢((((φ⊼ψ)⊼χ)⊼(φ⊼((φ⊼χ)⊼φ)))↔χ) .
Since parentheses are messy and unnecessary: In normal Polish notation
(which has no parentheses), the formula is just EDDDpqrDpDDprpr, which
could also be written in terms of {¬,→} as
¬(((((p→¬q)→¬r)→¬(p→¬((p→¬r)→¬p)))→r)→¬(r→(((p→¬q)→¬r)→¬(p→¬((p→¬r)→¬p)))))
[or NCCCCCpNqNrNCpNCCpNrNprNCrCCCpNqNrNCpNCCpNrNp in normal Polish notation]
in the way https://us.metamath.org/mmsolitaire/pmproofs.txt does it — this
time converted by my program. :-)
[email protected] schrieb am Donnerstag, 6. Juni 2024 um 16:27:28
UTC+2:
> Corrections:
>
>
> "Whichever rule(s) Stephen Wolfram's systems implicitly use [...] His
> minimal axiom written",
> "|- ( ( ( ( ph -/\ ps) -/\ ch) -/\ (ph -/\ ((ph -/\ ch) -/\ ph ) ) ) <->
> ch )",
>
> "⊢(((φ⊼ψ)⊼χ)⊼(φ⊼((φ⊼χ)⊼φ))↔χ)"
> ------------------------------
> *Von:* [email protected] <[email protected]> im Auftrag von
> Discher, Samiro <[email protected]>
> *Gesendet:* Donnerstag, 6. Juni 2024 16:18:52
> *An:* Gino Giotto; [email protected]
> *Betreff:* AW: [Metamath] Re: Shortest possible axiom for propositional
> calculus
>
> I don't like NAND-based systems because they tend to have rather
> complicated rules of inference (which doesn't make them look fundamental,
> which is the whole point of single-axiom systems).
> Whichever rule(s) Stephen Wolfram's system implicitly use(s), he didn't
> even write them down explicitly — apparently not aware that this is
> important, but possibly hiding the actual complex definition of the system.
>
> His axiom written in Metamath's language is simply
>
> |- (((ph -/\ ps) -/\ ch) -/\ (ph -/\ ((ph -/\ ch) -/\ ph))) <-> ch
>
> in ASCII tokens (https://us.metamath.org/mpeuni/mmascii.html), or
>
> ⊢((φ⊼ψ)⊼χ)⊼(φ⊼((φ⊼χ)⊼φ))↔χ
>
> in Unicode symbols.
>
> ------------------------------
> *Von:* 'Thierry Arnoux' via Metamath <[email protected]>
> *Gesendet:* Donnerstag, 6. Juni 2024 11:42:40
> *An:* [email protected]; Gino Giotto
> *Betreff:* Re: [Metamath] Re: Shortest possible axiom for propositional
> calculus
>
>
> The `=` sign here is set.mm's biconditional `<->`and we would probably
> count it as a second operation, which needs to be defined, etc.
>
> But maybe could encode it into two Metamath axioms:
>
> ${
> ax-1.1 $e |- ((p·q)·r)·(p·((p·r)·p))
> ax-1 $a |- r
> $}
> and
>
> ${
> ax-2.1 $e |- r
> ax-2 $a |- ((p·q)·r)·(p·((p·r)·p))
> $}
> _
> Thierry
>
>
> On 06/06/2024 11:06, Gino Giotto wrote:
>
> > There are propositional systems with even smaller axioms, but those
> systems are not even based on modus ponens, e.g.:
> https://writings.stephenwolfram.com/2018/11/logic-explainability-and-the-future-of-understanding/
> .
>
> 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? The set.mm
> database does not introduce the primitive "=" symbol until ax-6, so we are
> not allowed to use its properties at that stage. Given how Metamath works,
> my guess is that you'll need more than one "$a |-" statement anyway.
>
> Il Gio 6 Giu 2024, 03:32 [email protected] <
> [email protected]> ha scritto:
>
>> Meredith's axiom under https://us.metamath.org/mpeuni/meredith.html is a
>> minimal axiom (one out of seven) in the Hilbert system with operators {→,
>> ¬} and modus ponens.
>>
>> Since 2021, assuming general correctness of Walsh's and Fitelson's paper
>> <http://fitelson.org/walsh.pdf> (which is still declared as under
>> review), it has been proven by exhaustive search that it is indeed not only
>> smallest-known, but minimal.
>>
>> In contrast, https://us.metamath.org/mpeuni/merco1.html is a minimal
>> axiom in the Hilbert system with operators { →, ⊥} and modus ponens.
>>
>>
>> Such things always depend on which operators and rule(s) of inference are
>> allowed. There are propositional systems with even smaller axioms, but
>> those systems are not even based on modus ponens, e.g.:
>> https://writings.stephenwolfram.com/2018/11/logic-explainability-and-the-future-of-understanding/.
>>
>> (Note that all systems based on modus ponens must have formulas written in
>> terms of →.)
>>
>> I am researching systems of minimal axioms in terms of {→,¬} with open
>> access at https://github.com/xamidi/pmGenerator/discussions/2 in case
>> you are interested — you could even contribute to the project. On the
>> project's
>> main page <https://github.com/xamidi/pmGenerator> I also wrote a few
>> things about Metamath's propositional system of set.mm, which I called
>> "Frege's calculus simplified by Łukasiewicz" due to its origin, and I used
>> it as a default system for my tool.
>>
>>
>> [email protected] schrieb am Donnerstag, 6. Juni 2024 um 02:37:03
>> UTC+2:
>>
>>> In the discussion below, Samiro mentioned ~ retbwax1, which got me
>>> looking at
>>> ~ meredith and friends:
>>>
>>> https://groups.google.com/d/msgid/metamath/bc1cdba2626540ad8582917ddcec4d74%40rwth-aachen.de
>>>
>>>
>>> The comment in ~ meredith mentions that it's "thought to be the shortest
>>> possible axiom for propositional calculus", but then ~ merco1 and ~
>>> merco2 go
>>> on to show ones that appear shorter. Does the ~ meredith comment still
>>> apply,
>>> and if so how is length of an axiom defined in this game?
>>>
>> --
>> 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/90b6ca2b-f4d5-442e-890d-ae85bcea56e1n%40googlegroups.com
>>
>> <https://groups.google.com/d/msgid/metamath/90b6ca2b-f4d5-442e-890d-ae85bcea56e1n%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/CAPKSAW5oD62rvGSbcsL4eJHbdxiOh4GaSdf7Cqq8B8s7DFz4Vw%40mail.gmail.com
>
> <https://groups.google.com/d/msgid/metamath/CAPKSAW5oD62rvGSbcsL4eJHbdxiOh4GaSdf7Cqq8B8s7DFz4Vw%40mail.gmail.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/4f007556-4d80-4b8c-934e-01c52e43ce26%40gmx.net
>
> <https://groups.google.com/d/msgid/metamath/4f007556-4d80-4b8c-934e-01c52e43ce26%40gmx.net?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/b32870b9c8b64b5cb90ee1b3fac08a24%40rwth-aachen.de
>
> <https://groups.google.com/d/msgid/metamath/b32870b9c8b64b5cb90ee1b3fac08a24%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/8cba0cac-a0c4-4ef5-b9cc-edc14ab55c51n%40googlegroups.com.
