Infinitary logic

Last updated

An infinitary logic is a logic that allows infinitely long statements and/or infinitely long proofs. [1] The concept was introduced by Zermelo in the 1930s. [2]

Contents

Some infinitary logics may have different properties from those of standard first-order logic. In particular, infinitary logics may fail to be compact or complete. Notions of compactness and completeness that are equivalent in finitary logic sometimes are not so in infinitary logics. Therefore for infinitary logics, notions of strong compactness and strong completeness are defined. This article addresses Hilbert-type infinitary logics, as these have been extensively studied and constitute the most straightforward extensions of finitary logic. These are not, however, the only infinitary logics that have been formulated or studied.

Considering whether a certain infinitary logic named Ω-logic is complete promises to throw light on the continuum hypothesis. [3]

A word on notation and the axiom of choice

As a language with infinitely long formulae is being presented, it is not possible to write such formulae down explicitly. To get around this problem a number of notational conveniences, which, strictly speaking, are not part of the formal language, are used. is used to point out an expression that is infinitely long. Where it is unclear, the length of the sequence is noted afterwards. Where this notation becomes ambiguous or confusing, suffixes such as are used to indicate an infinite disjunction over a set of formulae of cardinality . The same notation may be applied to quantifiers, for example . This is meant to represent an infinite sequence of quantifiers: a quantifier for each where .

All usage of suffixes and are not part of formal infinitary languages.

The axiom of choice is assumed (as is often done when discussing infinitary logic) as this is necessary to have sensible distributivity laws.

Formal languages

A first-order infinitary language , regular, or , has the same set of symbols as a finitary logic and may use all the rules for formation of formulae of a finitary logic together with some additional ones: [4]

The language may also have function, relation, and predicate symbols of finite arity. [5] Karp also defined languages with an infinite cardinal and some more complicated restrictions on that allow for function and predicate symbols of infinite arity, with controlling the maximum arity of a function symbol and controlling predicate symbols. [6]

The concepts of free and bound variables apply in the same manner to infinite formulae. Just as in finitary logic, a formula all of whose variables are bound is referred to as a sentence .

Definition of Hilbert-type infinitary logics

A theory in infinitary language is a set of sentences in the logic. A proof in infinitary logic from a theory is a (possibly infinite) sequence of statements that obeys the following conditions: Each statement is either a logical axiom, an element of , or is deduced from previous statements using a rule of inference. As before, all rules of inference in finitary logic can be used, together with an additional one:

If , forming universal closures may not always be possible, however extra constant symbols may be added for each variable with the resulting satisfiability relation remaining the same. [8] To avoid this, some authors use a different definition of the language forbidding formulas from having more than free variables. [9]

The logical axiom schemata specific to infinitary logic are presented below. Global schemata variables: and such that .

The last two axiom schemata require the axiom of choice because certain sets must be well orderable. The last axiom schema is strictly speaking unnecessary, as Chang's distributivity laws imply it, [10] however it is included as a natural way to allow natural weakenings to the logic.

Completeness, compactness, and strong completeness

A theory is any set of sentences. The truth of statements in models are defined by recursion and will agree with the definition for finitary logic where both are defined. Given a theory T a sentence is said to be valid for the theory T if it is true in all models of T.

A logic in the language is complete if for every sentence S valid in every model there exists a proof of S. It is strongly complete if for any theory T for every sentence S valid in T there is a proof of S from T. An infinitary logic can be complete without being strongly complete.

A cardinal is weakly compact when for every theory T in containing at most many formulas, if every ST of cardinality less than has a model, then T has a model. A cardinal is strongly compact when for every theory T in , without restriction on size, if every ST of cardinality less than has a model, then T has a model.

Concepts expressible in infinitary logic

In the language of set theory the following statement expresses foundation:

Unlike the axiom of foundation, this statement admits no non-standard interpretations. The concept of well-foundedness can only be expressed in a logic that allows infinitely many quantifiers in an individual statement. As a consequence many theories, including Peano arithmetic, which cannot be properly axiomatised in finitary logic, can be in a suitable infinitary logic. Other examples include the theories of non-archimedean fields and torsion-free groups. [11] [ better source needed ] These three theories can be defined without the use of infinite quantification; only infinite junctions [12] are needed.

