Proof of an imbecile doctrine

[godelian]

We will analyze the following imbecile doctrine:

Axiomatization:

1) Mr.X Is God.
2) Mr.X is the son of God

Prove the following theorem:

Mr.X is the son of himself.

We now encode the imbecile doctrine in the TPTP format. The acronym "TPTP" stands for "Thousands of Problems for Theorem Provers". It is the standard format for Automated Theorem Provers:

% ---------------------------------
% Imbecile doctrine in TPTP format
% ---------------------------------

% Mr.X Is God

fof(axiom1, axiom,god(MrX)).

% Mr.X is the son of God

fof(axiom2, axiom, son_of(MrX, God)).

% Imbecile conclusion. Prove that Mr.X is the son of himself.

fof(conjecture1, conjecture, son_of(MrX, MrX)).

We now use the Vampire automated theorem prover to produce the proof for the imbecile conclusion:

$ ./vampire imbecile-doctrine.txt
% Running in auto input_syntax mode. Trying TPTP
% Refutation found. Thanks to Tanya!
% SZS status Theorem for imbecile-doctrine
% SZS output start Proof for imbecile-doctrine
2. son_of(X0,X1) [input]
3. son_of(X0,X0) [input]
4. ~! [X0] : son_of(X0,X0) [negated conjecture 3]
6. ! [X1,X0] : son_of(X0,X1) [closure 2]
8. ? [X0] : ~son_of(X0,X0) [ennf transformation 4]
9. ! [X0,X1] : son_of(X1,X0) [rectify 6]
10. ? [X0] : ~son_of(X0,X0) => ~son_of(sK0,sK0) [choice axiom]
11. ~son_of(sK0,sK0) [skolemisation 8,10]
12. son_of(X1,X0) [cnf transformation 9]
13. ~son_of(sK0,sK0) [cnf transformation 11]
14. $false [subsumption resolution 13,12]
% SZS output end Proof for imbecile-doctrine

So, we have indeed successfully proven that Mr. X is the son of himself. Why is it possible to prove this imbecile conclusion? Well, obviously, because the axioms of this doctrine are imbecile. It is an excellent example of the Garbage In, Garbage Out principle:

https://en.wikipedia.org/wiki/Garbage_in,_garbage_out

In computer science, garbage in, garbage out (GIGO) is the concept that flawed, biased or poor quality ("garbage") information or input produces a result or output of similar ("garbage") quality. The adage points to the need to improve data quality in, for example, programming. Rubbish in, rubbish out (RIRO) is an alternate wording.[1][2][3]

Since the doctrine is pure garbage, it is obvious that its theorems will also be complete garbage. In other words, an imbecile doctrine is unusable for any practical purpose.

[Skepdick]

blah blah blah

You still haven't figured out that loops are integral to dynamic processes/any system with iterative feedback.

It is 100% correct that you are your own ancestor. You think it's garbage because you've left out the temporal dimension. Yesterday-Me is an ancestor to Today-Me.

The reason you can't get out of Plato's cave is because you are still stuck running on Classical Logic in your brain. No matter how vehemently you assert to reject it/accept constructive methods. You haven't internalized it enough to begin using/applying it in practice.

Saying you accept bicycle riding isn't the same as learning to ride it.

[Age]

'The son' 'grows up' to be 'the father'.

'The two' become 'the one'.

There is also 'a son' grows to be 'a father', and/or to be 'like' 'its father'.

There is NO 'thing' that just REMAINS 'the same', forever, (except of course for the two things, 'matter' and 'space', which these 'two things' make up the One thing, the Universe, Itself, which IS also FOREVER). So, besides these things EVERY thing else is NEVER just 'one thing' as 'they' ALL be-come, or come-to-be something else. Just like children be-come adults and/or parents, and like how sons be-come or come-to-be fathers, which is just like how daughters be-come mothers.

Until you define what so-called 'mr x' IS, EXACTLY, then 'mr x' COULD be 'the son' OF what 'it' BECOMES.

[godelian]

blah blah blah

You still haven't figured out that loops are integral to dynamic processes/any system with iterative feedback.

It is 100% correct that you are your own ancestor. You think it's garbage because you've left out the temporal dimension. Yesterday-Me is an ancestor to Today-Me.

The reason you can't get out of Plato's cave is because you are still stuck running on Classical Logic in your brain. No matter how vehemently you assert to reject it/accept constructive methods. You haven't internalized it enough to begin using/applying it in practice.

