But, you do acknowledge that the complexity class of a algorithmic theorem's proof can be indeterminate, as long as the machine engages in non-brute force methods to determine "complexity"?

But, you do acknowledge that the complexity class of a theorem's proof can be indeterminate, as long as the machine engages in non-brute force methods to determine "complexity"? — Shawn

I have no idea, I know very little of these matters.

I have no idea, I know very little of these matters. — fishfry

Do you know of any way to approach this problem? I'm assuming you will reference information theory, which isn't what I think is appropriate to ascertain "complexity", or is it?

Do you know of any way to approach this problem? I'm assuming you will reference information theory, which isn't what I think is appropriate to ascertain "complexity", or is it? — Shawn

I've referred you to Turing degree, complexity theory, and proof systems like Agda and Coq. I'm all out of ideas. A good resource for complexity theory is everything on Scott Aaronson's website. https://www.scottaaronson.com/

Turing degree — fishfry

Whether the problem of quantifying "complexity" is undecidable or decidable, I know not.

I'm assuming you can decide the Turing degree; but, I have no idea how difficulty would be estimated, nor how it could be estimated.

A machine for ascertaining the length of the shortest proof of a theorem doesn't involve anything like oracles — TonesInDeepFreeze

A posteriori I assume? Not a priori.

@TonesInDeepFreeze, how would you reformulate the OP to better ask the question?

I'm wondering about reaching out on somewhere like Stack Exchange for more information or how to answer it.

Thanks in advance!

I'm wondering about reaching out on somewhere like Stack Exchange for more information or how to answer it — Shawn

That's a possibility, but be prepared for some confusion about what you are asking. You're in a different ball game on that forum.

how does the machine do this without a brute force method? — Shawn

I'm still not sure what your question is. Also, I'm not very informed about complexity, so my own formulation might need correction too. But here's my best try:

For first order theories, is it correct that there is a brute force algorithm that tells us the shortest proof length for any given theorem ('length' means the sum of the lengths of the formulas that appear as lines in the proof)? What is the complexity class for the algorithm? Are there algorithms better than brute force? What is the least complexity class for an algorithm to tell us the shortest proof length?

https://math.stackexchange.com/questions/4141341/problem-of-finding-shortest-proof-how-complex-is-it

Darn. I need to edit my reply.

Can you edit your stackexchange post?

(I think complexity class pertains to the problem not the algorithm?)

This is better:

For first order theories, is it correct that there is a brute force algorithm that tells us the shortest proof length for any given theorem ('length' means the sum of the lengths of the formulas that appear as lines in the proof)? Are there algorithms better than brute force? What is the complexity class for the problem?

Edited, let me know if the title needs to be more precise.

I would title it:

Problem of finding shortest proof - how complex is it?

But I really have to warn that, since I'm not really informed on this particular subject, my own formulation might get shot down.

A response to it:

If your theories are allowed to have infinitely many axioms (defined by some recursive enumeration of the axioms), then there is no such brute force algorithm: the shortest possible proof of ⊢ϕ is when ϕ is an axiom, but it would require an infinite search through the axioms to find out whether that is so. If you restrict to finitely axiomatisable theories, then there is a brute force algorithm that just enumerates all the proofs of length 1, then 2 and so on and will find the shortest proof if the input ϕ is a theorem. I imagine the complexity will be enormous. — Rob Arthan

I was going to write:

"I should have stipulated that we're talking about finitely axiomatizable theories. Even if the theory is recursively axiomatizable but not finitely axiomatizable, then the method would not work."

So I thought his argument was correct. But then I saw that he amended to say that brute method would work if 'length' is defined by symbols not lines. (And we did define by symbols not lines.) So, by his amended argument, the paragraph above in which I correct myself is not correct and I never needed to correct myself except to include that the theory is recursively axiomatizable. But I don't see why his original argument is still not correct, whether it's symbols or lines. So I am confused.

He gave this as the answer:

https://math.stackexchange.com/a/4141376/928370

There are two reasonable ways to measure the length of a proof: by steps or by symbols. For step-length, we can brute-force-search for proofs and be certain we've found the shortest one as long as our axiom system is finite - for symbol-length, we only need that the language is finite and our axiom system is computably axiomatized (e.g. PA and ZFC).

