Presentation of My Interpretation of Gödel's Ontological Argument! (By modern language of logics, uncontroversially.)

UoD: Everything.
Gx: x is God-like
Ex: x has essential properties.
Ax: x is an essence of A.
Bx: x is a property of B.
Px: property x is positive.
Nx: x is a General property.
Xx: x is Positive existence.
Cx: x is consistent.

The final argument by my interpretation is presented below in 4 parts:

1.

1 │ □Ex ≡ □Px ≡ □Gx A (A is Assumption)
2 │ □Ex A
3 │ ◊Px ≡ □Px A
4 │ ◊Px A
------------------
5 │ □Px ≡ □Gx 1, 2 ≡E
6 │ □Px 3, 4 ≡E
------------------
7 │ □Gx 5, 6 ≡E

Alt. 1, 1st.

1 │ □Ex ≡ □Px ≡ □Gx A (A is Assumption)
2 │ □Ex A
3 │ ◊Px ⊃ □Px A
4 │ ◊Px A
------------------
5 │ □Px ≡ □Gx 1, 2 ≡E
6 │ □Px 3, 4 ⊃E
------------------
7 │ □Gx 5, 6 ≡E

Alt. 1, 2nd.

1 │ □Ex ≡ □Px ≡ □Gx A (A is Assumption)
2 │ (□Px ⊃ □Nx) ⊃ □Px A
3 │ □Px ⊃ □Nx A
4 │ □Ex A
------------------
5 │ □Px 2, 3 ⊃E
6 │ □Px ≡ □Gx 1, 2 ≡E
------------------
7 │ □Gx 6, 5 ≡E

This alternative, nr. 2, takes care of the former line ”6 │ (□Px ⊃ □Nx) ⊃ □Px A” and adds overall description by this!

2.

1 │ □Px ≡ □Gx A (A is Assumption)
2 │ □Xx ⊃ □Px A
3 │ □Xx A
------------------
4 │ □Px 2, 3 ⊃E
------------------
5 │ □Gx 1, 4 ≡E

3.

1 │ ◊Cx ≡ □Gx A (A is Assumption)
2 │ □Px ∨ ~□Px A
3 │ □Px ⊃ ◊Cx A
------------------
4 ││ □Px A
0 ││-----------------
5 ││ □Px 6 R

6 ││ ~□Px A
0 ││-----------------
7 ││ □Px 6 R
8 │ □Px 4, 6-9 ∨E
9 │ ◊Cx 8, 3 ⊃E
------------------
10│ □Gx 9, 1 ≡E

4.

1 │ □Bx ≡ □Gx A (A is Assumption)
2 │ ◊Ax ≡ □Bx ≡ (◊Ax ⊃ □Bx) A
3 │ ◊Ax A
------------------
4 │ □Bx 3, 2 ≡E
------------------
5 │ □Gx 4, 1 ≡E

Note for the 4th part: Consider (◊Ax ⊃ □Bx) as “added explanation”!
Also, line 2 of the 4th part is Definition 2 from the original argument of Gödel.
Note2: The following lines are taken out for having no use in this interpretation of the argument.
8 │ □Gx ⊃ □Px A
16│ □Gx ⊃ □Cx A
17│ □Gx ⊃ □Ax A
No need to put any emphasis to the line numbers 8, 16 and 17 above.
Note3: A forgotten line 6 and its own alternative has been added now, 16:28, 13.03.2012 CET.
Note4: Small corrections. Adding the direct relations to Gödel's Ontological Argument. Added now, 23:40, 13.03.2012 CET.
Note5: The above time stamps relate to publishing on Facebook as note! The whole presentation has therefore been imported from the original place on Facebook to this blog. By Leonardo F. Olsnes-Lea on Facebook on Saturday, 14 January 2012 at 02:43 CET(?).

Else, development has been:
(relating to Gödel's argument directly, put after the connector),

1 │ □Ex ≡ □Px ≡ □Gx A (A is Assumption) – Def. 1
2 │ ◊ Ax ≡ □ Bx ≡ (◊Ax ⊃ □Bx) A - Def. 2
3 │ □Ex A – Def. 3
4 │ □Px A
5 │ □Px ∨ ~□Px A – Axiom 1
6 │ (□Px ⊃ □Nx) ⊃ □Px A – Axiom 2
7 │ ◊ Ax A
8 │ □Gx ⊃ □Px A – Axiom 3
9 │ ◊Px ≡ □Px A – Axiom 4
10│ ◊Px A
11│ □Xx ⊃ □Px A – Axiom 5
12│ □Xx A
13│ ◊ Px ⊃ □Px A – Axiom 6
14│ □Px ⊃ ◊Cx A – Theorem 1
15│ ◊Px ≡ □Px A
16│ □Gx ⊃ □Cx A – Corollary 1
17│ □Gx ⊃ □Ax A – Theorem 2
------------------------------
18│ □Ex R (R is Reiteration)
19│ □Px ≡ □Gx 1, 13 ≡E (≡E is Biconditional Elimination)
20│ □Px 4 R
------------------------------
21│ □Gx 14, 15 ≡E – Theorem 3

Various notes to the development have also been written under the argument as note on Facebook!