Saying you accept bicycle riding isn't the same as learning to ride it.

You can also use the same imbecile axioms to prove that God is the son of himself:

$ cat imbecile-doctrine.txt
% ---------------------------------
% Imbecile doctrine in TPTP format
% ---------------------------------

% Mr.X Is God

fof(axiom1, axiom,god(MrX)).

% Mr.X is the son of God

fof(axiom2, axiom, son_of(MrX, God)).

% Prove that God is the son of himself

fof(conjecture1, conjecture, son_of(God, God)).

As you can see below, this logical consequence is perfectly provable from the imbecile doctrine:

$ ./vampire imbecile-doctrine.txt
% Running in auto input_syntax mode. Trying TPTP
% Refutation found. Thanks to Tanya!
% SZS status Theorem for imbecile-doctrine
% SZS output start Proof for imbecile-doctrine
2. son_of(X0,X1) [input]
3. son_of(X1,X1) [input]
4. ~! [X1] : son_of(X1,X1) [negated conjecture 3]
6. ! [X1,X0] : son_of(X0,X1) [closure 2]
7. ~! [X0] : son_of(X0,X0) [rectify 4]
9. ? [X0] : ~son_of(X0,X0) [ennf transformation 7]
10. ! [X0,X1] : son_of(X1,X0) [rectify 6]
11. ? [X0] : ~son_of(X0,X0) => ~son_of(sK0,sK0) [choice axiom]
12. ~son_of(sK0,sK0) [skolemisation 9,11]
13. son_of(X1,X0) [cnf transformation 10]
14. ~son_of(sK0,sK0) [cnf transformation 12]
15. $false [subsumption resolution 14,13]
% SZS output end Proof for imbecile-doctrine
% ------------------------------
% Version: Vampire 4.9 (commit 5ad494e78 on 2024-06-14 14:05:27 +0100)
% Linked with Z3 4.12.3.0 79bbbf76d0c123481c8ca05cd3a98939270074d3 z3-4.8.4-7980-g79bbbf76d

Imbecile axiomatizations are actually interesting in their own right. What else can we prove from them?
An imbecile doctrine is very useful for the purpose of proving imbecile conclusions!

[godelian]

'The son' 'grows up' to be 'the father'.
'The two' become 'the one'.

Yes, you can indeed prove that Mr. X is also his own grandfather as well as his own grandchild. So, that allows us to prove the theorem of the imbecile grandchild:

$ cat imbecile-grandchild.p
% ---------------------------------
% Imbecile doctrine in TPTP format
% ---------------------------------

% Mr.X Is God

fof(axiom1, axiom,god(MrX)).

% Mr.X is the son of God

fof(axiom2, axiom, son_of(MrX, God)).

% define grandson as the son of the son

fof(grandchild_def, axiom,
! [A, B] : (grandson(A, B) <=> ? [Z] : (son_of(A, Z) & son_of(Z, B)))).

% Theorem: Prove that MrX is his own grandchild
fof(prove_grandchild, conjecture,
grandson(MrX, MrX)).

As you can see below, the theorem of the imbecile grandchild is a perfectly logical consequence of the imbecile doctrine:

$ ./vampire imbecile-grandchild.p
% Running in auto input_syntax mode. Trying TPTP
% Refutation found. Thanks to Tanya!
% SZS status Theorem for imbecile-grandchild
% SZS output start Proof for imbecile-grandchild
2. son_of(X0,X1) [input]
3. ! [X2,X3] : (grandson(X2,X3) <=> ? [X4] : (son_of(X4,X3) & son_of(X2,X4))) [input]
4. grandson(X0,X0) [input]
5. ~! [X0] : grandson(X0,X0) [negated conjecture 4]
7. ! [X1,X0] : son_of(X0,X1) [closure 2]
8. ! [X0,X1] : (grandson(X0,X1) <=> ? [X2] : (son_of(X2,X1) & son_of(X0,X2))) [rectify 3]
9. ! [X0,X1] : (? [X2] : (son_of(X2,X1) & son_of(X0,X2)) => grandson(X0,X1)) [unused predicate definition removal 8]
11. ! [X0,X1] : (grandson(X0,X1) | ! [X2] : (~son_of(X2,X1) | ~son_of(X0,X2))) [ennf transformation 9]
12. ? [X0] : ~grandson(X0,X0) [ennf transformation 5]
13. ! [X0,X1] : son_of(X1,X0) [rectify 7]
14. ? [X0] : ~grandson(X0,X0) => ~grandson(sK0,sK0) [choice axiom]
15. ~grandson(sK0,sK0) [skolemisation 12,14]
16. son_of(X1,X0) [cnf transformation 13]
17. grandson(X0,X1) | ~son_of(X2,X1) | ~son_of(X0,X2) [cnf transformation 11]
18. ~grandson(sK0,sK0) [cnf transformation 15]
19. grandson(X0,X1) | ~son_of(X0,X2) [subsumption resolution 17,16]
20. grandson(X0,X1) [subsumption resolution 19,16]
21. $false [subsumption resolution 18,20]
% SZS output end Proof for imbecile-grandchild
% ------------------------------
% Version: Vampire 4.9 (commit 5ad494e78 on 2024-06-14 14:05:27 +0100)
% Linked with Z3 4.12.3.0 79bbbf76d0c123481c8ca05cd3a98939270074d3 z3-4.8.4-7980-g79bbbf76d

