Логика второго порядка

В логике и математике является логика второго порядка расширением логики первого порядка , которая сама является расширением логики высказываний . Логика второго порядка, в свою очередь, расширяется логикой высшего порядка и теорией типов .

Логика первого порядка дает количественную оценку только переменным, которые варьируются в пределах индивидуумов (элементы области дискурса ); логика второго порядка, кроме того, количественно оценивает отношения . второго порядка Например, предложение $\forall P\,\forall x(Px\lor \neg Px)$ говорит, что для каждой формулы P и каждого отдельного x либо Px истинно, либо нет ( Px ) истинно (это закон исключенного третьего ). Логика второго порядка также включает количественную оценку множеств , функций и других переменных (см. раздел ниже ). Логика как первого, так и второго порядка использует идею области дискурса (часто называемой просто «областью» или «вселенной»). Домен представляет собой набор, в котором отдельные элементы могут быть оценены количественно.

Примеры

Граффити в Нойкёльне (Берлин), изображающее простейшее предложение второго порядка, допускающее нетривиальные модели, «∃𝜑𝜑».

Логика первого порядка может оценивать индивидов, но не свойства. То есть мы можем взять атомарное предложение , такое как Cube( b ), и получить квантифицированное предложение, заменив имя переменной и присоединив квантор:

∃ х Куб( х )

Однако мы не можем сделать то же самое с предикатом. То есть следующее выражение:

∃ПП( б )

не является предложением логики первого порядка, но это законное предложение логики второго порядка. Здесь P — переменная-предикат и семантически представляет собой набор индивидов.

В результате логика второго порядка обладает большей выразительной силой, чем логика первого порядка. Например, в логике первого порядка невозможно идентифицировать множество всех кубов и тетраэдров. Но существование этого множества можно утверждать в логике второго порядка как:

∃P ∀ x (Px ↔ (Куб( x ) ∨ Tet( x ))).

Затем мы можем утверждать свойства этого набора. Например, следующее говорит о том, что множество всех кубов и тетраэдров не содержит додекаэдров:

∀P (∀ x (Px ↔ (Cube( x ) ∨ Tet( x ))) → ¬ ∃ x (Px ∧ Dodec( x ))).

Количественная оценка второго порядка особенно полезна, поскольку она дает возможность выразить свойства достижимости . Например, если Parent( x , y ) обозначает, что является родителем y , то логика первого порядка не может выразить свойство, что x является предком y x . В логике второго порядка мы можем выразить это, сказав, что каждое множество людей, содержащее y и замкнутое по отношению Parent, содержит x :

∀P ((P y ∧ ∀ a ∀ b ((P b ∧ Parent(a, b)) → Pa ) ) → P x ).

Примечательно, что, хотя у нас есть переменные для предикатов в логике второго порядка, у нас нет переменных для свойств предикатов. Мы не можем, например, сказать, что существует свойство Shape( P ), которое верно для предикатов P Cube, Tet и Dodec. Для этого потребуется логика третьего порядка .

Синтаксис и фрагменты

Синтаксис логики второго порядка определяет, какие выражения являются правильно составленными формулами . В дополнение к синтаксису логики первого порядка , логика второго порядка включает множество новых видов (иногда называемых типами ) переменных. Это:

• Своего рода переменные, которые варьируются в зависимости от множества людей. Если S — переменная такого типа, а t — член первого порядка, то выражение t ∈ S (также пишется как S ( t ) или St для сохранения круглых скобок) является атомарной формулой . Наборы индивидуумов также можно рассматривать как унарные отношения в области.
• Для каждого натурального числа k существует своего рода переменные, которые распространяются на все k -арные отношения между индивидами. Если R является такой k -арной переменной отношения и t ₁ ,..., t _k являются членами первого порядка, то выражение R ( t ₁ ,..., t _k ) является атомарной формулой.
• Для каждого натурального числа k существует своего рода переменные, которые охватывают все функции, принимающие k элементов области определения и возвращающие один элемент области определения. Если f является такой k -арной функциональной переменной и t ₁ ,..., t _k являются членами первого порядка, то выражение f ( t ₁ ,..., t _k ) является термином первого порядка.

Каждая из только что определенных переменных может быть подвергнута универсальной и/или экзистенциальной количественной оценке для построения формул. Таким образом, существует множество видов кванторов, по два для каждого вида переменных. Предложение в логике второго порядка, как и в логике первого порядка, представляет собой правильно построенную формулу без свободных переменных (любого рода).

