The predicate calculus is the dominant system of modern logic, having displaced the traditional Aristotelian syllogistic logic that had been the previous paradigm. Like Aristotle’s, it is a logic of quantifiers – words like ‘every’, ‘some’ and ‘no’ that are used to express that a predicate applies universally or with some other distinctive kind of generality, for example ‘everyone is mortal’, ‘someone is mortal’, ‘no one is mortal’. The weakness of syllogistic logic was its inability to represent the structure of complex predicates. Thus it could not cope with argument patterns like ‘everything Fs and Gs, so everything Fs’. Nor could it cope with relations, because a logic of relations must be able to analyse cases where a quantifier is applied to a predicate that already contains one, as in ‘someone loves everyone’. Remedying the weakness required two major innovations.
One was a logic of connectives – words like ‘and’, ‘or’ and ‘if’ that form complex sentences out of simpler ones. It is often studied as a distinct system: the propositional calculus. A proposition here is a true-or-false sentence and the guiding principle of propositional calculus is truth-functionality, meaning that the truth-value (truth or falsity) of a compound proposition is uniquely determined by the truth-values of its components. Its principal connectives are negation, conjunction, disjunction and a ‘material’ (that is, truth-functional) conditional. Truth-functionality makes it possible to compute the truth-values of propositions of arbitrary complexity in terms of their basic propositional constituents, and so develop the logic of tautology and tautological consequence (logical truth and consequence in virtue of the connectives).
The other invention was the quantifier-variable notation. Variables are letters used to indicate things in an unspecific way; thus ‘x is mortal’ is read as predicating of an unspecified thing x what ‘Socrates is mortal’ predicates of Socrates. The connectives can now be used to form complex predicates as well as propositions, for example ‘x is human and x is mortal’; while different variables can be used in different places to express relational predicates, for example ‘x loves y’. The quantifier goes in front of the predicate it governs, with the relevant variable repeated beside it to indicate which positions are being generalized. These radical departures from the idiom of quantification in natural languages are needed to solve the further problem of ambiguity of scope. Compare, for example, the ambiguity of ‘someone loves everyone’ with the unambiguous alternative renderings ‘there is an x such that for every y, x loves y’ and ‘for every y, there is an x such that x loves y’.
The result is a pattern of formal language based on a non-logical vocabulary of names of things and primitive predicates expressing properties and relations of things. The logical constants are the truth-functional connectives and the universal and existential quantifiers, plus a stock of variables construed as ranging over things. This is ‘the’ predicate calculus. A common option is to add the identity sign as a further logical constant, producing the predicate calculus with identity. The first modern logic of quantification, Frege’s of 1879, was designed to express generalizations not only about individual things but also about properties of individuals. It would nowadays be classified as a second-order logic, to distinguish it from the first-order logic described above. Second-order logic is much richer in expressive power than first-order logic, but at a price: first-order logic can be axiomatized, second-order logic cannot.
SUBFORMULA AND SEPARATION PROPERTIES IN NATURAL DEDUCTION VIA SMALL KRIPKE MODELS