Truth predicates for countable languages are definable in . [13]

Complete infinitary logics

Two infinitary logics stand out in their completeness. These are the logics of and . The former is standard finitary first-order logic and the latter is an infinitary logic that only allows statements of countable size.

The logic of is also strongly complete, compact and strongly compact.

The logic of fails to be compact, but it is complete (under the axioms given above). Moreover, it satisfies a variant of the Craig interpolation property.

If the logic of is strongly complete (under the axioms given above) then is strongly compact (because proofs in these logics cannot use or more of the given axioms).

Related Research Articles

In differential geometry, the Einstein tensor is used to express the curvature of a pseudo-Riemannian manifold. In general relativity, it occurs in the Einstein field equations for gravitation that describe spacetime curvature in a manner that is consistent with conservation of energy and momentum.

In differential geometry, the Cotton tensor on a (pseudo)-Riemannian manifold of dimension n is a third-order tensor concomitant of the metric. The vanishing of the Cotton tensor for n = 3 is necessary and sufficient condition for the manifold to be locally conformally flat. By contrast, in dimensions n ≥ 4, the vanishing of the Cotton tensor is necessary but not sufficient for the metric to be conformally flat; instead, the corresponding necessary and sufficient condition in these higher dimensions is the vanishing of the Weyl tensor, while the Cotton tensor just becomes a constant times the divergence of the Weyl tensor. For n < 3 the Cotton tensor is identically zero. The concept is named after Émile Cotton.

In differential geometry, a tensor density or relative tensor is a generalization of the tensor field concept. A tensor density transforms as a tensor field when passing from one coordinate system to another, except that it is additionally multiplied or weighted by a power W of the Jacobian determinant of the coordinate transition function or its absolute value. A tensor density with a single index is called a vector density. A distinction is made among (authentic) tensor densities, pseudotensor densities, even tensor densities and odd tensor densities. Sometimes tensor densities with a negative weight W are called tensor capacity. A tensor density can also be regarded as a section of the tensor product of a tensor bundle with a density bundle.

In differential geometry and mathematical physics, a spin connection is a connection on a spinor bundle. It is induced, in a canonical manner, from the affine connection. It can also be regarded as the gauge field generated by local Lorentz transformations. In some canonical formulations of general relativity, a spin connection is defined on spatial slices and can also be regarded as the gauge field generated by local rotations.

Scalar–tensor–vector gravity (STVG) is a modified theory of gravity developed by John Moffat, a researcher at the Perimeter Institute for Theoretical Physics in Waterloo, Ontario. The theory is also often referred to by the acronym MOG.

In mathematics, compact quantum groups are generalisations of compact groups, where the commutative -algebra of continuous complex-valued functions on a compact group is generalised to an abstract structure on a not-necessarily commutative unital -algebra, which plays the role of the "algebra of continuous complex-valued functions on the compact quantum group".

In the mathematical discipline of set theory, there are many ways of describing specific countable ordinals. The smallest ones can be usefully and non-circularly expressed in terms of their Cantor normal forms. Beyond that, many ordinals of relevance to proof theory still have computable ordinal notations. However, it is not possible to decide effectively whether a given putative ordinal notation is a notation or not ; various more-concrete ways of defining ordinals that definitely have notations are available.

The Newman–Penrose (NP) formalism is a set of notation developed by Ezra T. Newman and Roger Penrose for general relativity (GR). Their notation is an effort to treat general relativity in terms of spinor notation, which introduces complex forms of the usual variables used in GR. The NP formalism is itself a special case of the tetrad formalism, where the tensors of the theory are projected onto a complete vector basis at each point in spacetime. Usually this vector basis is chosen to reflect some symmetry of the spacetime, leading to simplified expressions for physical observables. In the case of the NP formalism, the vector basis chosen is a null tetrad: a set of four null vectors—two real, and a complex-conjugate pair. The two real members often asymptotically point radially inward and radially outward, and the formalism is well adapted to treatment of the propagation of radiation in curved spacetime. The Weyl scalars, derived from the Weyl tensor, are often used. In particular, it can be shown that one of these scalars— in the appropriate frame—encodes the outgoing gravitational radiation of an asymptotically flat system.

