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.

Definition of Hilbert-type infinitary logics

A first-order infinitary language Lα,β, α regular, β = 0 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:

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 .

A theory T in infinitary language is a set of sentences in the logic. A proof in infinitary logic from a theory T is a (possibly infinite) sequence of statements that obeys the following conditions: Each statement is either a logical axiom, an element of T, 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:

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, [5] 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. [6] [ better source needed ] These three theories can be defined without the use of infinite quantification; only infinite junctions [7] are needed.

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

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 mathematics, particularly in linear algebra, tensor analysis, and differential geometry, the Levi-Civita symbol or Levi-Civita epsilon represents a collection of numbers; defined from the sign of a permutation of the natural numbers 1, 2, ..., n, for some positive integer n. It is named after the Italian mathematician and physicist Tullio Levi-Civita. Other names include the permutation symbol, antisymmetric symbol, or alternating symbol, which refer to its antisymmetric property and definition in terms of permutations.

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 theoretical physics, the Rarita–Schwinger equation is the relativistic field equation of spin-3/2 fermions in a four-dimensional flat spacetime. It is similar to the Dirac equation for spin-1/2 fermions. This equation was first introduced by William Rarita and Julian Schwinger in 1941.

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.

In theoretical physics, a source field is a background field coupled to the original field as

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.

In quantum field theory, and especially in quantum electrodynamics, the interacting theory leads to infinite quantities that have to be absorbed in a renormalization procedure, in order to be able to predict measurable quantities. The renormalization scheme can depend on the type of particles that are being considered. For particles that can travel asymptotically large distances, or for low energy processes, the on-shell scheme, also known as the physical scheme, is appropriate. If these conditions are not fulfilled, one can turn to other schemes, like the minimal subtraction scheme.

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 theoretical physics, more specifically in quantum field theory and supersymmetry, supersymmetric Yang–Mills, also known as super Yang–Mills and abbreviated to SYM, is a supersymmetric generalization of Yang–Mills theory, which is a gauge theory that plays an important part in the mathematical formulation of forces in particle physics.

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. S2CID   115693908.
  2. Kanamori, Akihiro (2004). "Zermelo and set theory" (PDF). The Bulletin of Symbolic Logic. 10 (4): 487–553. doi:10.2178/bsl/1102083759. S2CID   231795240 . 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. S2CID   7900557 . Retrieved 1 March 2024.
  4. Karp 1964, pp. 39–54.
  5. 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 . S2CID   120348873 .
  6. Rosinger, Elemer E. (2010). "Four departures in Mathematics and Physics". arXiv: 1003.0360 . CiteSeerX   10.1.1.760.6726 . S2CID   17446826 .
  7. Bennett, David W. (1980). "Junctions". Notre Dame Journal of Formal Logic . 21 (1): 111–118. doi: 10.1305/ndjfl/1093882943 . S2CID   218839738 .
  8. 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