2
$\begingroup$

There are several axioms that are known to be independent of the usual ones; for instance, the Axiom of Choice. This axiom can be stated in several equivalent ways, e.g.:

  • For every set $A$, $\mathcal{P}(A) \setminus \{\emptyset\}$ has a choice function.
  • For every infinite set $A$, there is a bijective map between the sets $A$ and $A \times A$.
  • Every surjective function has a right inverse.
  • All sets have a cardinality, which has a strict total order.

There are several different fundamental axioms you can pick for a proof system. No matter what you pick, if your selection is powerful enough to be useful, you can derive the "axioms" that a different proof system uses from your axioms.

Given how axioms can be defined in terms of each other, and some sets of axioms are independent of others, it feels like you can describe the relationships between axioms using the language of graph theory, and from there you could explore minimal independent sets of axioms. I imagine there are certain properties that all sets of axioms share; I might have found one or two, but I have no idea how to go about investigating further.

I imagine somebody's already studied this, but I have no idea what they might have called it. What is known about this already?

Improve this question
$\endgroup$
13
  • 1
    $\begingroup$ Are you looking for reverse mathematics? $\endgroup$
    – Josh
    Feb 22, 2022 at 16:51
  • $\begingroup$ They're doing it completely differently to how I thought they would, but yes, that looks like what I'm talking about. $\endgroup$
    – wizzwizz4
    Feb 22, 2022 at 16:55
  • 3
    $\begingroup$ I'm voting to close since this does not pertain PAs, but it is a (valid) mathematical logic question, more suitable for MO or math.SE $\endgroup$
    – Pedro Sánchez Terraf
    Feb 22, 2022 at 18:33
  • 1
    $\begingroup$ As an argument that this should be on-topic, the question is relevant to designing small kernels and axiomatic systems, and doesn't really have many other applications outside of that. $\endgroup$
    – wizzwizz4
    Feb 22, 2022 at 23:20
  • 2
    $\begingroup$ The question could be reopened if it explained why having small sets of axioms is supposed to be good for proof assistants. Is it really? Even better would be something along the lines: in logic minimal systems of axioms are valued because they easy meta-logical analysis of a theory, how important is minimality/independence of axioms for proof assistants? As the question stands, it's just about logic and nothing else. $\endgroup$
    – Andrej Bauer
    Feb 23, 2022 at 15:49

2 Answers 2

Reset to default
7
$\begingroup$

From the point of view of the proof assistants, Metamath is an interesting tool for studying minimal sets of axioms.

In the set.mm database, classical propositional calculus is developed from the 4 axioms of Łukasiewicz, and then, several other equivalent axiomatizations are presented, as well as derivations between them.

Using a Metamath function which lists the axioms from which a theorem has been proved, it is possible to show that such derivations are only based on a given set of axioms. This is also interesting if one wants to find out whether the axiom of choice is required for a given proof.

One might also consider the intuitionistic logic: in iset.mm set theory is developed without the law of excluded middle; yet another axiomatisation.

Improve this answer
$\endgroup$
1
  • $\begingroup$ Maybe also of interest, a recent article of Benoît Jubin proving the independence of some finite axiom-schematization of classical first-order logic: https://arxiv.org/abs/2202.10383 $\endgroup$
    – Thierry Arnoux
    Feb 23, 2022 at 11:22
2
$\begingroup$

For set theory, I refer you to mathoverflow, there is a similar question.

For reverse mathematics, I point you to Reverse Mathematics Zoo.

Improve this answer
$\endgroup$
5
  • $\begingroup$ I'm downvoting because I want to discourage the answering of off-topic questions. If there is any way to put something about PAs in the answer, that would be and improvement $\endgroup$
    – Pedro Sánchez Terraf
    Feb 22, 2022 at 18:34
  • $\begingroup$ @PedroSánchezTerraf You can see Reverse Mathematics Zoo as a proof assistant. $\endgroup$
    – M. Lonardi
    Feb 22, 2022 at 18:38
  • $\begingroup$ Is it? I'm checking the Usage page and it doesn't look like a “general purpose” PA, but perhaps it is just that the docs are incomplete or I fail to understand that they are describing that. $\endgroup$
    – Pedro Sánchez Terraf
    Feb 22, 2022 at 18:50
  • $\begingroup$ @PedroSánchezTerraf Oh no, RM Zoo is not general purpose, however it is still a proof assistant (sui generis and sensu lato). $\endgroup$
    – M. Lonardi
    Feb 22, 2022 at 20:06
  • $\begingroup$ I'll will reconsider if the question is kept open! $\endgroup$
    – Pedro Sánchez Terraf
    Feb 22, 2022 at 21:38

Not the answer you're looking for? Browse other questions tagged or ask your own question.