Calculus Of Constituents - A Decidable Fragment Of Second Order PL
We may think of symbolic logic as an attempt of syntactical description of some knowledge. Syntactical level is impor- tant because it is detached from interpretation, i.e. concrete meaning, thus, at least potentially, programable. Here by programmability we actually mean decidability. In logical terms, some formal knowledge (formal theory) is decidable if there is an algorithm which decides whether some sentence of this system is a theorem (formally deducible sentence) or not. In mathematics, the most common formalism is a first order predicate calculus. This is not a single formalism, but rather a nice framework that allows an axiomatization of various parts of mathematics, such as Boolean algebras, groups, fields, vector spaces etc. Such formalizations are called a first order theories.