As far as I can guess, you are asking what I already mentioned:

Given P, is "What is the length of the shortest proof of P?" computable? — TonesInDeepFreeze

Well, yes. I'm concerned with complexity of a theorems proof or what I think is how you can gauge complexity in mathematics, through determining how simple the proof is for any theorem.

Does that sound about right?

And, based on past reasoning, whether a theorems proof is determinate in regards to complexity in a formal axiomatic system, then the method at determining this is dependent on XYZ, with XYZ helping in determining complexity of a theorem proof's least exhaustive Q.E.D. to be performed by a Turing machine or simply computable.

Let me know if that's a word salad again. :sweat:

"XYZ"-In my mind is either or related to completeness or consistency, which is where my confusion seems to arise.

As far as I can guess, you are asking what I already mentioned:

Given P, is "What is the length of the shortest proof of P?" computable?
— TonesInDeepFreeze

Well, yes. I'm concerned with complexity of a theorems proof — Shawn

And by 'complexity' do you mean 'the sum of the lengths of the formulas in the proof'?

Well, yes. I'm concerned with complexity of a theorems proof or what I think is how you can gauge complexity in mathematics, through determining how simple the proof is for any theorem. — Shawn

I'm thinking again of having proven a theorem, putting into a computer algorithm, then counting symbols to ascertain "complexity." I guess that would be some sort of definition, but why one would wish to do that is not clear to me. I suppose one could say, "Oh, Gill's proof of Theorem X has complexity 32, whereas Kojita's proof has complexity 56." Then what? :roll:

I find it interesting whether there is an algorithm to compute the least length.

I take it we are talking about proofs in the first-order predicate calculus.

