Lucas K.
|
Registered User
|
I thought I was good in math, but then I see all the questions and answers and I doubt.
Interest in repairing Hilbert's program, by adding extra axioms, such as the constructive omega rule.
I believe that PI2 sentences, are the only fundamental mathematical problems. All mathematical problems that can not be expressed as PI2 sentence, is to my opinion, meta-mathematics (that does not imply that it has lower value).
|
|
May 6 |
awarded | ● Yearling |
|
Jan 20 |
comment |
Can invariant of transitive reflexive closure in FOL+PA always been proven? Access to the book again. The problem is that the first lemma of 6.4 is a lemma that can not be expressed as a lemma in FOL+PA (therefore not formally proven). If you want something that can be expressed in FOL+PA, one should have a sequence like construction, where you prove that the sequence can be extended with a new element. Such as theorem 1.9ii of the piece of Jaap van Oosten. Consequence is that Shoenfield only proves informally that certain functions are recursive, but is insufficient shown that recursiveability is provable in PA. I don't know if any theorems in the book depend on it. |
|
Jan 19 |
comment |
Is equality of terms for “real” numbers with roots, logarithm, exponential, sin, cos, and other trigonometric operations decidable with a Turing-machine? If the answer is yes, then the next question is if it is NPC. |
|
Jan 19 |
comment |
Can invariant of transitive reflexive closure in FOL+PA always been proven? I agree with you that a fully formal proof would make a book unreadable (although, in these times you can put it on the internet and give a reference in the book :-). However, one can adopt a style of writing, where it is very clear how theorems (so, not proofs) could be writtten formaly. The referenced piece of Jaap van Oosten follows this style, and leaves many proofs to the reader (which I consider okay). The Shoenfield book doesn't follow this style. The sequences pop up in informal mathematics, without proper link to the formal part. |
|
Jan 19 |
comment |
Can invariant of transitive reflexive closure in FOL+PA always been proven? Note, that the proof is not required for the remaining part of the book. It is necessary to show that you can do basic mathematics (whatever that is) in FOL+PA. The book only addresses that FOL+PA can define certain things, such as computable functions. Still, I consider it an omission. My question popped up, because I was looking at rather simple systems where you could do some real mathematics, without the complexity of ZFC or type theory. If you start with a closure operator and a successor operator, you don't need the + and x of PA and it is a better prequal to 2nd order logic. |
|
Jan 19 |
comment |
Can invariant of transitive reflexive closure in FOL+PA always been proven? Andreas, I don't have the book by hand, because I am typing from a different location. But I do not agree with you that the proof was designed to be easily formalizable. The informal proof starts with an sequence. In the formal part, you are just trying to prove the basic properties of sequence. So, that is a no go. If you look to the reference I gave of Jaap van Oosten, you will see that the proof contains several non trivial induction step. You need to prove that a sequence can be extended. This is not trivial, when it is encoded with prime number, because you need to choose a new one. |
|
Jan 8 |
comment |
What axioms are used to prove Godel’s Incompleteness Theorems? @Andrew, although it is often mentioned that PA or PRA suffices, it is very hard to find the right material that tells how. There are some tricks to go from numbers to more complex datastructures and proves of that. Loops in programs can be rather easily expressed in closures. But, then you need the basic properties of closures. See for a detailed build of theorems: staff.science.uu.nl/~ooste110/syllabi/… |
|
Dec 30 |
comment |
Role of statistical estimation in formal proof There is always the problem with probabilistic or statistical methods, that you may not ignore knowledge. In mathematical proof you may ignore info, that you don't need. If value c is determined, but someone comes with a good argument that the c is incorrect in this particular case, then you may not ignore that argument. That makes any answer obtained by this method, instable due to future knowledge. |
|
Dec 30 |
answered | Can invariant of transitive reflexive closure in FOL+PA always been proven? |
