A~proof scheme in discrete mathematics

Yu. V. Matiyasevich

Zapiski Nauchnykh Seminarov POMI, Studies in constructive mathematics and mathematical logic. Part VI, Tome 40 (1974), pp. 94-100

Résumé

The following scheme is proposed as apossible pattern for proofs in discrete mathematics. Let some property $P$ of discrete objects be fixed and for any object $X$ a formal system $\mathfrak P_x$ be specified such that an object $X$ has the property $P$ if and only if a formula of a certain type (one of so called final formulas) is deducible in $\mathfrak P_x$. To prove the implication $P(X)\Longrightarrow Q(X)$ one can specify a property $Q^*$ (defined on couples $\langle X,P\rangle$ where $P$ is a formula) such that $Q^*$ is posessed by axioms of $\mathfrak P_x$ and is inherited by conclusions of the rules of $\mathfrak P_x$, for every final formula $P$ $Q^*(X,P)$ implies $Q(X)$. A new proof according to this scheme is given to a known theorem in the theory of graph-coloring.