Computability by Monadic Second-Order Logic

TL;DR

This paper establishes that a binary relation on graphs is recursively enumerable if and only if it can be defined by a monadic second-order logic formula, linking logical definability with computability.

Contribution

It provides a characterization of recursively enumerable graph relations through monadic second-order logic, connecting logic and computability theory.

Findings

Recursively enumerable graph relations are exactly those definable by monadic second-order logic.

The paper formalizes how logical formulas correspond to computational processes on graphs.

It bridges the gap between logical definability and algorithmic computability for graph relations.

Abstract

A binary relation on graphs is recursively enumerable if and only if it can be computed by a formula in monadic second-order logic. The latter means that the formula defines a set of graphs, in the usual way, such that each "computation graph" in that set determines a pair consisting of an input graph and an output graph.