First of all, I would like to say that I've only recently started researching infinitary logics. I have read some segments of Barwise - related papers on the topic, and I could not find anything discussing 'uncountable logics' (logic's that allow formulae of uncountable length) within them. I am aware of basic properties of infinitary logics being that it fails to prove 'standard' compactness and completeness (a stronger definition is required for infinitary logics, https://en.wikipedia.org/wiki/Infinitary_logic), but what properties would be unique to an uncountable logic?
For specificity, this is the type of uncountable languages I am talking about (Lω2,ω2).
I have never seen the above logic referenced before so I also wonder is there something wrong with this type of logic that I haven't found out? Or that this something that just hasn't been studied enough yet?
Theoretically, since we can always have 'greater' logics that allow for longer formulae, I would like to present the idea of an 'ultimate logic'. The logic would look something like this (LΩ ,Ω) and would would be able to 'define' (in that the Godel coding's for such formulas are elements of the language) all possible formulae within logic (via allowing formulae of any length). My second question is that, could we one day hope to create an 'all defining' logic?
EDIT: The 'ultimate language' that allows for formulae of any ordinal length is L∞,∞. But are there any known theories based off of this language?