Complexity of a propositional formula

Stream: new members

[Donald Sebastian Leung]

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]

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]

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

[Floris van Doorn]

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

[Floris van Doorn]

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]

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]

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]

quantifier alternations is usually called "arithmetic complexity" specifically