Deductive Systems
A deductive system for a logic is a set of inference rules and logical axioms that determine which sequences of formulas constitute valid proofs. Several deductive systems can be used for second-order logic, although none can be complete for the standard semantics (see below). Each of these systems is sound, which means any sentence they can be used to prove is logically valid in the appropriate semantics.
The weakest deductive system that can be used consists of a standard deductive system for first-order logic (such as natural deduction) augmented with substitution rules for second-order terms. This deductive system is commonly used in the study of second-order arithmetic.
The deductive systems considered by Shapiro (1991) and Henkin (1950) add to the augmented first-order deductive scheme both comprehension axioms and choice axioms. These axioms are sound for standard second-order semantics. They are sound for Henkin semantics if only Henkin models that satisfy the comprehension and choice axioms are considered.
Read more about this topic: Second-order Logic
Famous quotes containing the word systems:
“The geometry of landscape and situation seems to create its own systems of time, the sense of a dynamic element which is cinematising the events of the canvas, translating a posture or ceremony into dynamic terms. The greatest movie of the 20th century is the Mona Lisa, just as the greatest novel is Gray’s Anatomy.”
—J.G. (James Graham)