Abstract

This is an abstract of my paper \Programs and program verication in a general setting" submitted to Theoretical Computer Science.! denotes the set of natural numbers. Let X = fxi : i 2!g be the set of variables, Lt be the set of classical rst order formulas of some type t possibly with free variables. Let L n t Lt be the set of formulas the free variables of which are among fxi : i < ng, in particular L 0 t denotes the set of formulas without free variables. Let T L 0 t be a consistent theory.