任意公理系统的依赖基

形式化定义了值依赖的公理、公理系统及依赖基。严格证明了任何公理系统对任何背景都具有依赖基,给出 了对任意一个公理系统求任意背景依赖基的方法,并证明了每个公理系统的依赖基不唯一。进而还提出了一种诱导 背景,通过诱导背景可把这个证明过程及依赖基的计算过程形象地反映出来。