Kalküle

Zusammenfassung

Daß die Quantorenlogik (und als Teil davon die Junktorenlogik) kalkülisiert werden kann, ist eine relativ späte Entdeckung. Sie gründet sich auf die Erkenntnis, daß die Begriffe der Ableitung aus Prämissen und des Beweises vollständig formalisierbar sind. Darunter ist die Tatsache zu verstehen, daß formale Ableitungen und Beweise nur auf die äußere, rein syntaktisch beschreibbare Gestalt der beteiligten Sätze Bezug nehmen. Darüber hinaus wird allgemein vorausgesetzt, daß es sich bei Ableitungen und Beweisen um entscheidbare Eigenschaften von Ausdrucksfolgen handelt, so daß man es prinzipiell einer Maschine überlassen könnte, festzustellen, ob eine angebliche Ableitung auch eine tatsächliche Ableitung bzw. ein angeblicher Beweis auch ein tatsächlicher Beweis ist. Die Entscheidbarkeit wird dadurch gewährleistet, daß Ableitungen bzw. Beweise sich aus elementaren Schritten zusammensetzen, wobei jeder dieser Schritt ein Anwendungsfall einer formalen Regel ist. ,Formale Regel‘ ist hierbei gleichbedeutend mit ,syntaktische Regel‘; denn eine derartige Regel hat stets die allgemeine Gestalt ,von Ausdrücken solcher und solcher syntaktischer Struktur darf man zu einem Ausdruck von der und der syntaktischen Struktur übergehen‘.