I'm curious where you studied; I also took a semester course on "logic and computability" where the main text we read was 'Godel, Escher, Bach'
We briefly talked about Godel's proofs, but they are nontrivial. Henkin's proof of completeness is hard enough[1]. I don't mean to sound dismissive, but a class where Godel, Escher, Bach is the text does not seem very rigorous. Logic is very tricky stuff. And once you get into infinities, it's not even intuitive.
[1] https://www.cs.nmsu.edu/historical-projects/Projects/complet...
To answer your question, I went to one of the so-called "elite" American colleges that still has a primarily classical/analytic philosophy program (as opposed to what is known as a "Continental" program). Would rather not say which one, but I was able to take some great logic courses through the philo department.
We used Godel's work directly, and if memory serves also some Goldfarb.
https://www.amazon.com/Computability-Logic-George-S-Boolos/d...
https://github.com/FormalTheology/GoedelGod
Now we just wait for someone to code a proof of Erdos' Supreme Fascist..
The main problem with ontological arguments (and why, even as a Christian, I don't like them) is because they seem to embed the conclusion in their first premise. E.g.: the possibility of a maximally great being seems to definitionally imply its necessity. Why? Because such a being B must have some properties P = { ? ? ? ... }. We may not be sure what's inside P, but we know, with absolute certainty, that existence is in there.
Kant would disagree. He thinks that existence is not a property. This is a rare case when I think he's right.
One of my favourite tongue-in-cheeek replies I read to these ontological arguments: Ah, but surely there is no greater being than one who could create the universe despite not existing!
But that is also true of the informal rhetorical arguments that are more common in (christian) apologetics.
The gift of formal proofs is that they make explicit and unavoidable this embedding of conclusion in premise, which is fundamental to all (epistemologically rational) apologetics
It might be true of all ontological arguments, but certainly not all apologetic arguments.
One of the professors also had a very old newspaper clipping taped up (it was brown then and that was quite a while ago), about several mathematicians committing suicide in the wake of those proofs. I've looked for corroboration of this and have never found it. A bit difficult to comprehend from a modern perspective, but more plausible with an appreciation of the 19th Century faith in rationalism / logical positivism that Godel helped overturn.
Not many people are aware that Godel spent much of his life secretly working on a modern update of an ontological argument for God's existence, and didn't reveal this until late in life -- https://en.wikipedia.org/wiki/G%C3%B6del%27s_ontological_pro...