Nichttheoreme

Nichttheoreme Synopsis

Die effektive Erkennung von Nichttheoremen ist das zentrale Problem der Entscheidbarkeit von Theorien. Seit der Arbeit von Church 1936 gilt die (Hypo-)These, dass diese Erkennbarkeit nicht in allen Faellen moeglich ist. Als eine moegliche Forschungsaufgabe bleibt dann die Frage, ob es irgendwelche effektive entscheidbare Kriterien gibt, mittels deren man moeglichst grosse Teilklassen von Formeln als zur Klasse der Theoreme oder als zur Klasse der Nichttheoreme zugehoerig erkennen kann. Insbesondere Kriterien fuer die Zugehoerigkeit zur Klasse der Nichttheoreme waeren fuer automatische Theorembeweiser von grossem praktischen Interesse. In der vorliegenden Arbeit werden Kriterien fuer Nichttheoreme gefunden, die sich ausschliesslich an syntaktischen Eigenschaften von Formeln orientieren. Nebenbei wird der Tableaukalkuel in der Version von Smullyan erstmalig voll formalisiert.