В приведенном выше определении можно отказаться от введения функциональных переменных (и некоторые авторы это делают), поскольку n -арная функциональная переменная может быть представлена ​​переменной отношения арности n +1 и соответствующей формулой уникальности " результат" в аргументе n +1 отношения. (Шапиро 2000, стр. 63)

Монадическая логика второго порядка (MSO) — это ограничение логики второго порядка, в котором разрешена только количественная оценка унарных отношений (т. е. множеств). Таким образом, количественная оценка функций из-за эквивалентности описанным выше отношениям также не допускается. Логику второго порядка без этих ограничений иногда называют полной логикой второго порядка, чтобы отличить ее от монадической версии. Монадическая логика второго порядка особенно используется в контексте теоремы Курселя , алгоритмической мета-теоремы в теории графов . Теория MSO полного бесконечного двоичного дерева ( S2S ) разрешима. Напротив, полная логика второго порядка над любым бесконечным множеством (или логика MSO, например ( $\mathbb {N}$,+)) может интерпретировать истинную арифметику второго порядка .

Как и в логике первого порядка, логика второго порядка может включать в себя нелогические символы определенного языка второго порядка. Однако они ограничены тем, что все термины, которые они образуют, должны быть либо терминами первого порядка (которые могут быть заменены на переменную первого порядка), либо терминами второго порядка (которые могут быть заменены на переменную второго порядка соответствующий сорт).

A formula in second-order logic is said to be of first-order (and sometimes denoted $\Sigma _{0}^{1}$ или $\Pi _{0}^{1}$), если его кванторы (которые могут быть универсальными или экзистенциальными) распространяются только на переменные первого порядка, хотя у него могут быть свободные переменные второго порядка. А $\Sigma _{1}^{1}$ Формула (экзистенциального второго порядка) - это формула, дополнительно имеющая некоторые кванторы существования над переменными второго порядка, т.е. $\exists R_{0}\ldots \exists R_{m}\phi$, где $\phi$ является формулой первого порядка. Фрагмент логики второго порядка, состоящий только из экзистенциальных формул второго порядка, называется экзистенциальной логикой второго порядка и сокращенно ЭСО, т.е. $\Sigma _{1}^{1}$или даже как ∃SO. Фрагмент $\Pi _{1}^{1}$ formulas is defined dually, it is called universal second-order logic. More expressive fragments are defined for any k > 0 by mutual recursion: $\Sigma _{k+1}^{1}$ has the form $\exists R_{0}\ldots \exists R_{m}\phi$, where $\phi$ is a $\Pi _{k}^{1}$ formula, and similar, $\Pi _{k+1}^{1}$ has the form $\forall R_{0}\ldots \forall R_{m}\phi$, where $\phi$ is a $\Sigma _{k}^{1}$ formula. (See analytical hierarchy for the analogous construction of second-order arithmetic.)

Semantics

The semantics of second-order logic establish the meaning of each sentence. Unlike first-order logic, which has only one standard semantics, there are two different semantics that are commonly used for second-order logic: standard semantics and Henkin semantics. In each of these semantics, the interpretations of the first-order quantifiers and the logical connectives are the same as in first-order logic. Only the ranges of quantifiers over second-order variables differ in the two types of semantics (Väänänen 2001).

In standard semantics, also called full semantics, the quantifiers range over all sets or functions of the appropriate sort. A model with this condition is called a full model, and these are the same as models in which the range of the second-order quantifiers is the powerset of the model's first-order part. (2001) Thus once the domain of the first-order variables is established, the meaning of the remaining quantifiers is fixed. It is these semantics that give second-order logic its expressive power, and they will be assumed for the remainder of this article.

Leon Henkin (1950) defined an alternative kind of semantics for second-order and higher-order theories, in which the meaning of the higher-order domains is partly determined by an explicit axiomatisation, drawing on type theory, of the properties of the sets or functions ranged over. Henkin semantics is a kind of many-sorted first-order semantics, where there are a class of models of the axioms, instead of the semantics being fixed to just the standard model as in the standard semantics. A model in Henkin semantics will provide a set of sets or set of functions as the interpretation of higher-order domains, which may be a proper subset of all sets or functions of that sort. For his axiomatisation, Henkin proved that Gödel's completeness theorem and compactness theorem, which hold for first-order logic, carry over to second-order logic with Henkin semantics. Since also the Skolem–Löwenheim theorems hold for Henkin semantics, Lindström's theorem imports that Henkin models are just disguised first-order models.

