Does a necessary being (or thing) exist?

Clarifying the question
Modal logic is a standardized logic. It is taught in every major university and is used in many disciplines, especially computer science. It is a theorem in standard S5 modal logic that if something is possibly necessary, then it is actually necessary. So if a necessary entity is something that could even possibly exist, in this logicalmetaphysical sense, then per this theorem, it actually does exist: in fact it has to exist.
If that sounds weird at first, you’re not alone. This might help:
Necessary truths vs. contingent truths
Contrast necessary truths with contingent truths. For example, “Romney rather than Obama became the U.S. president” is false, but it is not necessarily false because if things had been different (which really could have been different), then Romney instead could have been president. “Romney became the U.S. president” just happens to be false. It's contingently false. Contrast this with necessary truths like “No squarecircles exist” or “1+1=2”. The latter is a mathematical truth, and all such truths are timeless and necessary. If 1+1=3 is false, then it is necessarily false and no possible change in the world could have made it true. Likewise, if it's true, then it's necessarily true.Epistemic possibility vs. Metaphysical possibility
One open problem in mathematics is Golbach's conjecture, that every even number equal to or greater than 4 is the sum of two prime numbers. From our perspective (i.e. epistemically), Golbach's conjecture may be true or false. We don't know! However, in reality (i.e. metaphysically) it has to be one or the other. And in fact, whichever it is, it is metaphysically necessary that it had to be that. [Note: When philosophers say something is “necessary” without a qualifier, they usually mean mean “metaphysically” necessary.]Putting it together
How does this help us see that possibly necessary entails actually necessary? Well, recall again that if Golbach's conjecture is true then it has to be true, because it is the kind of proposition that is necessarily true or necessarily false. In the same way, “God exists” is the kind of proposition that is necessarily true or necessarily false. Why? Because God is defined as a necessary being. That means that if theism is true, then “Necessarily, God exists”. By contrast, if theism is false, then “Necessarily, God does not exist”. So, “Theism is true” is very much like “Golbach's conjecture is true”. We may not know whether it is true or false, but like 1+1=x, whatever the answer is, it metaphysically could not be otherwise. So if it is metaphysically possible that God does not exist, then necessarily God does not exist. And if it is metaphysically possible that God exists, then metaphysically necessarily God exists.So the big debate today is over whether a necessary being like God is metaphysically possible. Traditional atheists say “no”, while traditional theists say “yes”.

Possibly Necessary implies Actually Necessary (A Proof)
As noted in several sources, for any proposition p, if it is possibly necessary that p is true, then it is necessary that p is true. That is to say, p is not a contingent truth; it is more like 2+2=4 or squarecircles do not exist.^{1}
Definitions:
Let '~' abbreviate 'it is not the case that'.
Let '◊' abbreviate 'it is possible that'.
Let '□' abbreviate 'it is necessary that' (or '~◊~').Axioms (of system S5):
M: □p → p
K: □(p → q) → (□p → □q)
4: □p → □□p
5: ◊p → □◊p“Theorem: If it is possibly necessary that p, then it is necessary that p.”
 ◊~p → □◊~p (5 axiom)
 ◊~p → ~◊~◊~p (Definition of □)
 ~~◊~◊~p → ~◊~p (Contraposition)
 ◊~◊~p → ~◊~p (Double negation)
 ◊□p → □p (Definition of □)^{2}
For example, if it is possible that there is a necessary being (i.e. something such that necessarily, it exists), then there is a necessary being.^{3}
 For example, G.E. Huges & M. J. Cresswell, A New Introduction to Modal Logic (Routledge, 1996), 58.
 This proof is given by Christopher Menzel (Texas A&M University) via Josh Rasmussen (Azusa Pacific University).
 To be technically precise: “There is a necessary being” = “∃x□(x=x)”, which entails “□∃x□(x=x)”.

Turri's Argument from Beginnings
(1): It is possible that the first contingent thing is caused to exist. (Premise)
(2): In the possible case where the first contingent thing is caused to exist, a causally powerful necessary being must cause it to exist. (Premise)
(3): A causally powerful necessary being possibly exists. (From 1 and 2)
(4): A possibly causally powerful necessary being necessarily exists. (From 3, using the S5 theorem from the intro) “A New and Improved Argument for a Necessary Being.” The Australiasian Journal of Philosophy, Vol. 89, No 2. (June 2011): 357359.