In the Newman–Penrose (NP) formalism of general relativity, Weyl scalars refer to a set of five complex scalars which encode the ten independent components of the Weyl tensor of a four-dimensional spacetime.

In proof theory, ordinal analysis assigns ordinals to mathematical theories as a measure of their strength. If theories have the same proof-theoretic ordinal they are often equiconsistent, and if one theory has a larger proof-theoretic ordinal than another it can often prove the consistency of the second theory.

In mathematical logic and set theory, an ordinal collapsing function is a technique for defining certain recursive large countable ordinals, whose principle is to give names to certain ordinals much larger than the one being defined, perhaps even large cardinals, and then "collapse" them down to a system of notations for the sought-after ordinal. For this reason, ordinal collapsing functions are described as an impredicative manner of naming ordinals.

In continuum mechanics, a compatible deformation tensor field in a body is that unique tensor field that is obtained when the body is subjected to a continuous, single-valued, displacement field. Compatibility is the study of the conditions under which such a displacement field can be guaranteed. Compatibility conditions are particular cases of integrability conditions and were first derived for linear elasticity by Barré de Saint-Venant in 1864 and proved rigorously by Beltrami in 1886.

The table of chords, created by the Greek astronomer, geometer, and geographer Ptolemy in Egypt during the 2nd century AD, is a trigonometric table in Book I, chapter 11 of Ptolemy's Almagest, a treatise on mathematical astronomy. It is essentially equivalent to a table of values of the sine function. It was the earliest trigonometric table extensive enough for many practical purposes, including those of astronomy. Since the 8th and 9th centuries, the sine and other trigonometric functions have been used in Islamic mathematics and astronomy, reforming the production of sine tables. Khwarizmi and Habash al-Hasib later produced a set of trigonometric tables.

Vasiliev equations are formally consistent gauge invariant nonlinear equations whose linearization over a specific vacuum solution describes free massless higher-spin fields on anti-de Sitter space. The Vasiliev equations are classical equations and no Lagrangian is known that starts from canonical two-derivative Frønsdal Lagrangian and is completed by interactions terms. There is a number of variations of Vasiliev equations that work in three, four and arbitrary number of space-time dimensions. Vasiliev's equations admit supersymmetric extensions with any number of super-symmetries and allow for Yang–Mills gaugings. Vasiliev's equations are background independent, the simplest exact solution being anti-de Sitter space. It is important to note that locality is not properly implemented and the equations give a solution of certain formal deformation procedure, which is difficult to map to field theory language. The higher-spin AdS/CFT correspondence is reviewed in Higher-spin theory article.

In set theory and logic, Buchholz's ID hierarchy is a hierarchy of subsystems of first-order arithmetic. The systems/theories are referred to as "the formal theories of ν-times iterated inductive definitions". IDν extends PA by ν iterated least fixed points of monotone operators.

In mathematics, Rathjen's  psi function is an ordinal collapsing function developed by Michael Rathjen. It collapses weakly Mahlo cardinals to generate large countable ordinals. A weakly Mahlo cardinal is a cardinal such that the set of regular cardinals below is closed under . Rathjen uses this to diagonalise over the weakly inaccessible hierarchy.

In supersymmetry, eleven-dimensional supergravity is the theory of supergravity in the highest number of dimensions allowed for a supersymmetric theory. It contains a graviton, a gravitino, and a 3-form gauge field, with their interactions uniquely fixed by supersymmetry. Discovered in 1978 by Eugène Cremmer, Bernard Julia, and Joël Scherk, it quickly became a popular candidate for a theory of everything during the 1980s. However, interest in it soon faded due to numerous difficulties that arise when trying to construct physically realistic models. It came back to prominence in the mid-1990s when it was found to be the low energy limit of M-theory, making it crucial for understanding various aspects of string theory.