For theories such as second-order arithmetic, the existence of non-standard interpretations of higher-order domains isn't just a deficiency of the particular axiomatisation derived from type theory that Henkin used, but a necessary consequence of Gödel's incompleteness theorem: Henkin's axioms can't be supplemented further to ensure the standard interpretation is the only possible model. Henkin semantics are commonly used in the study of second-order arithmetic.

Jouko Väänänen (2001) argued that the distinction between Henkin semantics and full semantics for second-order logic is analogous to the distinction between provability in ZFC and truth in V, in that the former obeys model-theoretic properties like the Lowenheim-Skolem theorem and compactness, and the latter has categoricity phenomena. For example, "we cannot meaningfully ask whether the $V$ as defined in $\mathrm {ZFC}$ is the real $V$ . But if we reformalize $\mathrm {ZFC}$ inside $\mathrm {ZFC}$, then we can note that the reformalized $\mathrm {ZFC}$ ... has countable models and hence cannot be categorical."

Expressive power

Second-order logic is more expressive than first-order logic. For example, if the domain is the set of all real numbers, one can assert in first-order logic the existence of an additive inverse of each real number by writing ∀x ∃y (x + y = 0) but one needs second-order logic to assert the least-upper-bound property for sets of real numbers, which states that every bounded, nonempty set of real numbers has a supremum. If the domain is the set of all real numbers, the following second-order sentence (split over two lines) expresses the least upper bound property:

(∀ A) ([(∃ w) (w ∈ A) ∧ (∃ z)(∀ u)(u ∈ A → u ≤ z)]

→ (∃ x)(∀ y)([(∀ w)(w ∈ A → w ≤ x)] ∧ [(∀ u)(u ∈ A → u ≤ y)] → x ≤ y))

This formula is a direct formalization of "every nonempty, bounded set A has a least upper bound." It can be shown that any ordered field that satisfies this property is isomorphic to the real number field. On the other hand, the set of first-order sentences valid in the reals has arbitrarily large models due to the compactness theorem. Thus the least-upper-bound property cannot be expressed by any set of sentences in first-order logic. (In fact, every real-closed field satisfies the same first-order sentences in the signature $\langle +,\cdot ,\leq \rangle$ as the real numbers.)

In second-order logic, it is possible to write formal sentences that say "the domain is finite" or "the domain is of countable cardinality." To say that the domain is finite, use the sentence that says that every surjective function from the domain to itself is injective. To say that the domain has countable cardinality, use the sentence that says that there is a bijection between every two infinite subsets of the domain. It follows from the compactness theorem and the upward Löwenheim–Skolem theorem that it is not possible to characterize finiteness or countability, respectively, in first-order logic.

Certain fragments of second-order logic like ESO are also more expressive than first-order logic even though they are strictly less expressive than the full second-order logic. ESO also enjoys translation equivalence with some extensions of first-order logic that allow non-linear ordering of quantifier dependencies, like first-order logic extended with Henkin quantifiers, Hintikka and Sandu's independence-friendly logic, and Väänänen's dependence logic.

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 restricted to Henkin models satisfying the comprehension and choice axioms.

Non-reducibility to first-order logic

One might attempt to reduce the second-order theory of the real numbers, with full second-order semantics, to the first-order theory in the following way. First expand the domain from the set of all real numbers to a two-sorted domain, with the second sort containing all sets of real numbers. Add a new binary predicate to the language: the membership relation. Then sentences that were second-order become first-order, with the formerly second-order quantifiers ranging over the second sort instead. This reduction can be attempted in a one-sorted theory by adding unary predicates that tell whether an element is a number or a set, and taking the domain to be the union of the set of real numbers and the power set of the real numbers.

But notice that the domain was asserted to include all sets of real numbers. That requirement cannot be reduced to a first-order sentence, as the Löwenheim–Skolem theorem shows. That theorem implies that there is some countably infinite subset of the real numbers, whose members we will call internal numbers, and some countably infinite collection of sets of internal numbers, whose members we will call "internal sets", such that the domain consisting of internal numbers and internal sets satisfies exactly the same first-order sentences as are satisfied by the domain of real numbers and sets of real numbers. In particular, it satisfies a sort of least-upper-bound axiom that says, in effect:

Every nonempty internal set that has an internal upper bound has a least internal upper bound.