A “Sumstyled” Contingency Argument
A “Sumstyled” Contingency Argument.^{1}
(1): Everything not existing by necessity (i.e. everything that could fail to exist) owes its existence to something external to itself. (For example, planets, lightning, and humanity each owes existence to something else.)(2): Something exists (call it “Universe” or “Big Contingent Sum”) which is the sum of all these things which do not exist by necessity.^{2}
(3): Therefore, “Big Contingent Sum” owes its existence to something external to itself.
(4): Whatever exists externally to “Big Contingent Sum” obviously cannot itself be contingent (i.e. cannot be part of that sum).
(5): Therefore, whatever exists externally to "Big Contingent Sum" is not contingent; by definition it exists of necessity.
Conclusion: Therefore, “Big Contingent Sum” owes its existence to something that exists by necessity.
 Note: “Sumstyled” is a neologism I'm employing to denote cosmological arguments which focus on explaining a “sum” of a given kind.
 One might object to the assumption that there is an aggregate or sum of those things that is distinct from the parts, making up some kind of composite object. This worry is partially what invites the following even more modest version, which doesn't even assume there is a set of such things. Here is another more technically rigorous example, whereby “concrete thing” we mean something that possibly causes something.
• Alexander Pruss & Joshua Rasmussen: “
(1) For any particular contingent concrete things, there is an explanation of the fact that those things exist.
(2) Considering all the contingent concrete things that exist, if there is an explanation of the fact that those things exist, then there is a necessary concrete thing.
(3) Therefore, there is a necessary concrete thing.” In the next footnote is a symbolic formulation.  (1) ∀xs[[∀y(y ∈ xs) → C(x)] → EE(xs)].
(2) (∃xs(EE(xs) ∧ ∀y(C(x) → y ∈ xs))) → ∃yN(y).
(3) ∴ ∃xN(x). [Necessary Existence) (Oxford, 2018), 38.]
They interpret the predicates as follows:
• ‘EE(xs)’ reads ‘there is an explanation of the fact that the xs exist’.
• ‘C(x)’ reads ‘x contingently exists and is concrete (causallycapable)’.
• ‘N(x)’ reads ‘x is a necessary being’—i.e., ‘x necessarily exists and is concrete (causally capable)’ • ‘y ∈ xs’ reads ‘y is one of the xs’.

A “Startstyled” Contingency Argument
A “Startstyled” Contingency Argument.^{1, 2, 3}
(1): It is metaphysically possible for a first contingent thing's existing to be caused.
(2): In this possible (even if nonactual) scenario, a noncontingent causer must exist to cause that first contingent thing.
(3): So this noncontingent (necessary) causer exists in this possible scenario.
(4): If a necessary entity exists in any truly possible scenario, then it exists in all possible scenarios. (Existing in all possible scenarios is just what it means to be necessary.)
(5): Therefore, the necessary causer in that actual or nonactual scenario exists.
 Note: “Startstyled” is a neologism I'm employing here to denote cosmological arguments which focus on explaning some “first” thing. This version is my own formulation, but arguments along these lines perhaps originate with John Turri, who was himself influenced by Rasmussen's work. Turri's argument ran as follows:
1. It is possible that the first contingent thing is caused to exist.
2. In the possible case where the first contingent thing is caused to exist, a causally powerful necessary being must cause it to exist.
3. So a causally powerful necessary being possibly exists.
4. So a causally powerful necessary being necessarily exists. [“A New And Improved Argument For A Necessary Being” Australasian Journal of Philosophy 89 (2)(2011): 357359.]
One challenge with Turri's formulation is that being “causally powerful” need not be an essential property of the necessary being—it might be a necessary being, and only in some worlds be causally powerful.  Another “Startstyled” Contingency Argument comes from Rutgers philosopher Christopher Weaver (see here). He couches his argument in terms of events specifically (rather than “thing”). It is more complex, but perhaps also more rigorous, since the proper relata in causation will always or typically be events. Moreoever, he foucses on “purely” contingent facts, which are facts that have no necessary component. The motivation here is to prevent “the cause of the cause” type objections. For example, in my simplified argument, what is the first contingent thing? Is it an event, or an object.
 Regarding definitions: By “thing” here I mean what philosophers call a “concrete object” (as opposed to an abstract object, like a number). And by “scenario” I mean by philosophers call “a possible world.”
 Note: “Startstyled” is a neologism I'm employing here to denote cosmological arguments which focus on explaning some “first” thing. This version is my own formulation, but arguments along these lines perhaps originate with John Turri, who was himself influenced by Rasmussen's work. Turri's argument ran as follows:

