Declaring a second-order block #

A DescriptiveComplexity.SigmaSODefinable witness guesses its certificate in a DescriptiveComplexity.SOBlock, and its kernel is a sentence over the base vocabulary summed with the block's. Setting that up means an index type with a Fintype instance, the block itself, one ⟨.i, rfl⟩ symbol per relation variable, the summed language, and – for every symbol of the base vocabulary as well – an abbreviation injecting it into the sum. None of that is guessable from the mathematics, and all of it is determined by the arities.

fo_block writes it:

/-- The existential block of Subgraph Isomorphism. -/
fo_block isoGuessBlock over Language.twoGraphs tg into subgraphSOLang with sg where
  /-- The guessed map from the pattern to the host. -/
  map : 2

reads the symbols of Language.twoGraphs out of the environment, and declares IsoGuessBlockIx (with DecidableEq and Fintype), isoGuessBlock, subgraphSOLang, the relation variable sgMapRel, and the symbols of the sum: sgPatVSym, sgHostVSym, sgPatESym, sgHostESym on the left and sgMapSym on the right. The base vocabulary is named with the prefix its symbols carry, so that the command can find tgPatV from the constructor patV; it must therefore have been declared by DescriptiveComplexity.fo_language, or by hand following the same convention.

The generated declarations are the hand-written ones. The index type is a named inductive rather than Unit or Fin k even for a single variable: a numeral does not elaborate at the ι field, and a named constructor is what the ⟨.i, rfl⟩ symbols and the assignment ρ read.

source

def DescriptiveComplexity.foVarDecl :

Lean.ParserDescr

One relation variable of a block: map : 2.

Equations