Computational complexity of formulas of infinite length

[nortexoid]

Hi, I was wondering whether what the computational complexity for valid formulas of infinite length is in a language with denumerably many symbols. In particular, infinite disjunctions and conjunctions are allowed, but the prefix must be finite---i.e. there can only be finitely many distinct variable occurrences.

What about the same question where there may only be infinitely many free variables but a finite prefix?

How about for a language with nondenumerably many symbols, where formulas may be of nondenumerable length?

 

[DrPizza]

I don't believe I understand your question.

 

[Matthias99]

I think I *sort of* understand what you're getting at, but not really. Perhaps you can provide an example of the sort of language you're talking about?

Generally, recognition time for potentially-infinite-length strings is unbounded, since there could be an arbitrary number of symbols you have to process before you can accept or reject the string.

 

[sao123]

Originally posted by: nortexoid
Hi, I was wondering whether what the computational complexity for valid formulas of infinite length is in a language with denumerably many symbols. In particular, infinite disjunctions and conjunctions are allowed, but the prefix must be finite---i.e. there can only be finitely many distinct variable occurrences.

What about the same question where there may only be infinitely many free variables but a finite prefix?

How about for a language with nondenumerably many symbols, where formulas may be of nondenumerable length?

I think someone who has had a little less coffee...doc...translate.

 

[nortexoid]

Let me ask another question.

Is there a *complete* proof theory (decision procedure) for a nondenumerable language consisting of denumerably many predicate letters but nondenumerably many function symbols (including 0-place constants) and variables? Consider the case when the predicate have finite arity, and the case when they have infinite arities (i.e. they may take infinitely many arguments).

 

[Matthias99]

Originally posted by: nortexoid
Let me ask another question.

Is there a *complete* proof theory (decision procedure) for a nondenumerable language consisting of denumerably many predicate letters but nondenumerably many function symbols (including 0-place constants) and variables? Consider the case when the predicate have finite arity, and the case when they have infinite arities (i.e. they may take infinitely many arguments).

I want to say 'yes', but I'm still a little vague on the conditions (it's been a while since I took computational complexity and analysis, so bear with me). You're talking about a language with a potentially infinite (but countable) number of symbols, but a potentially uncountably infinite number of rules/mappings ('function symbols')?

I'm pretty sure you can extend normal techniques for working on infinite numbers of symbols/mappings, but your runtime will definitely be unbounded. You'd arrive at a decision *eventually*, but it could take an arbitrary amount of time if you have a potentially infinite number of rules.

 

[nortexoid]

Originally posted by: Matthias99

Originally posted by: nortexoid
Let me ask another question.

Is there a *complete* proof theory (decision procedure) for a nondenumerable language consisting of denumerably many predicate letters but nondenumerably many function symbols (including 0-place constants) and variables? Consider the case when the predicate have finite arity, and the case when they have infinite arities (i.e. they may take infinitely many arguments).

I want to say 'yes', but I'm still a little vague on the conditions (it's been a while since I took computational complexity and analysis, so bear with me). You're talking about a language with a potentially infinite (but countable) number of symbols, but a potentially uncountably infinite number of rules/mappings ('function symbols')?

I'm pretty sure you can extend normal techniques for working on infinite numbers of symbols/mappings, but your runtime will definitely be unbounded. You'd arrive at a decision *eventually*, but it could take an arbitrary amount of time if you have a potentially infinite number of rules.

I'm not exactly sure what the potential/actual infinity distinction is doing above. In any case, what I am saying is that the number of symbols is uncountable but the number of rules is finite (just one, modus ponens, let's say). There are countably many predicate letters of up to uncountable arity, and there are uncountably many function and constant symbols (where constant symbols are just function symbols of 0 arity, and the arity of function symbols is n for any finite n).

Given such a language, does it admit of a complete proof theory?

 

[Matthias99]

Originally posted by: nortexoid

Originally posted by: Matthias99

Originally posted by: nortexoid
Let me ask another question.

Is there a *complete* proof theory (decision procedure) for a nondenumerable language consisting of denumerably many predicate letters but nondenumerably many function symbols (including 0-place constants) and variables? Consider the case when the predicate have finite arity, and the case when they have infinite arities (i.e. they may take infinitely many arguments).

I want to say 'yes', but I'm still a little vague on the conditions (it's been a while since I took computational complexity and analysis, so bear with me). You're talking about a language with a potentially infinite (but countable) number of symbols, but a potentially uncountably infinite number of rules/mappings ('function symbols')?

I'm pretty sure you can extend normal techniques for working on infinite numbers of symbols/mappings, but your runtime will definitely be unbounded. You'd arrive at a decision *eventually*, but it could take an arbitrary amount of time if you have a potentially infinite number of rules.