You can draw infinitely many imbecile conclusions from the imbecile doctrine!

[Skepdick]

You can also use the same imbecile axioms to prove that God is the son of himself:

Yes, you can! That's how Quines work!

You execute the algorithm and the algorithm produces...itself. The algorithm is a son of itself!

https://en.wikipedia.org/wiki/Quine_(computing)

Just so it happens that Quine-generation is precisely what most of what passes for "philosophy" is all about - spin up elaborate narrative. Solve for fixed point (usually desired conclusion).
https://en.wikipedia.org/wiki/Quine_(co ... generation

[Age]

'The son' 'grows up' to be 'the father'.
'The two' become 'the one'.

Yes, you can indeed prove that Mr. X is also his own grandfather as well as his own grandchild.

WHAT?

How could 'you' PROVE that some thing is 'its' OWN 'grandfather', exactly?

And, WHY did you SAY and WRITE, 'Yes'?

you seem to be VERY CONFUSED, here.

I NEVER EVER SAID nor WROTE ABSOLUTELY ANY thing that even REMOTELY ALLUDED TO 'you can indeed prove that 'some thing' is 'its' OWN 'something else'.

So, 'what' are you SAYING, 'Yes' TO, here, EXACTLY?

And, WHY do you BELIEVE that you could prove that "mr.x" is 'its' OWN 'grandfather'?

So, that allows us to prove the theorem of the imbecile grandchild:

BUT, LOL, you have YET TO SHOW 'us' HOW you can prove that "rr.x" is 'its' OWN 'grandfather'.

$ cat imbecile-grandchild.p
% ---------------------------------
% Imbecile doctrine in TPTP format
% ---------------------------------

% Mr.X Is God

fof(axiom1, axiom,god(MrX)).

% Mr.X is the son of God

fof(axiom2, axiom, son_of(MrX, God)).

% define grandson as the son of the son

fof(grandchild_def, axiom,
! [A, B] : (grandson(A, B) <=> ? [Z] : (son_of(A, Z) & son_of(Z, B)))).

% Theorem: Prove that MrX is his own grandchild
fof(prove_grandchild, conjecture,
grandson(MrX, MrX)).

As you can see below, the theorem of the imbecile grandchild is a perfectly logical consequence of the imbecile doctrine:

