Talk:Addition of Natural Numbers is Provable
It's worth bearing in mind that we've already made a start on provability theory, but rather than take the route of using a Turing machine, we used an Unlimited Register Machine instead. The content and structure of the material in this area of mathematics was based more or less faithfully on the course in mathematical logic presented by the Open University some 20 years or so ago. Hence you may find a lot of the hard work you are putting into this can be alleviated by seeing whether you can parallel any of the work you're doing with the (easier to handle) analysis that is already there. --prime mover (talk) 09:00, 16 March 2023 (UTC)
- I'm aware of the existing work on recursive functions on this website. Right now, I'm basically composing an overcomplicated equivalence proof between Turing machines and said recursive functions, mostly because each step along the way is an interesting result on its own. Here's the sketch:
- Recursive Function reduces to $\Sigma_1$ WFF
- True $\Sigma_1$ WFF is provable
- Existence of theorem-proving (nondeterministic) Turing machine
- Reduction from nondeterministic Turing machine to Turing machine
- Is there an easier way to do this? Yes, absolutely. With multitude machines already handled, we can put each register of a URM on its own tape. That would yield a simple equivalence proof. I may add that proof at some point, but for now the long way shares steps with, for example, Gödel's Incompleteness Theorems. Also I thought it was cool. --CircuitCraft (talk) 10:59, 16 March 2023 (UTC)
- No worries then, if you're happy doing this then, as the saying goes, fill your boots. --prime mover (talk) 11:42, 16 March 2023 (UTC)
- Okay, I went back and reviewed the URM work, and I changed my mind on what I'm going to do. I'm going to construct the theorem prover as a recursive function in the same manner as Gödel, reusing as much as I can of the existing proofs, as they are much easier to compose (I was running into issues with embedding a Turing machine that decides the axioms into a nondeterministic machine). Then, I'll do the simple URM to Turing machine proof I mentioned earlier. Thanks for the advice! --CircuitCraft (talk) 14:40, 16 March 2023 (UTC)
The reason for the tableau structure is that I want to be very, very precise in these proofs. It's far too easy to accidentally use principles of natural numbers that do not hold in minimal arithmetic. Even more importantly, though, the tabular form contrasts strongly with the worded proofs, which emphasizes the boundary between "regular" logic, and the formal system. For example, induction is absolutely forbidden within one of these proofs, while it's perfectly acceptable (and used frequently) outside of them.
Besides, I intend on eventually talking about what theorems can be proven with a particular algorithm. This will involve showing that it completely contains the logical system in which they were derived. Keeping a formal structure like this is the best way I could come up with to make this rigorous. --CircuitCraft (talk) 17:00, 17 April 2023 (UTC)