In supersymmetry, type IIA supergravity is the unique supergravity in ten dimensions with two supercharges of opposite chirality. It was first constructed in 1984 by a dimensional reduction of eleven-dimensional supergravity on a circle. The other supergravities in ten dimensions are type IIB supergravity, which has two supercharges of the same chirality, and type I supergravity, which has a single supercharge. In 1986 a deformation of the theory was discovered which gives mass to one of the fields and is known as massive type IIA supergravity. Type IIA supergravity plays a very important role in string theory as it is the low-energy limit of type IIA string theory.

In supersymmetry, type IIB supergravity is the unique supergravity in ten dimensions with two supercharges of the same chirality. It was first constructed in 1983 by John Schwarz and independently by Paul Howe and Peter West at the level of its equations of motion. While it does not admit a fully covariant action due to the presence of a self-dual field, it can be described by an action if the self-duality condition is imposed by hand on the resulting equations of motion. The other types of supergravity in ten dimensions are type IIA supergravity, which has two supercharges of opposing chirality, and type I supergravity, which has a single supercharge. The theory plays an important role in modern physics since it is the low-energy limit of type IIB string theory.

In supersymmetry, type I supergravity is the theory of supergravity in ten dimensions with a single supercharge. It consists of a single supergravity multiplet and a single Yang–Mills multiplet. The full non-abelian action was first derived in 1983 by George Chapline and Nicholas Manton. Classically the theory can admit any gauge group, but a consistent quantum theory resulting in anomaly cancellation only exists if the gauge group is either or . Both these supergravities are realised as the low-energy limits of string theories, in particular of type I string theory and of the two heterotic string theories.

References

  1. Moore, Gregory H. (1997). "The prehistory of infinitary logic: 1885–1955". In Dalla Chiara, Maria Luisa; Doets, Kees; Mundici, Daniele; van Benthem, Johan (eds.). Structures and Norms in Science. Springer-Science+Business Media. pp. 105–123. doi:10.1007/978-94-017-0538-7_7. ISBN   978-94-017-0538-7.
  2. Kanamori, Akihiro (2004). "Zermelo and set theory" (PDF). The Bulletin of Symbolic Logic. 10 (4): 487–553. doi:10.2178/bsl/1102083759 . Retrieved 22 August 2023.
  3. Woodin, W. Hugh (2011). "The Continuum Hypothesis, the generic-multiverse of sets, and the Ω Conjecture". In Kennedy, Juliette; Kossak, Roman (eds.). Set Theory, Arithmetic, and Foundations of Mathematics: Theorems, Philosophies. Cambridge University Press. pp. 13–42. doi:10.1017/CBO9780511910616.003. ISBN   978-0-511-91061-6. Archived from the original on 1 March 2024. Retrieved 1 March 2024.
  4. Karp 1964, pp. 1–2.
  5. Karp 1964, p. 1.
  6. Karp 1964, pp. 101–102.
  7. Karp 1964, pp. 39–54.
  8. Karp 1964, p. 127.
  9. J. L. Bell, "Infinitary Logic". Stanford Encyclopedia of Philosophy, revised 2023. Accessed 26 July 2024.
  10. Chang, C. C. (1957). "On the representation of α-complete Boolean algebras". Transactions of the American Mathematical Society . 85 (1): 208–218. doi: 10.1090/S0002-9947-1957-0086792-1 .
  11. Rosinger, Elemer E. (2010). "Four departures in Mathematics and Physics". arXiv: 1003.0360 . CiteSeerX   10.1.1.760.6726 .
  12. Bennett, David W. (1980). "Junctions". Notre Dame Journal of Formal Logic . 21 (1): 111–118. doi: 10.1305/ndjfl/1093882943 .
  13. Pogonowski, Jerzy (10 June 2010). "Inexpressible longing for the intended model" (PDF). Zakład Logiki Stosowanej. Uniwersytet im. Adama Mickiewicza w Poznaniu. p. 4. Retrieved 1 March 2024.

Sources