形式推演

形式推演(formal deduction)模型论的基本概念之一指在语言犷中，从一个公式集合出发到一个公式的推演.如果存在一个有限公式序列必，，}z}...，}，}，使得}- }n，并且对每个公式必，它或是一个逻辑公理，或属于百，或能由次序在前的公式用分离规则或推广规则推得.这时称公式沪可以由公式集合艺推出，记为艺卜笋这样的公式序列}， } }z ，…，必。