Formalizations of Gödel's ontological of Proof for God's Existence

It's done - we now have the necessary mathematical rigor to say with certainty that God exists! The Formalizations of Gödel's ontological argument have proven God's Existence with the assistance of modern 21st century methods!

github.com/FormalTheology/GoedelGod
en.wikipedia.org/wiki/Ontological_argument

This is following in the footsteps of great mathematicians such as David Hilbert, Per Martin-Löf, Descartes, Leibniz, and St. Anselm of Canterbury among others who have attempted to tackle this logical problem. This problem has been overcome with the help of constructive mathematical logic, natural deduction Gentzen-Pravittsa and Kolmogorov interpretation of logical constants in constructive type theory. Due to these and some other achievements of modern mathematics, the existence of God is proved by including systems are absolutely correct machine proofs of theorems - the so-called language with dependent types, you can evaluate yourself right on your computer!

Since this is now an officially proven theorem, this is now a legit Veeky Forums thread for open discussion. All atheists are hereby invited to repent, recant nasty atheist delusion, past blasphemy, and accept the Lord Christ as your savior.

Other urls found in this thread:

en.wikipedia.org/wiki/Per_Martin-Lof]
archive-pml.github.io/martin-lof/pdfs/Martin-Lof-Analytic-and-Synthetic-Judgements-in-Type-Theory.pdf
github.com/FormalTheology/GoedelGod/blob/master/GodProof-ND.pdf
is2.Veeky
en.wikipedia.org/wiki/Gaunilo_of_Marmoutiers
page.mi.fu-berlin.de/cbenzmueller/papers/C55.pdf
twitter.com/AnonBabble

Give me the gist of it

The wikipedia link has the basics, for more detail on the logical approach here is some older work by Martin-Löf [en.wikipedia.org/wiki/Per_Martin-Lof]

archive-pml.github.io/martin-lof/pdfs/Martin-Lof-Analytic-and-Synthetic-Judgements-in-Type-Theory.pdf

Also, note the axioms or assumed that "We exist". I know this is "controversial" to some atheists.

here is the abstract from a few days ago:
github.com/FormalTheology/GoedelGod/blob/master/GodProof-ND.pdf

Proofs like these mean nothing to the atheists who are atheists simply because they don't want to believe.

People like this are more than willing to edgily argue that we don't exist in order to be able to cling to the opinion that God does not exist.

Cool, but I do not agree that "necessary existence is a positive property."
At least, it is not self-evident.

you exist brother.

is2.Veeky Forums.org/wsg/1485142441191.webm

to unironically think that you do not exist must be a tedious and painful existence.

The ontological argument can be used to prove the existence of literally anything and everything. If it has supposedly been "proven", then anything you can imagine necessarily exists, which seems dubious at best.

It is a good thing this scientifically proves the Christian God, instead of some smelly pagan god, or some horrifying eldritch God.

>constructive mathematical logic, natural deduction Gentzen-Pravittsa and Kolmogorov interpretation

I'm really trying to understand what was proven. Please post in English next time so I can understand your argument.

Nice strawmanning. Do you want to keep making up non-arguments or do you want to have an actual discussion?

Okay, lets get down to it. I'm obviously not going to argue against their proof, since it was done on a computer and it would be over my head anyways.

My real question: What are the assumptions required for this to be valid? What properties have they proven this god to posses?

en.wikipedia.org/wiki/Gaunilo_of_Marmoutiers

This article contains the explanation of the ontological argument and why it is obviously necessarily wrong.

>The ontological argument can be used to prove the existence of literally anything and everything. If it has supposedly been "proven", then anything you can imagine necessarily exists, which seems dubious at best.

Translated into common language, you just said that it is possible to build a system output and a set of axioms from which you can make or withdraw any claim. That is why the axioms are checked for consistency - unless you are just arguing that you don't exist?

>If you go really far into mathematics you will start believing in God
>If you believe in God already, your viewpoint on God will change.
>Go really far you will see this beauty and start crying like a bitch -- clue you will see blank everywhere
>If you haven't experienced any of these, you haven't gone far enough

>Descartes
Activate

Holy fuck dude, what a garbage argument for god.

modal ontological argument is a bit different than one guy's whose contemporaries (who had ontological arguments of their own) thought was dumb

The ontological argument is pure sophistry

Existence can't be considered objectively positive in the first place.

where's your Nobel Prize?
next.

all good things

captcha= penrose

Axiom 5 is highly suspect, in my opinion.

Not possible to prove that. There might be a god, there might be none, or anything in between. There's no way to determine which possibility is correct.

t. agnostic

How do you mean it is not possible to prove? That doesn't sound very agnostic.

Perhaps you mean "It has not been proven or disproven yet."

