Hilbert-type infinitary logic

edit

I've unmathified the definition of Lα,β, but there are some other problems in that section. "\implies", although the logical (pardon the pun) symbol, seems much too large. "\rightarrow" or "\Rightarrow" should be adequate. Also, transfinite induction might be a derived theorem schema

 

I'll get it right, eventually. — Arthur Rubin (talk) 08:20, 24 February 2011 (UTC)Reply

Origin of terminology "Hilbert-type infinitary logic" and L notation

edit

In my opinion it may be helpful if some historical information about the logics   were included. There is also no source for the use of the name "Hilbert-type" that I could immediately find. What are some citations that contain where and when the logics   originated from, and that explain the etymology of the name "Hilbert-type infinitary logic"?

Some possible leads:

  • Work of Karp in the 1950s and 60s seems to be central to the development of the theory of these logics. Karp's central problem was phrased as "For which cardinals  ,  do there exist definable complete formal systems for formulas of length less than   in which fewer than   variables can be quantified at a time?" in the preface to Languages with expressions of infinite length (1964). This book uses the   notation, and mentions Hilbert-style formal systems for proof (with discussion on sets of axioms and rules of inference). However the infinitary logic   itself might not be called Hilbert-type.
  • In Gloede's "Set theory in infinitary languages" (In Proceedings of the International Summer Institute and Logic Colloquium, Kiel 1974, Lecture Notes in Mathematics vol. 499), there is the quote "the languages   of KARP 1964".
  • In "A formal system of first-order predicate calculus with infinitely long expressions" by S. Maehara and G. Takeuti (1961, Project Euclid link), the  -notation is not introduced, only the logics that are now called   appear to be studied, while these logics are not called "Hilbert-type infinitary logics". It contains the quote "The first-order predicate calculus with infinitely long expressions is being developed by Berkeley school" on the origins of presumably the logics that are now called  . As the notation   is not used, maybe the notation did not exist (or at least was not known to Maehara and Takeuti) in 1961. C7XWiki (talk) 21:44, 15 March 2024 (UTC)Reply