If your question is whether an axiom of PA can be replaced by an equivalent statement which can serve as a replacement axiom and prove the old axiom as a theorem, then the answer is yes, and in a very boring way. Every mathematical statement has tons of interchangeable equivalent forms, like adding “and 1=1” to it. Then the new version proves the old version and all that jazz.
If your question is whether we should believe in PA more because it can arise from many different sets of axioms, then I’m not sure it’s meaningful. By the previous point, of course PA can arise from tons of different sets of axioms; but also, why should we care about “believing” in PA? We care only whether PA’s axioms imply this or that theorem, and that’s an objective question independent of any belief.
If your question is whether we can have a worldview independent of any assumptions at all, the answer is that we can’t. The toy example of math shows it clearly: if you have no axioms, you can’t prove any theorems. You have latitude in choosing axioms, but you can’t dispense of them completely.
re PA: I mean a statement that we would intuitively see as non-trivially different, not merely the same statement with “and 1=1” added.
re 3: I’m not asking if we can have a worldview independent of any assumptions at all. I’m asking if we can have a worldview independent of any specific assumptions. That is, among the various sets of assumptions we can use to justify our worldview, there’s no assumption that’s common to all sets (i.e, always required to justify the worldview).
Then I guess you need to quantify “intuitively see as non-trivially different”. For example, take any axiom A in PA, and any theorem T that’s provable in PA. Then A can be replaced by a pair of axioms: 1) T, 2) “T implies A”. Is that nontrivial enough? And there’s an unlimited amount of obfuscatory tricks like that, which can be applied in sequence. Enough to confuse your intuition when you’re looking at the final result.
No, I’m not talking about obfuscatory tricks of this sort. If you could replace A with T without also adding “T implies A” as an axiom, and still be able to prove A (an everything else you could have proved before, and nothing else you couldn’t prove before), that would be the sort of thing I’m talking about. Unfortunately I don’t know how to state this more precisely.
But perhaps an analogy could help—there’s a bunch of logic gates, and it turns out that some of them (NOR and NAND) can create every other logic gate if arranged correctly, while others can’t. So let’s say I build some circuit out of NANDs and someone blames me for “relying” on NANDs. In that case, I could show him that an equivalent circuit can be made out of NORs. I think before you learn the fact that both logic gates are universal, this would be a non-intuitive substitution.
When I talked to Abram he said that there’s probably many different formulations of number theory which logicians have proven equivalent to PA. I tried to quickly look for something like that to give as an example, but I’m really out of my depth (if I wasn’t I would have included such an example from the start).
I mean, consider a trick like replacing axioms {A, B} with {A or B, A implies B, B implies A}. Of course it’s what you call an “obvious substitution”: it requires only a small amount of Boolean reasoning. But showing that NOR and NAND can express each other also requires only a small amount of Boolean reasoning! To my intuition there doesn’t seem any clear line between these cases.
If your question is whether an axiom of PA can be replaced by an equivalent statement which can serve as a replacement axiom and prove the old axiom as a theorem, then the answer is yes, and in a very boring way. Every mathematical statement has tons of interchangeable equivalent forms, like adding “and 1=1” to it. Then the new version proves the old version and all that jazz.
If your question is whether we should believe in PA more because it can arise from many different sets of axioms, then I’m not sure it’s meaningful. By the previous point, of course PA can arise from tons of different sets of axioms; but also, why should we care about “believing” in PA? We care only whether PA’s axioms imply this or that theorem, and that’s an objective question independent of any belief.
If your question is whether we can have a worldview independent of any assumptions at all, the answer is that we can’t. The toy example of math shows it clearly: if you have no axioms, you can’t prove any theorems. You have latitude in choosing axioms, but you can’t dispense of them completely.
re PA: I mean a statement that we would intuitively see as non-trivially different, not merely the same statement with “and 1=1” added.
re 3: I’m not asking if we can have a worldview independent of any assumptions at all. I’m asking if we can have a worldview independent of any specific assumptions. That is, among the various sets of assumptions we can use to justify our worldview, there’s no assumption that’s common to all sets (i.e, always required to justify the worldview).
Then I guess you need to quantify “intuitively see as non-trivially different”. For example, take any axiom A in PA, and any theorem T that’s provable in PA. Then A can be replaced by a pair of axioms: 1) T, 2) “T implies A”. Is that nontrivial enough? And there’s an unlimited amount of obfuscatory tricks like that, which can be applied in sequence. Enough to confuse your intuition when you’re looking at the final result.
No, I’m not talking about obfuscatory tricks of this sort. If you could replace A with T without also adding “T implies A” as an axiom, and still be able to prove A (an everything else you could have proved before, and nothing else you couldn’t prove before), that would be the sort of thing I’m talking about. Unfortunately I don’t know how to state this more precisely.
But perhaps an analogy could help—there’s a bunch of logic gates, and it turns out that some of them (NOR and NAND) can create every other logic gate if arranged correctly, while others can’t. So let’s say I build some circuit out of NANDs and someone blames me for “relying” on NANDs. In that case, I could show him that an equivalent circuit can be made out of NORs. I think before you learn the fact that both logic gates are universal, this would be a non-intuitive substitution.
When I talked to Abram he said that there’s probably many different formulations of number theory which logicians have proven equivalent to PA. I tried to quickly look for something like that to give as an example, but I’m really out of my depth (if I wasn’t I would have included such an example from the start).
I mean, consider a trick like replacing axioms {A, B} with {A or B, A implies B, B implies A}. Of course it’s what you call an “obvious substitution”: it requires only a small amount of Boolean reasoning. But showing that NOR and NAND can express each other also requires only a small amount of Boolean reasoning! To my intuition there doesn’t seem any clear line between these cases.