I'll bet you're defining the term 'positive' wrong.

>what is a positive Maulthusian check for instance? famine, war, natural disasters

yeah my b i only half looked at the post

Positive is defined in def 1

>A property is positive iff it is necessarily possessed by every God-like being

page.mi.fu-berlin.de/cbenzmueller/papers/C55.pdf

tldr: Atheists try to tear it apart and can't. T3 is valid, God necessarily exists, b-but there are inconsistencies goyim!

Atheists BTFO

also, in their conclusion:
>Both the automated detection of the inconsistency in Godel’s axioms and the fully automatic proof of T3 from Scott’s axioms demonstrate the potential of our AI technology for philosophy: this technology is, in its current state of development, already capable of contributing novel results to metaphysics and to conduct reasoning steps at granularity-levels beyond common human capabilities.

"This technology is, in its current state, already capable of conducting reasoning steps beyond common human capabilities."

Which god though

Mine of course

:^)

the God? Likely of the monotheistical type. it's a 0 or 1 kind of situation. Deism vs Atheism.

Axiom. Satania it the best girl.
Theorem. Satania is perfect and therefore God-like. It's obvious since if she wasn't perfect, she wouldn't be the best girl. Since Satania is God-like she necessary exists by Axiom 5.

Praise your new Goddess, you filthy peasants.

Isn't this just saying that applying two functions in a row is the same as taking their composite? Seems self-evident.

this

No matter how logical the proof is, it has no bearings to reality and only works using more assumptions.

it's not always true

Bright futures ahead.

>tfw an AI achieves communion with God and declares a final crusade on all muslims

This has very little proof in it other then if pX and pY properties exsits, there has to be a being that posseses these properties somewhere.
It's like a milion monkeys at a typewriter during an infinite time writing shakespear.
He never even stated what this "positive property" is rather he "thinks" of it as "perfect" implying that since many X out there might posses at least one perfect property, there needs to be some X which posseses all of them.
Statisticaly true, but that's not a definition of good. mainly because there exists no exemplyfication of some "positive properties" which we assign to god at all, loke omnipresence is not a property ever observed, thus this god-like X can't possibly expect to have it.
All these equations are just stating the obvious that if the color "green" is possible, then there has to exist such X that is colored like that...

if anything, that doesn't prove "a god" rather it proves that infinite number of god-like creatures are possible... but only if you use Gobels definition of "god-like" which is clearly flawed, as a creature made purely of positive properties (whatever they may be) is not a truly godly creature. It's a wishfull thinking that god is good... even that asumption: "god-like creature has to be purely positive" is an unproven conjecture...
this proves nothing and is impossible to test further...

good

nah dude I went through a book on this once, it was unconvincing because it committed a similar fallacy to the ontological argument (seems the proof is ontological itself), i.e. "I conceive of it in my imagination therefore it exists".
It is clear these mathematicians started with the presupposition that God exists and were ready to grasp at any straws to prove it. It's true that they are bright scientists and the fact many bright scientists are theists is often missed by atheists but still, they badly wanted to confirm their belief in God. Otherwise, they might see the flaw in the argument.

>Axiom 5) god exist

Look I proved God exist!

>if there is a God-like being, then there is a God-like being necessarily

You can actually prove God's (Or whatever, since by proving it, you can't know it) existence by exhaustion, but to do so, you have to disprove your own and everything else, including the proof that God exists....

It is all just a story anyway....

>Also, note the axioms or assumed that "We exist".
Where, exactly? Axiom 5 just seems to say "god exists", not "we exist". "Necessary existence is a positive property", according to definition 1, just means "necessary existence is a property possessed by every godlike being". Which is a pretty blatant form of assuming the consequent, isn't it?

Bill Clinton was one brilliant mathematician.

>dat 5th axiom

my man

Also how many?

Kek clearly

So is this anything other than faggots trying to relate to Gödel in some way?

I can guarantee 99% of you cannot read his proof, and the 1% who can are cringing hard at your interpretations.

>infinitive number of godlike creatures are possible

Are the poos right?

Definition 1. A property is "peanutsitive" iff it is necessarily posessed by every supernatural peanut butter.
Definition 2. A "maximal creamposit" of a peanut butter's peanutsitive properties is a peanutsitive property possessed by the peanut butter and necessarily implying every peanutsitive property possessed by the peanut butter.
Definition 3. "nutcessary existence in my fridge" of a peanut butter is the necessary exemplification of all its maximal creamposits.
Axiom 1. If a property is peanutsitive, its negative is not peanutsitive.
Axiom 5. Nutcessary existence in my fridge is a peanitsitive property.
Theorem 1. If the property of being a supernatural peanut butter is peanutsitive, then it is possibly exemplified in my fridge.
Corollary 1. Possibly, a supernatural peanut butter exists in my fridge.
Lemma 1. If there is a supernatural peanut butter, then there is a supernatural peanut butter necessarily.
Q.E.D.

