You are using an outdated 18th century layman definition for the term "axiom".
In an automated theorem prover, there are input statements that construct the problem universe and which are called "axioms". There are output statements of which you want to prove that they necessarily and logically follow from the axioms, and which are called "conjectures" or "theorems".
There is no need for agreeing on the truth of axioms.
The theorem prover does not prove their truth. It does not seek to do that. The theorem prover only proves that a theorem necessarily follow from the axioms:
When a1, a2, a3, ..., a[k] are the axioms and c1 is the conjecture, then the theorem prover does not prove that a1, a2, a3, ..., a[k] are true. The theorem prover also does not prove that c1 is true. The theorem prover only proves the following:https://tptp.org/UserDocs/TPTPLanguage/ ... uage.shtml
The TPTP Language
Annotated Formulae
TPTP problems and TSTP solutions are built from annotated formulae of the form language(name,role,formula,source,[useful_info]).. The languages currently supported are thf - formulae in typed higher-order form, tff - formulae in typed first-order form (including extended form), fof - formulae in first order form, and cnf - formulae in clause normal form. The name identifies the formula within the problem. The role gives the user semantics of the formula, one of axiom, hypothesis, definition, assumption, lemma, theorem, corollary, conjecture, negated_conjecture, plain, type, interpretation, logic, and unknown.
The axiom-like formulae are those with the roles axiom, hypothesis, definition, assumption, lemma, theorem, and corollary. They are accepted, without proof, as a basis for proving conjectures in THF, TFF, and FOF problems. In CNF problems the axiom-like formulae are accepted as part of the set whose satisfiability has to be established. There is no guarantee that the axiom-like formulae of a problem are consistent.
a1, a2, a3, ..., a[k] ⊢ c1
The theorem prover only proves that c1 necessarily follows from a1, a2, a3, ..., a[k].
In general, mathematics never proves A. Mathematics never proves B. Mathematics only proves:
A ⊢ B
A is called a "theory". B is called a "theorem".
You can prove a "theorem" from a "theory". You can never prove the "theory" itself. You can also never prove a "theorem" without "theory".
In other words, context-free truth does not exist.
Furthermore, there is never proof for the context itself. Therefore, you do not need to agree on the context. You only need to establish that a particular truth necessarily follows from a particular context.
If you want to understand the notion of truth in mathematics, read up on Tarski's semantic theory of truth:
The truth certainly exists but it may not be what you think it is.https://en.m.wikipedia.org/wiki/Semanti ... y_of_truth
A semantic theory of truth is a theory of truth in the philosophy of language which holds that truth is a property of sentences.[1]
The semantic conception of truth, which is related in different ways to both the correspondence and deflationary conceptions, is due to work by Polish logician Alfred Tarski. Tarski, in "On the Concept of Truth in Formal Languages" (1935), attempted to formulate a new theory of truth in order to resolve the liar paradox. In the course of this he made several metamathematical discoveries, most notably Tarski's undefinability theorem using the same formal technique Kurt Gödel used in his incompleteness theorems. Roughly, this states that a truth-predicate satisfying Convention T for the sentences of a given language cannot be defined within that language.