reckless intuitions of an epistemic hygienist ([info]gustavolacerda) wrote,
@ 2005-05-24 21:30:00
Previous Entry  Add to memories!  Tell a Friend!  Next Entry
Entry tags:logic

proof of mathematical result by non-constructively showing that there must exist a proof of it(?)
Has 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'.


(Post a new comment)


[info]combinator
2005-05-24 07:33 pm UTC (link)
I suppose the proof of your mathematical result would be a proof of A, then? How would this not be a construction of a proof?

(Reply to this)

Non-constructively that There Exists A Proof
[info]r6
2005-05-24 08:32 pm UTC (link)

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.

(Reply to this) (Thread)
Re: Non-constructively that There Exists A Proof
[info]gustavolacerda
2005-05-24 09:02 pm UTC (link)
“there exists a proof of A” is a Σ1 sentence
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?

(Reply to this) (Parent)

(Deleted post)
Re: Non-constructively that There Exists A Proof
[info]gustavolacerda
2006-05-30 02:52 pm UTC (link)
I can imagine that there are cases in which the existence of an object (in this case a proof of phi) is more easily proven than exhibited. In such cases, we would know that a proof exists even though we don't have it (although, as you point out, it could be found by exhaustive search).

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.

(Reply to this) (Parent)(Thread)
Re: Non-constructively that There Exists A Proof
[info]r6
2006-05-30 03:18 pm UTC (link)
We can easily prove that PA proves induction for any ordinal &alpha < ε0; however, the proofs become arbitrarily large as &alpha approaches ε0. This might be what you are looking for, but I’m not sure if the proof lengths are polynomial in terms of the length of the ordinal notation for &alpha or not. I suppose it needs to be non-polynomial for this to be an example of what you are looking for.

(Reply to this) (Parent)(Thread)
Re: Non-constructively that There Exists A Proof
[info]r6
2006-05-30 03:30 pm UTC (link)

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 φ = ⊥.

(Reply to this) (Parent)
Re: Non-constructively that There Exists A Proof
[info]gustavolacerda
2006-05-30 04:18 pm UTC (link)
My thoughts are still confused, but here they are anyway.


<< 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

(Reply to this) (Parent)
Hello2
(Anonymous)
2008-09-28 10:38 am UTC (link)
Hello
Nice site!

G'night

(Reply to this)

Create an Account
Forgot your login or password?
Login w/ OpenID
English • Español • Deutsch • Русский…