形式推演

形式推演(formal deduction)模型論的基本概念之一指在語言獷中，從一個公式集合出發到一個公式的推演.如果存在一個有限公式序列必，，}z}...,},}，使得}- }n，並且對每個公式必，它或是一個邏輯公理，或屬於百，或能由次序在前的公式用分離規則或推廣規則推得.這時稱公式滬可以由公式集合藝推出，記為藝卜筍這樣的公式序列}, } }z ,…，必。稱為由藝到滬的一個形式推演(簡稱推演).特別地，如果滬可以由空集推出，則稱滬是一個形式定理，記為卜筍