Zulip Chat Archive

Stream: new members

Topic: Complexity of a propositional formula

Donald Sebastian Leung (Feb 22 2020 at 05:17):

In the Chapter 7 exercises in "Theorem Proving in Lean", question 4 asks me to define the type of propositional formulas and a function for measuring the complexity of a formula, among other things. What is meant by "complexity of a formula" here?

Floris van Doorn (Feb 22 2020 at 07:15):

Usually it means something like the length of a formula, the number of variables plus the number of logical symbols (like connectives/negations). But it could mean different things, like the depth (how many nested logical connectives are there).

Donald Sebastian Leung (Feb 22 2020 at 07:16):

I see, thanks. So there's no universally accepted definition of "complexity of a formula"?

Floris van Doorn (Feb 22 2020 at 07:21):

I don't think so, but if there was I would guess the number of symbols in it.

Floris van Doorn (Feb 22 2020 at 07:23):

For first-order logic formulas there is a different kind of complexity, which counts the number of quantifier changes (in a certain normal form): https://en.wikipedia.org/wiki/Arithmetical_hierarchy
But this doesn't make sense for propositional formulae, since there are no quantifiers.

Marc Huisinga (Feb 22 2020 at 08:11):

my guess is that it's asking for some kind of evaluation complexity (i.e. how many steps it would take to evaluate the formula), given that it also asks to implement evaluation right before that

Mario Carneiro (Feb 22 2020 at 08:27):

Generally when this term is used it doesn't really matter what it is precisely, as long as it's a natural number and subformulas have smaller complexity

Mario Carneiro (Feb 22 2020 at 08:29):

quantifier alternations is usually called "arithmetic complexity" specifically

Last updated: Dec 20 2023 at 11:08 UTC