Timeline for Proof as a Σ₁ approximation to truth: what about higher degrees?
Current License: CC BY-SA 4.0
7 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Aug 8, 2018 at 3:39 | comment | added | James | (cont'd) for if you went one-by-one checking numbers in increasing order, you either never find a number in that set, or there is a first time when you find a number in that set. I think the fact that it is an axiom schema rather than an axiom obfuscates the fact that the least number principle is really a single principle with an intuitive picture, rather than a collection of related principles. It's not so easy to see what the intuitive picture behind the consistency of PA is. What is the general principle which allows you to conclude PA and similar theories are consistent? | |
| Aug 8, 2018 at 3:35 | comment | added | James | (cont'd) that we have some prior knowledge of how to prove things about such machines. E.g., it seems humans have the ability to see that many different hypothetical adding machines are all equivalent. The axioms of PA minus induction maybe could be considered "obvious", and constitute background assumptions (which exist in all fields of science). Most people have a pretty clear understanding of why the least number principle is true: every natural number can be reached by adding 1 to itself multiple times, and there must be a first such number in any non-empty set we can define, | |
| Aug 8, 2018 at 3:27 | comment | added | James | Of course circularity is a problem if you try to completely formalize this notion. The idea would be that certain machines (or machines that create machines, or machines that create machines that create machines) will serve essentially as physical Skolem functions. The existence of such a machine, together with a proof of its correctness, can constitute a verification of a formula, even if it has many alternations of quantifiers. The circularity comes, as you point out, from the fact that PA would probably be the theory we use to prove correctness of such machines. However, it could be argued | |
| Aug 7, 2018 at 22:27 | comment | added | Andreas Blass | I find it difficult to think of a (non-trivial) meaning for "things we can know without access to an oracle" that would exclude "PA is consistent" but would include all the induction axioms of PA for arbitrarily complex arithmetical formulas. (The reason I wrote "non-trivial" is that, of course, one could take provability in PA as one's criterion for oracle-less knowability, but that would make any resulting claim about a special status for PA circular.) | |
| Aug 7, 2018 at 20:25 | comment | added | James | We can build a machine which takes $n$ and outputs a prime bigger than $n$. Perhaps verfiability is the wrong word. | |
| Aug 7, 2018 at 20:15 | comment | added | Nik Weaver | "that PA consists of exactly the verifiable truths of arithmetic (those which you could, hypothetically, build a machine to verify)" --- this seems like a misleading way to summarize the previous comment. (PA proves that there are infinitely many primes: is this something you could, hypothetically, build a machine to verify?) | |
| Aug 7, 2018 at 19:22 | history | answered | James | CC BY-SA 4.0 |