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
<http://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 <http://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.
