Shawn

He gave this as the answer: https://math.stackexchange.com/a/4141376/928370

A response to it:

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

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

@"TonesInDeepFreeze", how would you reformulate the OP to better ask the question? I'm wondering about reaching out on somewhere like Stack Exchange f...

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

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

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

I see, so that's where I kinda made the quip in the OP about stuff like quantum computing that take the route of least complexity eg. Shor's algorithm...

How would you define it? Is it even possible to define this? And, may I ask how is this distinct from estimating Kolmogorov complexity?

But, how does the machine do this without a brute force method?

Assuming you have a metric to do this by, which is why I reference the need for a way to ascertain the computability beforehand, meaning some kind of ...

OK, I sat down, read it, and read it more, and seemingly you would have the have a powerful oracle machine to make the decision to do this with least ...

OK

Do you think complexity class can determine "complexity" quantifiably for a Turing computable algorithm?

Yes, sir. I'm only pondering if class complexity can be ascertained at the moment for a proof of a theorem in a formal system, for Turing computabilit...

I was talking about type theory in general avoiding the issue of the set of all sets by assigning hierarchy classes as I last read about the issue.

So, within a formal system does anyone think that to determine complexity of a Turing computable proof of a theorem, that consistency is of greater im...

Had this been a total submission to God, @"unenlightened"?

It's off topic; but, I recall reading that Russell solved this by class hierarchy in type theory. I'll search if I'm wrong on this.

Sorry, I'm still struggling with the language on the issue. Feel free to ignore my word salads. I seem to have last been on the same page here, and br...

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

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

That's my estimate. What do you think? See the previous post to you.

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

It's interesting that Abraham changed God's mind that day, but only when it was about authority.

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

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

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

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

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

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 "comp...

And, based on past reasoning, whether a theorems proof is determinate in regards to complexity in a formal axiomatic system, then the method at determ...

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

I'm asking if n or m<n is determine in shortest Turing Computable length given P, and L(P) being P's proof.

Yeah, and that's not even counterintuitive, until I bring into the discussion completeness and consistency of a theorem, which seemingly, as I view it...

It's interesting @"tim wood" and @"fishfry", that Kolmogorov complexity is not computable, so not sure if this is moot.

Yes. No, according to how I view complexity, it's ascertained or determined by the shortest Q.E.D. Well, yes. Meaning that the amount of primitives an...

A rising tide lifts all 'oats. Brotherly love: https://i.imgur.com/JMei5Ek.png

So, when I say that a proof of a theorem is subject to not being able to determine its complexity does that mean anything? What I'm trying to determin...

Please forgive my lack of knowledge on the matter; but, what I wanted to say that a theorems proof for an axiomatic system in math is unable to be asc...

The subject or point in question is whether one can determine a theorem's complexity from the fact that a theorem cannot both be consistent and comple...

Actually, in even more simpler terms to determine the complexity of theorems, supposedly, of greater importance would be a focus on completeness rathe...

Yes, jgill, that's what I mean. In simpler terms, I don't see how logically you can begin to ascertain "complexity" or Turing complexity of a theorem'...

Then provide your reasoning. I don't see what your getting at. Everything written in the OP is just what it says.

There aren't many to talk if any, and Godel's Incompleteness theorems apply retroactively, to all that have denumerable and countable alphabets. Howev...

I think I can help with this question. It simply means the number of steps to determine a Q.E.D. result for a Turing machine. Of course there's no uni...

And, another approach is to determine the amount of information a proof "contains" informationally and then be able to ascertain this with a metric of...

Or in other words how are mathematical theorems and proofs scrutinized in terms of complexity if completeness cannot be determined first.

Another way of stating the OP in terms of a question seemingly would be: At which point when the entropic state of a localized system cause decoherenc...