June 2001
Intermediate to advanced
2128 pages
82h 43m
English
By Herbrand's theorem, every valid sequent containing weak quantifiers only defines a corresponding Herbrand sequent; thus, Herbrand complexity is well-defined. Still,
can be defined in several ways—depending on our choice of a complexity measure for sequents (an alternative would be to define ‖S‖ as the number of symbol occurrences in the sequent S). As skolemization is a method of removing strong quantifiers, any sequent resulting from a valid one has a Herbrand complexity. The following theorem shows that different forms of skolemization may yield sequents with strongly different Herbrand complexity.
Read now
Unlock full access