$ ./vampire imbecile-grandchild.p
% Running in auto input_syntax mode. Trying TPTP
% Refutation found. Thanks to Tanya!
% SZS status Theorem for imbecile-grandchild
% SZS output start Proof for imbecile-grandchild
2. son_of(X0,X1) [input]
3. ! [X2,X3] : (grandson(X2,X3) <=> ? [X4] : (son_of(X4,X3) & son_of(X2,X4))) [input]
4. grandson(X0,X0) [input]
5. ~! [X0] : grandson(X0,X0) [negated conjecture 4]
7. ! [X1,X0] : son_of(X0,X1) [closure 2]
8. ! [X0,X1] : (grandson(X0,X1) <=> ? [X2] : (son_of(X2,X1) & son_of(X0,X2))) [rectify 3]
9. ! [X0,X1] : (? [X2] : (son_of(X2,X1) & son_of(X0,X2)) => grandson(X0,X1)) [unused predicate definition removal 8]
11. ! [X0,X1] : (grandson(X0,X1) | ! [X2] : (~son_of(X2,X1) | ~son_of(X0,X2))) [ennf transformation 9]
12. ? [X0] : ~grandson(X0,X0) [ennf transformation 5]
13. ! [X0,X1] : son_of(X1,X0) [rectify 7]
14. ? [X0] : ~grandson(X0,X0) => ~grandson(sK0,sK0) [choice axiom]
15. ~grandson(sK0,sK0) [skolemisation 12,14]
16. son_of(X1,X0) [cnf transformation 13]
17. grandson(X0,X1) | ~son_of(X2,X1) | ~son_of(X0,X2) [cnf transformation 11]
18. ~grandson(sK0,sK0) [cnf transformation 15]
19. grandson(X0,X1) | ~son_of(X0,X2) [subsumption resolution 17,16]
20. grandson(X0,X1) [subsumption resolution 19,16]
21. $false [subsumption resolution 18,20]
% SZS output end Proof for imbecile-grandchild
% ------------------------------
% Version: Vampire 4.9 (commit 5ad494e78 on 2024-06-14 14:05:27 +0100)
% Linked with Z3 4.12.3.0 79bbbf76d0c123481c8ca05cd3a98939270074d3 z3-4.8.4-7980-g79bbbf76d

You can draw infinitely many imbecile conclusions from the imbecile doctrine!

[godelian]

How could 'you' PROVE that some thing is 'its' OWN 'grandfather', exactly?

I just did. It follows necessarily from the imbecile doctrine:

==Axioms==
Mr.X is God.
Mr.X is the son of God.

==Theorems==
Hence, Mr.X is his own grandfather.
Hence, Mr.X is simultaneously his own grandson.

I have encoded the imbecile doctrine for proof by an automated theorem prover (in TPTP format). The imbecile conclusions mentioned above undeniably follow from it. In fact, you can prove an infinite number of imbecile conclusions from the imbecile doctrine.

[Age]

How could 'you' PROVE that some thing is 'its' OWN 'grandfather', exactly?

I just did. It follows necessarily from the imbecile doctrine:

==Axioms==
Mr.X is God.
Mr.X is the son of God.

==Theorems==
Hence, Mr.X is his own grandfather.
Hence, Mr.X is simultaneously his own grandson.

Just SAYING and CLAIMING that some thing is something else is NOT proving that it is.

And by the very Fact that one thing can NOT be, in and of itself, something else PROVES your CLAIM to be not just ABSURD but also absolutely False and Wrong.

I have encoded the imbecile doctrine for proof by an automated theorem prover (in TPTP format). The imbecile conclusions mentioned above undeniably follow from it. In fact, you can prove an infinite number of imbecile conclusions from the imbecile doctrine.

Obviously you can so-called 'prove' things to "your" 'self', but you certainly are NOT necessarily 'proving' those things to ANY one ELSE.

But this is just the 'power' of BELIEF, and of CONFIRMATION BIAS.

you people can and do FOOL and DECEIVE NOT just others but even "your" OWN 'selves', AS WELL.

[godelian]

Obviously you can so-called 'prove' things to "your" 'self', but you certainly are NOT necessarily 'proving' those things to ANY one ELSE.

Axiom a1 and a2 lead to conclusion c1.

If c1 necessarily follows from a1 and a2 then you can prove c1 from a1 and a2.

You do not seem to understand the notion of "proof". Have you ever tried to use an automated theorem prover? I don't think so.

[Impenitent]

c1?

you've obviously never played in a band...

a1 and a2... music starts

-Imp

[Age]

Obviously you can so-called 'prove' things to "your" 'self', but you certainly are NOT necessarily 'proving' those things to ANY one ELSE.

Axiom a1 and a2 lead to conclusion c1.

If c1 necessarily follows from a1 and a2 then you can prove c1 from a1 and a2.

You do not seem to understand the notion of "proof". Have you ever tried to use an automated theorem prover? I don't think so.

LOL

If something is some thing, then it can NOT be something ELSE.

So, your CLAIM that something is 'one thing' - your a1, here, then it can NOT be something else - your a2.
Therefore, your OWN conclusion - your c1 does NOT follow AT ALL, let alone necessarily follow.

So, BECAUSE your c1, here, does NOT logically, necessarily, NOR even at all, follow from your a1 and a2, you have NOT proved c1 from a1 and a2 AT ALL.

you do NOT understand 'proof', NOR even just 'logical reasoning', and 'following logically'.

Have you ever tried to just IMAGINE HOW 'one thing' could even be 'something else', entirely?

