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.
