What's so individualistic about being poor, unless this is just trite satire?

I'm also trying to figure out whether the complexity class is determinate for the first question I asked on StackExchange.

https://math.stackexchange.com/questions/4144858/finding-the-shortest-proof-how-complex-is-it

This thread is a fishing expedition. I'm seeking out those who disagree with this proposition: Science is a good thing, to see what their arguments are. — Banno

What you fishing for?

I tend to lean on pragmatism, is that an interesting fish?

Yes, it's no longer a special place.

@TonesInDeepFreeze,

I've been wondering if the question posted over at StackExchange, is generalizable?


What do you think?

Here's the other question asked just for fun:

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

I got this reply, which is really interesting for me to understand:

The real key to Gödel is that the axioms are recursively enumerable, not countable. We can show there exist maximal consistent subsets of the countable set of all statements, and take those as axioms. Then we can show that maximality implies completeness. It’s just not useful for human or computer-read proofs, because there is no way to algorithmically prove each step is allowed.

What do you think @jgill, and @TonesInDeepFreeze?

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

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

It's an interesting topic, yeah?

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.

Let me know what you think to say?

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.

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

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 for more information or how to answer it.

Thanks in advance!

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.

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?

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

The method I mentioned is brute force. I don't know whether there's a better method. — TonesInDeepFreeze

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.

What's interesting is that this is not a linear order. — fishfry

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

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

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

Rather, it's about know the complexity of solving this particular solvable problem. — TonesInDeepFreeze

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 robust oracle machine.

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

Am I getting that much right?

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 computability. That's where I left off with @TonesInDeepFreeze

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 importance, no?

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

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

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

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.

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.

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.

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. What do you think?

See the previous post to you.

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.

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

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?