If you HAD, then you WOULD HAVE SEEN, and RECOGNIZED and NOTICED, they, BY DEFINITION, those two 'DIFFERENT things' are NOT the 'SAME thing', OBVIOUSLY.

Therefore, ANY CLAIM that 'one thing' is 'one thing' AND 'something else', at the 'exact same time', is NOT just ABSURD but IS ALSO ABSOLUTELY ILLOGICAL and NONSENSICAL, to say the least.

your USE of the 'imbecile' word, quite frequently, here, may well SAY, SHOW, and EXPLAIN MORE that I have HAD TO, here.

[godelian]

c1?

you've obviously never played in a band...

a1 and a2... music starts

-Imp

Well, yeah, the TPTP format insists that you explicitly name the axioms and the theorem:

fof(id, statementtype, sentence)

The first position in the declaration is "id", which is the name that you give to the sentence.

The term "fof" stands for "first-order form". It means that you limit the sentence to first-order logic. You can also use typed first-order or even higher-order logic.

Keeping it simple, however, increases the likelihood that the reasoning engine will be able to construct a proof.

The "statementtype" is typically either "axiom", which constructs the universe in which you want to prove a sentence, or "conjecture" (or "theorem"), which is the sentence of which you seek to prove that it is true in the universe constructed.

So, in the universe constructed by the following axioms (or "basic beliefs"):

==Axioms==
Mr.X is God.
Mr.X is the son of God.

The reasoning engine can trivially prove that the following consequences necessarily follow:

==Theorems==
Hence, Mr.X is his own son.
Hence, Mr.X is his own father.
Hence, Mr.X is his own grandfather.
Hence, Mr.X is simultaneously his own grandson.
...

As I have mentioned previously, there are an infinite number of imbecile conclusions that necessarily follow from the imbecile doctrine.

In fact, you can trivially prove that the imbecile basic beliefs are in violation of the Axiom of Foundation in Zermelo-Fraenckel standard set theory:

https://en.m.wikipedia.org/wiki/Axiom_of_regularity

In mathematics, the axiom of regularity (also known as the axiom of foundation) is an axiom of Zermelo–Fraenkel set theory that states that every non-empty set A contains an element that is disjoint from A. In first-order logic, the axiom reads:

∀x(x≠∅→(∃y∈x)(y∩x=∅))

The axiom of regularity together with the axiom of pairing implies that no set is an element of itself, and that there is no infinite sequence (an) such that ai+1 is an element of ai for all i.

I just try to point out why you should not axiomatize the imbecile basic beliefs of the imbecile doctrine. Adopting imbecile basic beliefs makes you stupid. You gradually become a complete idiot.

[godelian]

you do NOT understand 'proof', NOR even just 'logical reasoning', and 'following logically'.

Since you think that you know so well what the term "proof" means, can you write an example script in TPTP format that we can supply to any automated theorem prover for the construction of a proof?

Define the axioms. Define a theorem to prove from these axioms. Write it all down in TPTP format.

I did that several times already.

If you are so fantastically good at proof, then show us your mettle.

As Linus Torvalds, author of the Linux kernel, so famously quipped: Talk is cheap. Show us the code!

[Age]

you do NOT understand 'proof', NOR even just 'logical reasoning', and 'following logically'.

Since you think that you know so well what the term "proof" means, can you write an example script in TPTP format that we can supply to any automated theorem prover for the construction of a proof?

Not before you explain what they are, to you, EXACTLY.

Define the axioms. Define a theorem to prove from these axioms. Write it all down in TPTP format.

I did that several times already.

If you are so fantastically good at proof, then show us your mettle.

As Linus Torvalds, author of the Linux kernel, so famously quipped: Talk is cheap. Show us the code!

And, what you did was just TALK, and SAY and CLAIM, that 'one thing' IS 'two DIFFERENT things'. Which, by ANY and ALL 'logic', will NEVER ACTUALLY WORK.

Now, if an 'axiom' is just a statement that is so evident or well-established, that it is accepted without controversy or question, and thus agreed upon as True, then if two or more 'axioms' are 'logically reasonably followed', then the 'conclusion' should also follow to be accepted, and agreed upon, as True.

But, OBVIOUSLY, your so-called a1 and a2 do NOT 'logically follow' AT ALL. For, AGAIN, it is NOT accepted that 'one thing' can be 'another thing' at the 'exact same time'. As just ALL could AGREE WITH.