Countability of the set of all internal numbers (in conjunction with the fact that those form a densely ordered set) implies that that set does not satisfy the full least-upper-bound axiom. Countability of the set of all internal sets implies that it is not the set of all subsets of the set of all internal numbers (since Cantor's theorem implies that the set of all subsets of a countably infinite set is an uncountably infinite set). This construction is closely related to Skolem's paradox.

Thus the first-order theory of real numbers and sets of real numbers has many models, some of which are countable. The second-order theory of the real numbers has only one model, however.This follows from the classical theorem that there is only one Archimedean complete ordered field, along with the fact that all the axioms of an Archimedean complete ordered field are expressible in second-order logic. This shows that the second-order theory of the real numbers cannot be reduced to a first-order theory, in the sense that the second-order theory of the real numbers has only one model but the corresponding first-order theory has many models.

There are more extreme examples showing that second-order logic with standard semantics is more expressive than first-order logic. There is a finite second-order theory whose only model is the real numbers if the continuum hypothesis holds and that has no model if the continuum hypothesis does not hold (cf. Shapiro 2000, p. 105). This theory consists of a finite theory characterizing the real numbers as a complete Archimedean ordered field plus an axiom saying that the domain is of the first uncountable cardinality. This example illustrates that the question of whether a sentence in second-order logic is consistent is extremely subtle.

Additional limitations of second-order logic are described in the next section.

Metalogical results

It is a corollary of Gödel's incompleteness theorem that there is no deductive system (that is, no notion of provability) for second-order formulas that simultaneously satisfies these three desired attributes:

• (Soundness) Every provable second-order sentence is universally valid, i.e., true in all domains under standard semantics.
• (Completeness) Every universally valid second-order formula, under standard semantics, is provable.
• (Effectiveness) There is a proof-checking algorithm that can correctly decide whether a given sequence of symbols is a proof or not.

This corollary is sometimes expressed by saying that second-order logic does not admit a complete proof theory. In this respect second-order logic with standard semantics differs from first-order logic; Quine (1970, pp. 90–91) pointed to the lack of a complete proof system as a reason for thinking of second-order logic as not logic, properly speaking.

As mentioned above, Henkin proved that the standard deductive system for first-order logic is sound, complete, and effective for second-order logic with Henkin semantics, and the deductive system with comprehension and choice principles is sound, complete, and effective for Henkin semantics using only models that satisfy these principles.

The compactness theorem and the Löwenheim–Skolem theorem do not hold for full models of second-order logic. They do hold however for Henkin models.

History and disputed value

Predicate logic was introduced to the mathematical community by C. S. Peirce, who coined the term second-order logic and whose notation is most similar to the modern form (Putnam 1982). However, today most students of logic are more familiar with the works of Frege, who published his work several years prior to Peirce but whose works remained less known until Bertrand Russell and Alfred North Whitehead made them famous. Frege used different variables to distinguish quantification over objects from quantification over properties and sets; but he did not see himself as doing two different kinds of logic. After the discovery of Russell's paradox it was realized that something was wrong with his system. Eventually logicians found that restricting Frege's logic in various ways—to what is now called first-order logic—eliminated this problem: sets and properties cannot be quantified over in first-order logic alone. The now-standard hierarchy of orders of logics dates from this time.

It was found that set theory could be formulated as an axiomatized system within the apparatus of first-order logic (at the cost of several kinds of completeness, but nothing so bad as Russell's paradox), and this was done (see Zermelo–Fraenkel set theory), as sets are vital for mathematics. Arithmetic, mereology, and a variety of other powerful logical theories could be formulated axiomatically without appeal to any more logical apparatus than first-order quantification, and this, along with Gödel and Skolem's adherence to first-order logic, led to a general decline in work in second (or any higher) order logic.

This rejection was actively advanced by some logicians, most notably W. V. Quine. Quine advanced the view that in predicate-language sentences like Fx the "x" is to be thought of as a variable or name denoting an object and hence can be quantified over, as in "For all things, it is the case that . . ." but the "F" is to be thought of as an abbreviation for an incomplete sentence, not the name of an object (not even of an abstract object like a property). For example, it might mean " . . . is a dog." But it makes no sense to think we can quantify over something like this. (Such a position is quite consistent with Frege's own arguments on the concept-object distinction). So to use a predicate as a variable is to have it occupy the place of a name, which only individual variables should occupy. This reasoning has been rejected by George Boolos.

In recent years second-order logic has made something of a recovery, buoyed by Boolos' interpretation of second-order quantification as plural quantification over the same domain of objects as first-order quantification (Boolos 1984). Boolos furthermore points to the claimed nonfirstorderizability of sentences such as "Some critics admire only each other" and "Some of Fianchetto's men went into the warehouse unaccompanied by anyone else", which he argues can only be expressed by the full force of second-order quantification. However, generalized quantification and partially ordered (or branching) quantification may suffice to express a certain class of purportedly nonfirstorderizable sentences as well and these do not appeal to second-order quantification.

Relation to computational complexity

The expressive power of various forms of second-order logic on finite structures is intimately tied to computational complexity theory. The field of descriptive complexity studies which computational complexity classes can be characterized by the power of the logic needed to express languages (sets of finite strings) in them. A string w = w₁···w_n in a finite alphabet A can be represented by a finite structure with domain D = {1,...,n}, unary predicates P_a for each a ∈ A, satisfied by those indices i such that w_i = a, and additional predicates that serve to uniquely identify which index is which (typically, one takes the graph of the successor function on D or the order relation <, possibly with other arithmetic predicates). Conversely, the Cayley tables of any finite structure (over a finite signature) can be encoded by a finite string.

This identification leads to the following characterizations of variants of second-order logic over finite structures:

• REG (the regular languages) is the set of languages definable by monadic, second-order formulas (Büchi-Elgot-Trakhtenbrot theorem, 1960)
• NP is the set of languages definable by existential, second-order formulas (Fagin's theorem, 1974).
• co-NP is the set of languages definable by universal, second-order formulas.
• PH is the set of languages definable by second-order formulas.
• PSPACE is the set of languages definable by second-order formulas with an added transitive closure operator.
• EXPTIME is the set of languages definable by second-order formulas with an added least fixed point operator.

Relationships among these classes directly impact the relative expressiveness of the logics over finite structures; for example, if PH = PSPACE, then adding a transitive closure operator to second-order logic would not make it any more expressive over finite structures.

See also

• First-order logic
• Higher-order logic
• Löwenheim number
• Omega language
• Second-order propositional logic
• Monadic second-order logic

References

• Andrews, Peter (2002). An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof (2nd ed.). Kluwer Academic Publishers.
• Boolos, George (1984). "To Be Is To Be a Value of a Variable (or to Be Some Values of Some Variables)". Journal of Philosophy. 81 (8): 430–50. doi:10.2307/2026308. JSTOR 2026308.. Reprinted in Boolos, Logic, Logic and Logic, 1998.
• Henkin, L. (1950). "Completeness in the theory of types". Journal of Symbolic Logic. 15 (2): 81–91. doi:10.2307/2266967. JSTOR 2266967. S2CID 36309665.
• Hinman, P. (2005). Fundamentals of Mathematical Logic. A K Peters. ISBN 1-56881-262-0.
• Putnam, Hilary (1982). "Peirce the Logician". Historia Mathematica. 9 (3): 290–301. doi:10.1016/0315-0860(82)90123-9.. Reprinted in Putnam, Hilary (1990), Realism with a Human Face, Harvard University Press, pp. 252–260.
• W. V. Quine (1970). Philosophy of Logic. Prentice Hall. ISBN 9780674665637.
• Rossberg, M. (2004). "First-Order Logic, Second-Order Logic, and Completeness" (PDF). In V. Hendricks; et al. (eds.). First-order logic revisited. Berlin: Logos-Verlag.
• Шапиро, С. (2000) [1991]. Основания без фундаментализма: аргументы в пользу логики второго порядка . Оксфорд: Кларендон Пресс. ISBN  0-19-825029-0 .
• Вяэнянен, Дж. (2001). «Логика второго порядка и основы математики» (PDF) . Бюллетень символической логики . 7 (4): 504–520. CiteSeerX   10.1.1.25.5579 . дои : 10.2307/2687796 . JSTOR   2687796 . S2CID   7465054 .

Дальнейшее чтение

• Гредель, Эрих; Колайтис, Фокион Г.; Либкин Леонид ; Мартен, Маркс; Спенсер, Джоэл ; Варди, Моше Ю .; Венема, Иде; Вайнштейн, Скотт (2007). Теория конечных моделей и ее приложения . Тексты по теоретической информатике. Серия EATCS. Берлин: Springer-Verlag . ISBN  978-3-540-00428-8 . Збл   1133.03001 .

• Вяэнянен, Йоуко. Эдвард Н. Залта (ред.). Логика второго и высшего порядка . Стэнфордская энциклопедия философии (выпуск осенью 2021 г.).