Talk:Infinitary logic

Hilbert-type infinitary logic

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

$\{\land _{\gamma <\delta }[\land _{\beta <\gamma }(A_{\beta })]\implies A_{\gamma }\}\implies \land _{\epsilon <\delta }A_{\epsilon }$

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

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

In my opinion it may be helpful if some historical information about the logics ${\mathcal {L}}_{\alpha \beta }$ 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 ${\mathcal {L}}_{\alpha \beta }$ 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 $a$,$b$ do there exist definable complete formal systems for formulas of length less than $a$ in which fewer than $b$ variables can be quantified at a time?" in the preface to Languages with expressions of infinite length (1964). This book uses the ${\mathcal {L}}_{\alpha \beta }$ notation, and mentions Hilbert-style formal systems for proof (with discussion on sets of axioms and rules of inference). However the infinitary logic ${\mathcal {L}}_{\alpha \beta }$ 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 ${\mathcal {L}}_{\kappa \lambda }$ 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 ${\mathcal {L}}$-notation is not introduced, only the logics that are now called ${\mathcal {L}}_{\alpha \alpha }$ 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 ${\mathcal {L}}_{\alpha \beta }$. As the notation ${\mathcal {L}}_{\alpha \alpha }$ 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)