I'm not exactly sure what the potential/actual infinity distinction is doing above. In any case, what I am saying is that the number of symbols is uncountable but the number of rules is finite (just one, modus ponens, let's say). There are countably many predicate letters of up to uncountable arity, and there are uncountably many function and constant symbols (where constant symbols are just function symbols of 0 arity, and the arity of function symbols is n for any finite n).

Given such a language, does it admit of a complete proof theory?

Less technospeak, more accuracy. I read 'nondenumerable' as 'uncountably infinite'... do you mean countable or uncountable infinities when you say the 'number of symbols is uncountable'? Which 'symbols' are you talking about? Saying something is 'countable' in mathematical terms does not mean it is finite, which I think might be confusing your description.

If you have a finite number of rules/symbols, but your inputs are of an arbitrary (and potentially infinite) length, then yes, you should be able to guarantee solvability/decidability (at least for languages in the Chomsky Language Hierarchy). However, you cannot guarantee a bounded runtime -- essentially, this reduces to trying to solve the halting problem.

 

[nortexoid]

There really isn't anything inaccurate in what I wrote. To be clearer, 'denumerable' means countable and 'nondenumerable' means uncountable. If I do not specify being infinite or not, as in "denumerably many symbols", then I am implying the possibility that there be infinitely many (but at most denumerably many). When I say nondenumerable, I just mean having the same cardinality as the set of real numbers.

The symbols I am talking about are the symbols of the language, which include as subsets a set of predicate letters (of arities I specified above--e.g. P_1, P_2,...), a set of function symbols (e.g. f_1,...) and variables (e.g. x_1,...) (with arities for the function symbols as indicated above), a set of sufficient logical constants (e.g. ~, &), and possibly {(,)}. (The parentheses aren't needed if we define our formation rules such that formulas are given by ordered pairs--e.g. (A & B) = <A,<&,B>>.)

Your comment "If you have a finite number of rules/symbols, but your inputs are of an arbitrary (and potentially infinite) length, then yes, you should be able to guarantee solvability/decidability (at least for languages in the Chomsky Language Hierarchy)" seems incorrect, depending on what you mean by the parenthetical remark. We know that classical first-order predicate logic with predicates of arity n>1 is undecidable. Specifically, it is only semidecidable (i.e. the decision problem for validity is semidecidable.)

I get the bounded runtime part, but how does that reduce to solving the halting problem (which is unsolvable)?

 

[Matthias99]

Originally posted by: nortexoid
There really isn't anything inaccurate in what I wrote. To be clearer, 'denumerable' means countable and 'nondenumerable' means uncountable. If I do not specify being infinite or not, as in "denumerably many symbols", then I am implying the possibility that there be infinitely many (but at most denumerably many). When I say nondenumerable, I just mean having the same cardinality as the set of real numbers.

I didn't say it was inaccurate, just confusing.

Why not just call them 'countably infinite' and 'uncountably infinite' like the rest of the world?

The symbols I am talking about are the symbols of the language, which include as subsets...

Okay, so by 'symbols' you meant 'predicates' or 'any logical construct in the language'. The sentence was vague (so I wasn't sure if you were referring to just variables/constants, or any 'symbols').

Your comment "If you have a finite number of rules/symbols, but your inputs are of an arbitrary (and potentially infinite) length, then yes, you should be able to guarantee solvability/decidability (at least for languages in the Chomsky Language Hierarchy)" seems incorrect, depending on what you mean by the parenthetical remark. We know that classical first-order predicate logic with predicates of arity n>1 is undecidable. Specifically, it is only semidecidable (i.e. the decision problem for validity is semidecidable.)

Hmm... good point. If you're allowing arbitrarily complex predicates, that does screw with things. I guess I was thinking more in terms of semidecidability/provability than true decidability, since looking at it again, it's definitely not going to work for all rulesets.

If your input length is potentially unbounded, you definitely cannot guarantee a bounded decidability runtime on a Turing Machine (or computation equivalent), even if you can guarantee decidability. The only way you could is if your runtime was constant (which would require that the rules not actually depend on the input).

Also, looking at your OP again, I'm *really* not sure how you would define a predicate with infinite arity and not have *that* take an unbounded amount of time to compute (unless it is a fairly trivial predicate, or you assume that they can all be computed in constant time or something).

I get the bounded runtime part, but how does that reduce to solving the halting problem (which is unsolvable)?

Basically, if you had a machine/algorithm that could decide on such languages in bounded time, you could solve the halting problem. At least, IIRC and I'm not screwing up. It's been a while since I've had to do anything this stupidly theoretical involving computational complexity, and computational theory was never my strong suit.