Founding mathematics from a set of axioms.

Solution 1:

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)$.

Solution 2:

Some of your questions are best asked of philosophers of mathematics, in particular the basis of mathematical reasoning.

A cop-out answer to your question about axioms that give all of mathematics is simply "the set of all true (mathematical) statements". But there are two issues with this. Firstly, what kind of statements are we making? And secondly, how do we know whether something is actually true, and thus a part of this? The first question can't be so general as "English" (as you run into trouble with paradoxes and contradictions), but it needs to be general enough to encompass all the statements of group theory, number theory, differential equations, and so on. The second question is a bit more complicated, and the end result is that we can't. What this means is that we won't be able to both ensure that we can tell is/isn't an axiom, and ensure that everything actually true can be proven.

A first attempt: just logic. Issue: this gives almost nothing.

If we look just at first order logic, we can informally show that certain proof systems give us everything in the sense that a theory $T$ proves a formula $\varphi$ (written $T\vdash\varphi$) iff $T$ logically implies $\varphi$ (written $T\models\varphi$). Ostensibly, we could then just found all of mathematics on $T=\emptyset$, since it would say that $\varphi$ is true iff it is provable. The issue is that $\emptyset\vdash\varphi$ iff $\varphi$ is always true, so it doesn't tell us whether $\varphi$ is actually true or not. For example, "there are two things" being $\exists x\exists y(x\not = y)$ wouldn't be, since it's conceivable for there to be only one thing. Hence we can't even think about common mathematical objects with just this framework, like the natural numbers. To go further than just validity, we need to make use of some axioms, as you indicate.

A second attempt: some axioms. Issue: it's incomplete or else unintelligible.

Right now this is the best we can do, and in the end you'd arrive at some sort of foundational system like (the most popular) set theory in the form of $\mathsf{ZFC}$. But regardless of what theory $T$ you use, if it's really going to serve as an underpinning for all of mathematics, it ought to be able to at least talk about (and be correct about) the natural numbers (that is, the structure $\textbf{N}$ of $\mathbb{N}$ with addition, multiplication, $0$, and $1$).

This is enough to envoke Gödel's first incompleteness theorem, which tell us that either we can't tell what is/isn't in $T$, or else there are formulas in the language of arithmetic that $T$ does not decide (i.e. $T\not\vdash\phi$ and $T\not\vdash\neg\phi$). Fully, Gödel's first incompleteness theorem says that there is no proof system for $\textbf{N}$ that is sound, and complete (such that it's computable whether something is a proof or not). In particular, the proof system of appealing to $T$ is incomplete.

If $T$ correctly proves all the facts about $\textbf{N}$, then clearly $T\vdash \phi$ (or some translation of $\phi$) implies $\textbf{N}\models\phi$. And the reverse easily holds since we're assuming $T$ decides every statement. In essence, $\textbf{N}\models\phi$ iff $T\vdash\phi$. But then we can consider whether an arbitrary $\phi$ is true or not just by seeing whether there is a proof of it. If membership in $T$ is computable, then it's sufficiently simple to check whether something is a proof from $T$. Hence all truth about $\textbf{N}$ collapses down to a certain level of complexity, which contradicts (loosely) that there are ever more complicated questions.

Since it's pretty easy to tell what a proof is in first-order logic, the issue of complexity falls onto the shoulders of $T$. If $T$ is too complex (where we can't write down what's actually in it), then the usefulness of $T$ as a foundation comes into question (e.g. my cop-out answer above). If we can actually write down what $T$ is, then there are number-theoretic statements which are undecidable from $T$.