How can one define a set of formulas inductively, without some base propositions being defined first?

79 Views Asked by At

In some contexts (i.e. coalgebraic logic/coalgebraic modal logic) I see people commonly define (coalgebraic) languages (indeed sets of formulas) without considering any atomic propositions (or base formulas, in other words) first. I have never seen like this before this.

How is that even possible? is it common in other branches of logic?

Following you can see a glance from the paper "Expressive logics for coalgebras via terminal sequence induction" by someone expert of the field. Please don't be ignorant to the question just because it is about coalgebras and you have never seen them; this question doesn't seem to have much to do with that: you van even consider the boolean part not the modality, if you don't want the story coalgebraic.

enter image description here

**For those who are curious, $\Lambda$ is a set of predicate liftings for the signature functor.

Thanks.