Not sure, but I think this is right: Any theorem has only finitely many symbols from the language signature, so a shortest proof would use only (1) connectives (of which there are only finitely many) and quantifiers (of which there are only finitely many), (2) signature symbols in the the theorem itself, and (3) finitely many variables. Then, modulo the variables used (since swapping variables wouldn't change length), for any n, there are only finitely many sequences of formulas whose sum of formula lengths is n. So, successively, for each n, look for proofs of the theorem. The answer is the first n that has a proof.

So, when I say that a proof of a theorem is subject to not being able to determine its complexity does that mean anything? — Shawn

What do you mean by the complexity of a proof? I've already suggested that it could be defined as the length of a proof in some formal proof system. What do you mean by it?

What I'm trying to determine is whether there is any possibility to determine the complexity of proofs by reasoning that a Q.E.D. would occur at the least exhaustive method of determining it. — Shawn

What is a QED? Do you mean a proof?

Does that make sense? Following with this logic, if you don't have a method of doing this, then how can you determine complexity in mathematical proofs? — Shawn

I've already suggested a way. I don't know that it's regarded as particularly important but I could be wrong about that. For sure it's important in computer science, and I pointed you to complexity theory.

And by 'complexity' do you mean 'the sum of the lengths of the formulas in the proof'? — TonesInDeepFreeze

Here's the inherent problem as I see it, in that there's no syntactically quantifiable method, not least a semantical qualitative method to make "complexity" determinate. What do you think?

Mathematicians often talk about a theorem or conjecture being qualitatively "hard", yet for "complexity", there's no syntax, or is there?

If all one wants to do is count primitives or the length of the proof, then there's still the burden of determining how to estimate its Turing complexity, yes?

Interesting ideas, but to my mind it's putting the cart before the horse. I don't see how this sort of knowledge would help prove a theorem, which is the essence of mathematics. But then the very idea of theorem proving as a programming exercise is foreign to me. However, I use the computer all the time for imagery and examples which may point the way forward in my deliberations. My age, I suppose.

I'm thinking again of having proven a theorem, putting into a computer algorithm, then counting symbols to ascertain "complexity." I guess that would be some sort of definition, but why one would wish to do that is not clear to me. I suppose one could say, "Oh, Gill's proof of Theorem X has complexity 32, whereas Kojita's proof has complexity 56." Then what? — jgill

Yes, and as to this, I think that it is important in terms of making mathematics more formal in saying that a less complex formal proof for a theorem is important, no?

I sort of dread the notion of making mathematics more formal. :scream:

Mathematicians often talk about a theorem or conjecture being qualitatively "hard" — Shawn

Nothing at all hard about the conjectures or the theorems. Be good if you payed attention to the words. It would appear you're getting your "completeness" from problems that are considered NP-complete. There are many Youtube videos on NP-completness, for almost every level of student. Give some a try .

What do you mean by the complexity of a proof? I've already suggested that it could be defined as the length of a proof in some formal proof system. What do you mean by it? — fishfry

I keep on repeating myself here; but, I discussed earlier that there's some lack of language with a syntax that could ascertain this. The only example I keep on mentioning is related to Kolmogorov complexity, which is non-computable.

What is a QED? Do you mean a proof? — fishfry

Yes.

I've already suggested a way. I don't know that it's regarded as particularly important but I could be wrong about that. For sure it's important in computer science, and I pointed you to complexity theory. — fishfry

Well, this much I understand; but, the point of this thread is in regards to whether there is any relation to an axiomatic system that is either or consistent and complete and the determination of "truth" as to whether the axiomatic system is subject to degrees of "complexity"? Which, seemingly can only be entertained when providing proofs, and those proofs being subject to a formal measure of complexity...

If my previous post is correct, then I take it that your full question is:

What is the complexity class of such an algorithm?

I don't know. And I'm not very much informed on complexity classes.

I don't see how this sort of knowledge would help prove a theorem — jgill

I find it interesting as a mathematical question onto itself.

Interesting ideas, but to my mind it's putting the cart before the horse. I don't see how this sort of knowledge would help prove a theorem, which is the essence of mathematics — jgill

There's something in my mind that I haven't disclosed, and this is more of a sentiment if you don't care or whatnot; but, without knowing that a theorem's proof is more complex or less, that this contributes to mathematics seeming a lot more, how to put this lightly, disorganized or uncategorized? I'm not sure if you follow me on this sentiment. Feel free to comment if not.

Nothing at all hard about the conjectures or the theorems. Be good if you payed attention to the words. It would appear you're getting your "completeness" from problems that are considered NP-complete. There are many Youtube videos on NP-completness, for almost every level of student. Give some a try . — tim wood

Yet, try and specify this syntactically/quantifiably in a formal system, if you can even begin to. Non-trivial stuff...

What is the complexity class of such an algorithm?

I don't know. And I'm not very much informed on complexity classes. — TonesInDeepFreeze

There was an attempt at doing this by Russell and Whitehead in the Principia Mathematica, where they utilized type theory extensively, to no avail. Set-theory can't do this; but, type theory can to some degree.

Food for thought?

Yet, try and specify this syntactically/quantifiably in a formal system, if you can even begin to. Non-trivial stuff... — Shawn

Don't make an idol out of your ignorance - been there done that; it doesn't work. Watch some videos, learn

If my attempt was correct, and there are only finitely many symbols in the signature, then, if I'm not mistaken, there is an algorithm to list the theorems in order of proof length (and, say, lexicographically within length).

I don't know. And I'm very much informed on complexity classes.
— TonesInDeepFreeze

There was an attempt at doing this by Russell and Whitehead in the Principia, where they utilized type theory extensively, to no avail. — Shawn

PM addressed complexity classes?

If my attempt was correct, and there are only finitely many symbols in the signature, then, if I'm not mistaken, there is an algorithm to list the theorems in order of proof length (and, say, lexicographically within length). — TonesInDeepFreeze

So, it's syntactic? How do you make it both syntactic and semantical within a formal system to ascertain the Turing complexity of the task, as I understand it, type theory doesn't do this syntactically to quantify this methodologically according to Turing Complexity; but, rather semantically.

PM addressed complexity classes? — TonesInDeepFreeze

That's my estimate. What do you think?

See the previous post to you.

Set-theory can't do this — Shawn

What does "this" refer to there? Set theory can't do a lot of things, but what is it in particular are you saying set theory can't do?

What does "this" refer to there? Set theory can't do a lot of things, but what is it in particular are you saying set theory can't do? — TonesInDeepFreeze

Sorry, I was thinking about it dialectically with regards to type theory, which I explained my thoughts about above in the post above.

PM addressed complexity classes?
— TonesInDeepFreeze

That's my estimate. — Shawn

Estimate based on what?

I don't see it in the table of contents given in the article on PM in the SEP.

A little off-topic; but, type theory can resolve the set of all set paradox by hierarchy classes, which is confusing, because its not entailed within it to do so; but, has to do it extra-syntactically or even semantically.

How do you make it both syntactic and semantical within a formal system to ascertain the Turing complexity of the task — Shawn

I have no idea what you mean.

What does "this" refer to there? Set theory can't do a lot of things, but what is it in particular are you saying set theory can't do?
— TonesInDeepFreeze

Sorry, I was thinking about it dialectically with regards to type theory, which I explained my thoughts about above in the post above. — Shawn

I have no idea what you mean.

Are you deliberately wasting people's time with remarks you've intentionally prepared to be gibberish or are so personally esoteric that no one but you could know what you mean?

Are you deliberately wasting people's time with remarks you've intentionally prepared to be gibberish or are so personally esoteric that no one but you could know what you mean? — TonesInDeepFreeze

Sorry, I'm still struggling with the language on the issue.

Feel free to ignore my word salads.

If my previous post is correct, then I take it that your full question is:

What is the complexity class of such an algorithm?

I don't know. And I'm not very much informed on complexity classes. — TonesInDeepFreeze

I seem to have last been on the same page here, and brought in type theory in regards to determining class hierarchy when talking about...

EDIT:

type theory, but, resolving entailment of the set of all sets, by hierarchy classes.

I find it interesting as a mathematical question onto itself. — TonesInDeepFreeze

True enough. Beyond my pale.

resolving entailment of the set of all sets, — Shawn

There is no set of all sets, I hope we're not going down this road.