![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
guslHas anyone ever proven a mathematical result by stating that there must exist a proof of it, and proceeding to prove this non-constructively?
i.e., you prove non-constructively that there exists a proof of A.
I've used arguments that there must exist a proof of A because A is dual to A' (in the sense that the axioms are preserved under permutation of, e.g. union and intersection), for which we already have a proof.
But in this case, it's pretty easy to construct the proof of A by applying a transformation on the proof of A'.
i.e., you prove non-constructively that there exists a proof of A.
I've used arguments that there must exist a proof of A because A is dual to A' (in the sense that the axioms are preserved under permutation of, e.g. union and intersection), for which we already have a proof.
But in this case, it's pretty easy to construct the proof of A by applying a transformation on the proof of A'.
![[identity profile]](https://www.dreamwidth.org/img/silk/identity/openid.png){kind=small}
(no subject)
Date: 2005-05-24 07:33 pm (UTC)Non-constructively that There Exists A Proof
Date: 2005-05-24 08:32 pm (UTC)The statement “there exists a proof of A” is a Σ1 sentence, and every classically provable Σ1 sentence is also constructively provable; just do a search.
Re: Non-constructively that There Exists A Proof
Date: 2005-05-24 09:02 pm (UTC)because proof-checking is Delta_1... ok.
every classically provable Σ1 sentence is also constructively provable; just do a search.
If "there exists a proof of A" is classically provable, then it's true. Then there exists a proof of A. Then a proof of A can be found by searching. But there's no guarantee that this proof will be constructive.
Your idea would work if we started with "there exists a constructive proof of A".
Ok, but even if all classically provable Sigma_1 sentences are constructively provable,
my question was about whether it could ever be easier / quicker to prove something by using the method above: is the non-constructive proof-existence proof easier to find?
btw, how do you do math symbols in HTML?
Re: Non-constructively that There Exists A Proof
Date: 2006-05-30 02:52 pm (UTC)This existence result, of course, serves as another proof of phi.
...but this would feel very strange, like a free lunch, since we don't have a procedure for constructing the concrete proof (other than exhaustively searching through all potential proofs). I'm wondering whether such a situation is possible, and if so, whether there are examples of it.
Re: Non-constructively that There Exists A Proof
Date: 2006-05-30 03:18 pm (UTC)Re: Non-constructively that There Exists A Proof
Date: 2006-05-30 03:30 pm (UTC)Of course it is important to note that the proof that PA proves these inductions requires a stronger system than PA. So if all you are intrested in is knowing induction upto ε0, then you might as well prove it directly in your stronger system and skip this whole nonsense about proofs in PA.
Bear in mind that for reasonable systems, T ⊬ PrT(φ) ⇒ φ—in particular when φ = ⊥.
Re: Non-constructively that There Exists A Proof
Date: 2006-05-30 04:18 pm (UTC)<< We can easily prove that PA proves induction for any ordinal &alpha < ε0; however, the proofs become arbitrarily large as &alpha approaches ε0. >>
Is this a Goedel-like result, in that for every axiom system stronger than PA, there is a sequence of theorems whose proof-length curve gets strictly less complex (e.g. from N^2 to N) when we add an additional axiom?
What does it mean to prove induction for an ordinal? oh, as in "the principle of transfinite induction"?
<< the proofs become arbitrarily large as &alpha approaches ε0. >>
It's interesting how adding an (independent) axiom reduces the complexity for a sequence of proofs. I think of such axioms as sort of oracles, adding to the fundamental expressivity of our language (in programming languages, a less fundamental kind of expressivity allows us to write shorter programs: I say "less fundamental" because in the limit, all programming languages can be written in each other, which is why KC is only machine-relative up to an additive constant).
So the shortest proofs are growing arbitrarily large, even larger than the input, I suppose? (our proofs need to be finite, so inputs like aleph_0 should be measured in terms of their Kolmogorov Complexity)... but this is a tangent.
It's also interesting that, at least in the weaker system, proofs are NOT like programs: the complexity of the shortest program computing something (i.e. Kolmogorov Complexity) grows linear with the size of the input, very trivially. It would seem that this is because axiom systems are not expressive as a Turing-complete language.
Theorems are more like specifications. The proofs/programs implementing them may grow at any rate, depending on the structure of the system and the language.
But what if we make an axiom system representing the lambda calculus? Never mind cut-freeness: we *need* CUT to make proofs shorter. Surely such a calculus is as expressive as anything, isn't it? In such a system, could there ever be any sequence of theorems whose proof-length curve is gets strictly less complex as we add an extra axiom?
Anyway, all these ideas seem to boil down to:
Proof length vs. Proof complexity
* The first one is language-dependent
* The second is "absolute"/"objective" (i.e. KC)
My intuition is that these two should be the same in an expressive enough language (i.e. lambda calculus).
Maybe I need to think harder about distinguishing between the lengths of:
* proof of phi
* brute force program that generating the proof of phi (small, very slow)
* things in between, possibly reducing the complexity only polynomially
Hello2
Date: 2008-09-28 10:38 am (UTC)Nice site!
G'night