Pruss's Leibnizan Cosmological Argument
Alexander Pruss's Contingency Argument (2009)^{1} is presented as a series of steps:
(1): Every contingent fact has an explanation.^{2}
(2): Some contingent fact includes all other contingent facts.
(3): Therefore, there is an explanation of this fact.
(4): This explanation must involve a necessary being.
 Note: Details definitions and Q&A are forthcoming. You can see Pruss's argument discussed in “Leibnizian Cosmological Arguments” The Blackwell Companion to Natural Theology (2009), 24100.
 In philosophy/logic, a fact is contingent just in case it is a proposition which could have been false. (For example, presumably 'planets exist' is only a contingently true fact. By contrast, 'purple does not weigh three pounds' seems to be necessarily true; it could not have been otherwise.)"

A Big Bang Argument from Beginnings
(1): Any genuinely possible event is possibly caused.
(2): A Big Bang event in which there is an ultimate beginning of contingent things is a genuinely possible event.
(3): Therefore, such a Big Bang event is possibly caused.
(4): Only a necessary being could cause an ultimate beginning of contingent things.
(5): Therefore, a necessary being is possible.
(6): If a necessary being is possible, then a necessary being exists.^{1}
(7): Therefore, a necessary being exists.^{2} A necessary being is one which by its definition cannot possibly exist unless it exists in all possible worlds, including the actual one. See proof above.
 This argument captures the flow of Rasmussen's Argument from Beginnings (below), but perhaps in a way that is easier to grasp. The paraphrase comes from Rasmussen himself (in personal correspondance).

Rasmussen's Modal Argument from Beginnings (Advanced)
Joshua Rasmussuen's Modal Argument from Beginnings (2011)^{1, 2} Paraphrase:
(1): Normally, for any intrinsic property p that (i) can begin to be exemplified and (ii) can be exemplified by something that has a cause, there can be a cause of p ’s beginning to be exemplified.(2): The property c of being a contingent concrete particular is an intrinsic property.
(3): Property c can begin to be exemplified.
(4): Property c can be exemplified by something that has a cause.
(5): Therefore, there can be a cause of c’s beginning to be exemplified.
(6): Therefore, if (5), then there is a necessary being.
(7): Therefore, there is a necessary being.
 This argument comes from Joshua Rasmussen, “A New Argument for a Necessary Being.” Australasian Journal of Philosophy (2011): 351356. Elaboration on and discussion of Rasmussen's paper, forthcoming.
 Rasmussen put forward what seems to be another sound argument for a necessary being shortly before. (“From States of Affairs to a Necessary Being.” Philosophical Studies (2010):183200. It runs like this:
(1): For any type T, if T “is a [intrinsic] type of” concrete contingent entity, then it is possible that there is at least one entity y, such that y causally produces O. (O = df. The concrete state of affairs of there being at least one member of the type “concrete contingent entity.”)
(2): For any type T, if T “is a type of” concrete contingent entity, then it is impossible that there is at least one entity y, such that y is a member of T and y causally produces O.
(3): Therefore, if it is possible that there is at least one entity y such that y causally produces O, then “it's possible for there to be a concrete” entity “that isn't contingent.”
(4): Therefore, it is possible that there is necessary concrete entity.
(5): Therefore, there is a necessary concrete entity.

Weaver's Argument from Beginnings (Advanced)
Christopher G. Weaver's Argument from Beginnings (2013)^{1, 2}
(1): Possibly, there is at least one entity x, such that x is a first purely contingent event.
(2): Necessarily, for any entity x, if x is a first purely contingent event, then possibly, there is at least one entity y, such that x is the first purely contingent event, and y causally produces x.
(3): Necessarily, for any entity x, and for any entity y, if both x is the first purely contingent event and y causally produces x, then y is an event that is not purely contingent.
(4): If, possibly there is at least one entity y, such that y is an event that is not purely contingent, then possibly there is at least one entity z, such that z is an individual and z exists necessarily.
(5): Therefore, possibly there exists a z, such that z is an individual and z exists necessarily.
 Originally posted on Scientia et Veritas.
 Formalized. Interpretation: {E!x: x exists; Fx: x is a first purely contingent event; Ix: x is an individual; Px: x is purely contingent; Vx: x is an event; Rxy: x causally produces y; Domain: unrestricted}
(1): ♦Ǝx(Fx) [Premise]
(2): ■∀x(Fx ⊃ ♦Ǝy(Fx & Ryx)) [Premise]
(3): ■∀x∀y((Fx & Ryx) ⊃ (Vy & ~Py)) [Premise]
(4): ♦Ǝy(Vy & ~Py) ⊃ ♦Ǝz(Iz & ■E!z) [Premise]
(5): Therefore, ♦Ǝz(Iz & ■E!z) [Conclusion]