Formal Theories of Occurrences and Substitutions

Abstract

Mathematische Grundlagen und wesentliche Methoden einer formalen Theorie von Vorkommen und Substitutionen werden anhand der Theorie von Vorkommen von Termen in Termen (einer erststufigen formalen Sprache der Logik) eingeführt. Darauf aufbauend werden intuitive Begriffe (etwa Unabhängigkeit von Vorkommen oder mathematische Rechenschritte) formal definiert und so einer mathematischen Argumentation zugänglich gemacht. Es werden exemplarisch Probleme diskutiert, die nur mithilfe einer formalen Theorie von Vorkommen gelöst werden können. Insbesondere wird der Begriff einer (expliziten) Substitutionsfunktion basierend auf dem Begriff der Substitution eingeführt, und es wird gezeigt, inwiefern diese Funktionen mit denen zusammenhängen, die üblicherweise als Substitutionsfunktion bezeichnet werden.