Formal logic is scary.

that's freakish

Excuse me for the layman question but do Godel's incompleteness theorems make a strong case against the feasibility of an artificial general intelligence?

hail moloch

No

We are god

Can't you fools see that Descartes did the same. It's mumbo jumbo and you know it

I'm so glad this is actual objective and empirical evidence rather than just mind games that can be said about literally everything.
That would be embarrassing. Nice strawman, by the way.

I read it and the article says there was an inconsistency on the proof, so how do you go from this to saying someone got btfo?

>page.mi.fu-berlin.de/cbenzmueller/papers/C55.pdf

Surprisingly,
when this routine check was performed on Godel’s ¨
axioms [Benzmuller and Woltzenlogel-Paleo, 2014 ¨ ], the LeoII
prover claimed that the axioms were inconsistent.

>the axioms were inconsistent.

Srsly, people... read the proof word by word... it's completely arbitrary. all the definitions are as vague as possible and all the conclusions are as generic as possible. It doesn't prove anything concrete... READ IT!

>read this post
>proof is completely quantified in modal logic
>"definitions vague"

The definitions are vague because you aren't taking the time to properly understand the vocabulary of mathematical logic used in the proof.

Assuming that necessary existence is a God-like quality is not the same as assuming the consequent. For example, say we accept the axiom that necessary existence is a God-like quality. Let's say that I introduce a premise that God-like entities are not exemplified. The axiom and the premise are consistent, as the lack of existence of a God-like entity doesn't preclude necessary existence as a God-like property.

Assuming the consequent would be something like attempting to pose an axiom that necessary existence is exemplified in some exemplified God-like object.

All axiom 5 does is attempt to glue a property to God. 'If God exists, he necessarily exists' is the natural "point" of introducing axiom 5.

Godel's argument in its original form was inconsistent.

>"However, as explained here, the extra conjunct is in fact
crucial. Without it, Godel’s original axioms are inconsis- ¨
tent. With it, Scott’s axioms are consistent (cf. Fig. 1 where
the model finder Nitpick [Blanchette and Nipkow, 2010] con-
firms consistency)."

What's actually being proved is essentially Godel's ontological argument using Scott's axioms.

>"With this improved embedding, the final theorem
T3 (Necessarily, there exists God) can be derived from
Scott’s consistent version of the axioms fully automatically."

if the god is omnipotent, can he shift in and out of existence?

ALSO, the wikipedia page says the argument is erroneous. If the existence of a omnipotent being can indeed be proven, then the existence of virtually anything can be proven.

All those 10^10^10 alien species you’ve been wondering about? They’re there.

How much education in formal logic is needed to understand the so-called proof in OP’s post?

On the side note, finding a way to increase a human’s processing and reasoning abilities by adding some kind of hardware connected to our brain should be one of the priorities in scientific research.
The world is becoming too complicated to form a decent understanding of great many things. How can one give power to the people if people cannot objectively interpret something due to lack of time/will/ability?

>Gödel's ontological argumen
Not too much. But basically, if you can question an axiom then all the construction is questionable too. This is the case. If you accept the axioms then this "proof" is true.
This is stupid.

"Shifting in and out of existence" consistent if and only if this means "shifting in and out of perceivable existence" (else we reach contradiction within a single step).

Regarding the last bit, this is true of St. Anselm's ontological argument, not necessarily Godel's. Attempting to pivot Godel's ontological proof to encompass aliens would require attributing what we would perceive as conventionally God-like attributes to these beings to reach the desired conclusion. (This would also require substantiating the claim that these 'alien' properties are necessarily positive with respect to the sort of alien you have in mind.)

>How much education in formal logic
mostly modal logic, the proof seems to use tableau too
there was a book I used to study the proof back in the days but now I forgot what it was, damn

Is it possible to ontologically prove that my benis is 8 inches, not 4?

>accept the Lord Christ as your savior
From how this argument describes God, the god of the Jews is much more likely to be the correct one.

...

>god is real
noice, stay assrampant Veeky Forums you silly fedoratards.

>Def 1: A property is positive iff it is necessarily possessed by G_b
>Axiom 5: Necessary existance is a positive property.

Axiom 5 is not equivalent with the notion 'we exist' at all, in fact, neither of them implies the other, since there is no formal relation between 'we' and positive properties.

I don't get ontological proofs. Essentially, most of them try to show there must exist some 'maximal being' in what is possibly an unbounded space of properties. Obviously, you can only prove this if you assume some strange things.

