Free variables are counted rather than named: $MSO r s$ is the type of formulas with $r$ free vertex variables and $s$ free set variables, and a quantifier turns a formula with one more free variable of its kind into a formula with one fewer. Satisfaction is therefore a total function of a formula and two environments, $Fin r → Fin n$ and $Fin s → Set (Fin n)$, one entry per free variable: there is no partial valuation, no default value for an unassigned variable, and no well-formedness side condition. A sentence is a formula of $MSO 0 0$, so being closed is a property of the type rather than a predicate to check. The price is that variables are de Bruijn positions rather than names; the alternative, named variables, needs capture-avoiding substitution inside the trusted definition, which is a considerably worse object to audit than an index.

Variables are levels, not indices: a quantifier extends the environment at its last position ($Fin.snoc$), so the outermost bound variable of a formula is $0$ and the innermost is the last. Nothing in the definition shifts an index.

Only negation, conjunction and existential quantification are constructors. Disjunction, implication and universal quantification are the usual abbreviations, written out where they are used: each of them as a constructor would add a case to the definition of satisfaction and buy nothing that is not already there.

The logic is monadic second-order logic in its MSO₁ form — quantification over vertices and over sets of vertices, with adjacency, equality and membership as the atoms. Sets of edges are not quantified over. This is not a step on the way to a fuller version that was left unfinished: MSO₁ and MSO₂, the logic that also quantifies over edges and sets of edges, are matched to different width measures. MSO₂ model checking is tractable on classes of bounded treewidth and is not tractable on classes of bounded cliquewidth unless the standard complexity assumptions fail, so a development that proved the MSO₁ statement for cliquewidth and then claimed MSO₂ "by the same argument" would be claiming something false. MSO₂ needs its own encoding — the incidence graph, or edge-set variables in the type algebra — and is deferred as one unit, logic and width measure together.