Has it been proved that ∨ ∧ ¬ ⇒ ⇔ ∀ ∃ and predicates are enough to express all known mathematics?

Question

I frequently encounter this statement in math books: "All of known mathematics can be expressed in terms of elementary predicates, logical connectives, and quantifiers."

Answer 1

You need a concept of proof that is

• sound in the sense that anything that's provable from a given set of hypotheses is true in every model in which the hypotheses are true, and
• effective, in the sense that there is a proof-checking algorithm.

It would also be nice for it to be

• complete in the sense that every proposision true in every model in which the hypotheses are true can be proved from those hypotheses.

That the logic based on the symbols you list satisfies the three bullet points was proved in the 1930s, provided you allow Gödel's non-constructive proof of the third point.

The second point raises the question: What is an algorithm. The answer is that it is that which can be done by your favorite general-purpose progamming language. For any two such languages, any algorithm in one of them can be written in the other: this has been checked carefully and extensively.

Could there be something that we would recognize as an algorithm that cannot be expressed in those languages? That is a maddening question. I don't think anyone knows how to make it precise. But if such a thing were found, it would not be currently known math. The proposition that there can be no such thing is the Church–Turing thesis.

The theory of sets is expressed using the symbols you list, and sometimes it is asserted that all known mathematics can be encoded within that (and sometimes it is asserted that not all of it can).