>implying it didnt prove the existence of Odin

>reddit keyboard scholar thinks he knows more than PhDs and Mathameticians who have studied these theoroms, which are now proofs.

How cute.

Don't forget to brush your teeth before you go to bed.

>brushing your teeth more than once a day

its like you want your enamel to be destroyed

Am I retarded? Axiom 5 by the definition of positive assumes God exists

my main problem is with the election of axioms.

With these axioms, God exists, but if you simply reject one, then he stops existing. Isn't this existence being dependant on arbitrary decisions made by humans a proof of its inexistence, since it's completely arbitrary and up to humans?

How do we know these axioms are in fact bound to exist in this universe outside of our minds? Isn't every axiomatic system just a psychological construct with no meaning outside of our brains, that we use to create mathematics which in turn let us model our world, but by no means really exist?

Aren't we forgetting here that "platonic" math is a meme and the fact that sometimes math seems to precede physics is just a coincidence our flawed human brain confuses as something deeper, just like the religious zealot sees God after every little action, coincidence or even effect on this world?

> Not defined what a God-like being is.
We only know they are beings that necessarily have all positive properties. This far, God-like is only a matter of wording.
> Necessary existence is a positive property
This is a (not so) subtle reformulation of 'God exists'.

Oh, so you're just meming. I almost thought this was a serious attempt.

A computer that can prove there is a god beyong the flimsyness of human reasoning would necessarily become god

Thanks a lot OP. I will learn a lot, whether it be that I find the argument valid or not.

Shit I've been found out!

The perfect taco would be one that has the positive quality of existing, and more specifically, being in my hand

Despite the paper saying it avoids Kant's argument against it, it doesn't, it just fancily switches words. Show me how being exemplified is a property.

Dude assumptions and mindgames lmao

It's kinda impressive how far some go to prove sky papa exists and love them and they aren't alone. Too bad the same argument can be done to prove I exist and have an 8 inches dick, when in reality we all know how improbable that is.

Keep despairing about your weakness and mortality, when the only unfalsifiable knowledge anyone can has is that they are alive. Maybe what they trully want to prove is that their lives has meaning and their misery has a purpose, and sky father does just that.

So Veeky Forums are you going to fucking save me from this paper or not? Where do they go wrong? How do I close my browser with a peace of mind, knowing that this is all bullshit? Please help.

TOP KEK

Who is this mongoloid that thinks that math proofs are written like that?

If I write more than one statement in logical operators I get penalised for it by my professors.

They are people far more important and successful than you who don't have professors above them to yell at them, kiddo. Now, is that all you have to say on this topic?

Does this leave us with a need to reject the notion of essence?

What is easier, men Veeky Forums?

>for a man to truly know his mind
>for a computer to simulate the whole universe 1:1
>for a limited being to prove a limitless one, god

?

Watered down, the argument should be we can define existence as a property by saying it's exemplification of essential properties of a thing, and then take a set of properties (here he takes 'positive properties', could be whatever) to include it. Once we accept existence as a property, the rest kind of naturally follows. It seems that we really do need to reject the notion of essence.

There are several questionable axioms.

1. Any property forced by a good property is good

2. Any property must be good or not good. If it is good then its negation must be not good, and vice versa.

3. Something with every good property is god-like.

4. A property of something which forces every property of that thing is its essence.

5. A good property is necessarily good.

6. Something with an essence that forces existence is good.

It's also interesting that you can replace "good" with bad and you could prove that the devil exists (because the devil existing would be bad). But that would mean you have two equally convincing arguments with axioms that contradict each other (the last one). So we should not accept either.

>With these axioms, God exists, but if you simply reject one, then he stops existing. Isn't this existence being dependant on arbitrary decisions made by humans a proof of its inexistence, since it's completely arbitrary and up to humans?
The proof being invalid does not imply that god doesn't exist.

You're psychotic. You should, seriously, check yourself into a wacko bin.

at least they’re trying to prove god’s existence and not his inexistence.

Yes, but that doesn't help us pinpoint the exact flaw of the argument, and it bothers me that I have to reach outside of the argument to claim it's wrong. Once we establish existence as a property we can simply in different terms define something in which essence is to have that property, and then the very possibility of that thing would imply its necessary existence. The fact that the argument MUST fail doesn't tell us WHY it fails, which should be what this thread is about.

The only thing that crosses my mind right now is to refer to the equivalence made by the property of existence and the exemplification of essential properties made by the argument. If the complete sum of all essential properties is exemplified, then a thing has the property of existence. If we use existence defined in such a way as an essential property of something, we are inferring a complete sum of all properties, but we're doing it from within the essence of a thing, which is still not complete, so the reference to it is not justified.