Founding mathematics from a set of axioms.

foundationslogicpredicate-logic

Is it possible in principle to justify all of mathematical knowledge and theorems and every deduction step taken in any of those theorems by a set of axioms ? And if the answer is yes what is that set of axioms ?

When I say every deduction step I mean that even something elementary like the validity of using truth tables must be justified and the assertion that two statements are equivalent if they have the same truth values also must be justified.

I'm interested in the minimum set of axioms that achieve that.

And if that is not possible, then how can we be sure that mathematics is objectively true ? true in the sense that we are not making it up !

Best Answer

There are several different sub-questions here, and I'll try to provide enough to address each of them to some degree, but I may not capture the aspects yousef magableh is most interested in.

All mathematical knowledge

This part is a bit of a problem, because different people may disagree as to which knowledge counts as "mathematical". I'm going to treat this as "the vast majority of mathematical knowledge" as I think that's a bit more approachable.

What axioms?

"Axiom" has a couple of closely related definitions and I don't really want to get into the details/distinctions, so I'm interpreting this very broadly as something like "what are all the foundations you need to be very rigorous?"

There are many possible choices, but working downwards, one sort of foundation would require:

  • All the definitions of complicated things in terms of simpler things (e.g. real numbers in terms of rationals, triangles in terms of line segments, maybe pairs in terms of sets, etc.)
  • All the basic properties of the simplest things. It's common to choose a variant of the standard set theory ZF, such as "ZFC" (ZF+the axiom of choice) or "TG" (ZFC+Grothendieck universes)
  • A logical framework in which to phrase propositions about those simplest things, such as standard first-order logic.
  • Something like deduction rules for that logical framework so you can reason about things. For example, a version of natural deduction or a Hilbert-style system.
  • Ideally, something like a formal grammar specifying exactly how statements/variables/whatever can be written in the first place. For example, is "$\land\to\lor ppq$" legal to write? If the deduction rules are going to discuss variable substitution, how does that work precisely? etc.

All of these requirements are met in various ways in things like automated formal proof checkers. For example, at the Metamath Proof Explorer you can see all the steps in derivations of various mathematical facts (including steps like "is this string even valid to write?" if you download the database and metamath program instead of just viewing things on the website). In that example, the lowest level is the Metamath language which basically describes a formal means to stitch together verbatim string substitutions into variables. Then there are "axioms" about how variables and symbols like $\in$ and $\land$ are used, "axioms" for propositional logic, "axioms" for quantifiers, "axioms" for TG set theory, and "axioms" for more complicated definitions like $\subseteq$ and $\mathbb R$.

I personally think using computers (ideally with systems like Metamath that have independent implementations written in different languages) is our best way to get close to objective truth.

Not making it up?

All of our logical systems are made up. And as mentioned in the comments, things like Gödel's incompleteness theorems mean we can't even be sure that we won't ever reach a contradiction with our favorite standard approach to the foundations.

Validity of truth tables

Separate from the rest of the discussion, (my interpretation of) this particular fact is the (soundness and) completeness of Propositional Logic. This has been proved in a number of logic textbooks, and checked carefully by a computer. For example, see Formalising the Completeness Theorem of Classical Propositional Logic in Agda (Proof Pearl) by Leran Cai, Ambrus Kaposi, and Thorsten Altenkirch.

equivalent if…same truth values

I don't know for sure that I understand what you mean by this, but I have an idea about how it might be spelled out. If you have something like $p\lor q$ and $q\lor p$, then they are logically/semantically equivalent because they have the same truth value no matter the assignment of truth values to $p$ and $q$. However, it's also the case that $(p\lor q)\leftrightarrow(q\lor p)$ is a tautology (equivalently by the soundness/completeness I mentioned above, that it's a theorem). With standard logic(s), these concepts indeed coincide. I don't have an ideal source, but Carl Mummert basically mentions this in this MSE answer.

minimum set of axioms

This is a bit tricky because "axiom" is used in a few slightly different ways, and often you can do something like connect a big list of axioms together into a single axiom with "$\land$". That said, one notable fact you may be interested in is that you can get all of propositional logic in a Hilbert System with just modus ponens as the rule of inference and Meredith's axiom $\left(\left(\left(\left(A\to B\right)\to\left(\neg C\to\neg D\right)\right)\to C\right)\to E\right)\to\left(\left(E\to A\right)\to\left(D\to A\right)\right)$.

Related Question