That said, in either case we have a serious issue as far as complexity is concerned: as long as our axiom system is "sufficiently rich," for every computable function F there is some theorem φ which has no proof of length ≤F(length(φ)). (Basically, we're looking at the Busy Beaver function in disguise when we talk about bounding proof searches ahead of time.)

That said, this doesn't rule out (i) efficient proof search in simpler theories or (ii) efficient proof search for particularly simple results. There's a rich literature on this topic, beginning with the already-interesting case of propositional proof search - "automated theorem proving" is a good keyword for this.

I read that.

Here's another:

Length & Complexity

Let me know what you think to say?

There still seems to be a little confusion about a priori vs a posteriori approaches to these ideas - at least for me. The notion of an automated theorem prover doing its job, and then the complexity of the proof being determined, seems quite distant from a program simply counting symbols and logical steps in existing proofs. But I can understand how an ATP might function under the guidance of a mathematician.

However, the idea that I could take the theorem I am trying to prove right now and turn it over to an ATP is far fetched. Although appealing, I must admit. I am at the point that there might be the slightest possibility it falls into the Godel Hole, since I find that to prove the conjecture seems to require that I assume the conjecture, a circular trap. I'm not speaking of an indirect proof. All my computer experiments suggest it is true. :worry:

I am at the point that there might be the slightest possibility it falls into the Godel Hole, since I find that to prove the conjecture seems to require that I assume the conjecture, a circular trap. I'm not speaking of an indirect proof — jgill

Can you explain this, as I'm quite interested?

Thank you.

It's an interesting topic, yeah?

Given clarity in discussion about it, yes, it is interesting. It's something I have wondered about before.

If I have time later, maybe I'll reply on StackExchange to better understand some of the points.

It's interesting for myself and perhaps @jgill that how do you discern axioms in the theorem that are non-computable from those that are computable.

What do you think?

how do you discern axioms in the theorem that are non-computable from those that are computable. — Shawn

What do you mean by 'computable axiom'?

'recursive axiomatization' is given a rigorous definition. With a theory that is recursively axiomatizable, it is computable whether a symbol string is or is not an axiom. And we may stipulate that we are using effectivized languages. In ordinary cases, if the theory is recursively axiomatizable, then we know an algorithm for checking whether a symbol string is or is not an axiom.

What do you mean by 'computable axiom'? — TonesInDeepFreeze

I have something that addresses this here:

Gödel's incompleteness theorem applies to formal languages with countable alphabets. So it does not rule out the possibility that one might be able to prove 'everything' in a formal system with an uncountable alphabet OR expand the alphabet to account for new variables.

Given the above, does it follow that, Turing complexity is subject to completeness rather than consistency of a theorem in a formal language with countable alphabets? However, if ordinality is considered, then consistency matters more for determining computational complexity, et that renders theorems posited in countable alphabets only.

I am trying to discern computability in terms of complexity with regards to a formal system with an uncountable alphabet OR expand the alphabet to account for new variables to render it as "complete" and Turing computable as possible without incurring uncountability? — Shawn

Is it meaningful to talk about computability of uncountable alphabets, at all and given this thread?

It's too much work for me to try to have you make that quote understandable.

If the language is uncountable, then the theory is not recursively axiomatizable and is not a formal theory. And, yes, Godel's theorem pertains only to formal theories.

A book you should read:

Godel's Theorem: An Incomplete Guide To Its Use and Abuse - Franzen.

It's not a technical tome, and I bet it would answer a lot of your questions right away.

I redid it and asked the following question:

Gödel's incompleteness theorem applies to formal languages with countable alphabets. So it does not rule out the possibility that one might be able to prove 'everything' in a formal system with an uncountable alphabet OR expand the alphabet to account for new variables.

Two ideas follow from the above:

-Hypothetically, a theorem can be "complete" if uncountable.
-A theorem can "reach" completeness in a limited fashion before being considered "uncountable", hence a sort of "loophole".


Therefore, would it be possible to demonstrate a theorem that is as close as possible to being "complete" without it becoming uncountable?

Concerning the "loophole" the demarcation between countability of an alphabet and uncountability would render the theorem complete, if the demarcation can be ascertained a priori or a posteriori?

https://math.stackexchange.com/questions/4142390/completeness-without-uncountability

I am interested to see what people there say about your notion of a 'complete theorem'.

I asked you previously: Do you understand the difference between a theory and a theorem?

it is computable whether a symbol string is or is not an axiom. — TonesInDeepFreeze

Not to argue, but that's quite a claim. No need for a citation - I wouldn't understand it - but can you take a second look and confirm? So that I may tell others that Tones told me so.