PA theorem provers aren’t reflective philosophical agents that can answer questions like “what is the origin of my axioms?”
To psychologize them to the point that they “have beliefs” or “make claims” is to interpret them according to a normative/functional theory of mind, such that it is conceivable that the prover could be broken.
A philosophical mathematician using a PA theorem prover uses a wide variety of oughts in ensuring that the theorem prover’s claims are trustworthy:
The prover’s axioms ought to correspond to the official PA axioms from a trustworthy source such as a textbook.
The prover ought to only prove valid theorems; it must not have bugs.
The programmer ought to reason about and test the code.
The user ought to learn and understand the mathematical notation and enter well-formed propositions.
Etc etc. Failure to adhere to these oughts undermines justification for the theorem prover’s claims.
PA theorem provers aren’t reflective philosophical agents that can answer questions like “what is the origin of my axioms?”
To psychologize them to the point that they “have beliefs” or “make claims” is to interpret them according to a normative/functional theory of mind, such that it is conceivable that the prover could be broken.
A philosophical mathematician using a PA theorem prover uses a wide variety of oughts in ensuring that the theorem prover’s claims are trustworthy:
The prover’s axioms ought to correspond to the official PA axioms from a trustworthy source such as a textbook.
The prover ought to only prove valid theorems; it must not have bugs.
The programmer ought to reason about and test the code.
The user ought to learn and understand the mathematical notation and enter well-formed propositions.
Etc etc. Failure to adhere to these oughts undermines justification for the theorem prover’s claims.