Logical arguments for the death of God.

[godelian]

If 'this' is what you, still, are 'currently' believing is true, then 'you' really are an absolute imbecile.

You call me an "imbecile" because when you see things like the Coq proof assistant, you feel like an imbecile.

You are entirely right to feel like an imbecile.

Someone who thinks he perfectly well knows what "proof" means but who is totally unfamiliar with the existence of theorem provers and proof assistants, let alone their use, and definitely not their construction, is effectively an ignorant idiot, i.e. an imbecile.

You see, I am just a very humble and occasional user of that kind of software. There is an entire demographic of people who create that kind of software, who are obviously at least one level up from me, if not more. You clearly have no idea of how low you are ranked in the hierarchy of knowledge. You are so convinced that you know, but in reality, you know fuck all. Seriously, you are not even at the bottom of these things.

This is the source code repository of the Rocq/Coq proof assistant:

https://github.com/rocq-prover/rocq

If you are so knowledgeable about "proof", then demonstrate that by writing a source code patch and getting it approved by the Rocq/Coq team. There are currently 92 pull requests waiting to get integrated in the sources: https://github.com/rocq-prover/rocq/pulls

If you cannot pull that off, then please, stop pretending that you "know everything" on the subject of "proof".

[godelian]

you appear to keep forgetting that it is 'you' who made the claim, you cannot produce 'proof' by observing absolutely any thing at all.

You really do not understand what that means, do you? You cannot feed a physical observation into the Rocq/Coq proof assistant and get him to confirm it as an irrefutable argument. So, no, you cannot produce proof by (physical) observation. It cannot be done.

How many times must I repeat the same thing before it sinks in?

[godelian]

And, you have also completely forgotten that, actually, I showed, and proved, how it is very, very simple and just as easy to produce 'proof' by observing things. Full stop. End of story.

What you believe about "proof", is completely wrong.

[Age]

If 'this' is what you, still, are 'currently' believing is true, then 'you' really are an absolute imbecile.

You call me an "imbecile" because when you see things like the Coq proof assistant, you feel like an imbecile.

Once again;

1. I have never ever called you an imbecile.

2. If you, still, can not even recognize and see what is and has been going on, here, then you are being more of an imbecile, here.

3. What makes 'you' believe that 'I' am the one feeliing like an imbecile, here.

You are entirely right to feel like an imbecile.

Someone who thinks he perfectly well knows what "proof" means but who is totally unfamiliar with the existence of theorem provers and proof assistants, let alone their use, and definitely not their construction, is effectively an ignorant idiot, i.e. an imbecile.

Okay. So, will 'you' ever get around to telling 'us' what 'proof' means, exactly?

if no, then why not?

You see, I am just a very humble and occasional user of that kind of software. There is an entire demographic of people who create that kind of software, who are obviously at least one level up from me, if not more. You clearly have no idea of how low you are ranked in the hierarchy of knowledge.

What, exactly, is 'it', that people, like "yourself", use in 'your ranking', in 'your hierarchy' 'of knowledge'?

You are so convinced that you know, but in reality, you know fuck all. Seriously, you are not even at the bottom of these things.

Again, if 'this' is really what you wan to believe is absolutely true, then 'this' is, really, what you will only see.

This is the source code repository of the Rocq/Coq proof assistant:

https://github.com/rocq-prover/rocq

If you are so knowledgeable about "proof", then demonstrate that by writing a source code patch and getting it approved by the Rocq/Coq team. There are currently 92 pull requests waiting to get integrated in the sources: https://github.com/rocq-prover/rocq/pulls

If you cannot pull that off, then please, stop pretending that you "know everything" on the subject of "proof".

Have you forgotten? you, still, have not yet answered, and clarified, whether you are able to prove what you have said and claimed, here.

[godelian]

Okay. So, will 'you' ever get around to telling 'us' what 'proof' means, exactly?
if no, then why not?

I have already simplified it to:

Provide your argument to the Rocq/Coq proof assistant. If he confirms it as irrefutable, then it is "proof".

No need to install anything. You can do it in the browser at https://coq.vercel.app :

Welcome to the jsCoq Interactive Online System!

jsCoq is an interactive, web-based environment for the Coq Theorem prover, and is a collaborative development effort. See the list of contributors below.

jsCoq is open source. If you find any problem that you wish to report or want to add your own contribution, you are extremely welcome! We await your feedback at GitHub and Zulip.

A First Example: rev ∘ rev = id

The following is a simple proof that rev, the standard list reversal function as commonly defined in ML and other languages of the family, is an involution.

Again, what you are saying, is "proof" if the jsCoq page above agrees that it is.

Simple, no? Could it be any simpler?

[Age]

you appear to keep forgetting that it is 'you' who made the claim, you cannot produce 'proof' by observing absolutely any thing at all.

You really do not understand what that means, do you? You cannot feed a physical observation into the Rocq/Coq proof assistant and get him to confirm it as an irrefutable argument.

No one that I am aware of, and especially me, have never ever, ever, said that you, nor any one else, could so-call 'feed a physical observation' into any such thing as you say and claim, here.

Really, where are these imagined claims of yours coming from, exactly?

If you are unaware, and would like to have a discussion, then I could, and would, explain things, here, for you.

So, no, you cannot produce proof by (physical) observation. It cannot be done.

So, again, if you want 'proof' in written out 'pure reason' you believe, absolutely, that no one could produce 'that proof' to, nor for, 'you', correct?

How many times must I repeat the same thing before it sinks in?

But, what you are completely missing and/or misunderstanding is that I am not saying and claiming what you keep believing and assuming I am saying and claiming. Like, for example, I have never said and I am not saying and claiming that you can feed a physical observation in any such thing any such so-called 'proof assistant'.

And, it is because of this very, very skewed and distorted 'current' belief of yours, you have ended up making some of the most outrageous, absurd, and ridiculous claims, here.

Again, you claimed that you can not produce proof by observing things. And,

I say it is possible to produce proof by observing things.

Could I make this any more simpler and easier for you, here?

If yes, then how, exactly?

[Age]

And, you have also completely forgotten that, actually, I showed, and proved, how it is very, very simple and just as easy to produce 'proof' by observing things. Full stop. End of story.

What you believe about "proof", is completely wrong.

What is 'it', exactly, which you believe I believe?

If you do not answer and clarify, again, then your unsubstantiated claims are, really, nothing at all, here.

[Age]

Okay. So, will 'you' ever get around to telling 'us' what 'proof' means, exactly?
if no, then why not?

I have already simplified it to:

Provide your argument to the Rocq/Coq proof assistant. If he confirms it as irrefutable, then it is "proof".

But, 'I' was the 'first one' to ask 'you' for clarification about if you were able to do this, "yourself".

you, obviously, have still not yet answered, and clarified.

Oh, and by the way, I certainly would not use some machine made by you human beings in order to find and obtain actual 'proof' nor 'verification', here.

No need to install anything. You can do it in the browser at https://coq.vercel.app :

And, the fact that 'you', here, are 'the one' promoting and claiming that 'proof' can not be 'observed', nor obtained without 'that thing', but then you will not even use it to 'prove' and 'verify' you claim, here, show and proves just how little faith you have in your own made up belief and claim, here.

Welcome to the jsCoq Interactive Online System!

jsCoq is an interactive, web-based environment for the Coq Theorem prover, and is a collaborative development effort. See the list of contributors below.

jsCoq is open source. If you find any problem that you wish to report or want to add your own contribution, you are extremely welcome! We await your feedback at GitHub and Zulip.

A First Example: rev ∘ rev = id

The following is a simple proof that rev, the standard list reversal function as commonly defined in ML and other languages of the family, is an involution.

Again, what you are saying, is "proof" if the jsCoq page above agrees that it is.

Simple, no? Could it be any simpler?

So, 'this one' needs a machine to inform it of what is actually irrefutably True in Life.

[godelian]

So, again, if you want 'proof' in written out 'pure reason' you believe, absolutely, that no one could produce 'that proof' to, nor for, 'you', correct?

The following example is pure reason. You can find it on the jsCoq front page (https://coq.vercel.app):

Code: Select all

From Coq Require Import List.
Import ListNotations.

Lemma rev_snoc_cons A :
  forall (x : A) (l : list A), rev (l ++ [x]) = x :: rev l.
Proof.
  induction l.
  - reflexivity.
  - simpl. rewrite IHl. simpl. reflexivity.
Qed.

Theorem rev_rev A : forall (l : list A), rev (rev l) = l.
Proof.
  induction l.
  - reflexivity.
  - simpl. rewrite rev_snoc_cons. rewrite IHl.
    reflexivity.
Qed.

From Coq.Program Require Import Basics.
From Coq Require Import FunctionalExtensionality.
Open Scope program_scope.

Theorem rev_invol A : rev (A:=A) ∘ rev (A:=A) = id.
Proof.
  apply functional_extensionality.
  intro x.
  unfold compose, id. rewrite rev_rev.
  reflexivity.
Qed.

This Coq script proves that list reversal is an involution. So, concerning "involution", if you reverse a list and then reverse it again, you get the original list back. It is an irrefutable argument based exclusively on pure reason.

There are literally millions of irrefutable arguments. However, as I have pointed out already, none of your arguments are irrefutable. If you have one argument that is irrefutable, please, then paste it into the jsCoq window, so that we can verify it.

[godelian]

So, 'this one' needs a machine to inform it of what is actually irrefutably True in Life.

Try to produce one argument, just one, that this machine will verify and confirm as irrefutable. If you cannot, then absolutely none of your arguments are irrefutable.

[Age]

So, again, if you want 'proof' in written out 'pure reason' you believe, absolutely, that no one could produce 'that proof' to, nor for, 'you', correct?

The following example is pure reason. You can find it on the jsCoq front page (https://coq.vercel.app):

Code: Select all

From Coq Require Import List.
Import ListNotations.

Lemma rev_snoc_cons A :
  forall (x : A) (l : list A), rev (l ++ [x]) = x :: rev l.
Proof.
  induction l.
  - reflexivity.
  - simpl. rewrite IHl. simpl. reflexivity.
Qed.

Theorem rev_rev A : forall (l : list A), rev (rev l) = l.
Proof.
  induction l.
  - reflexivity.
  - simpl. rewrite rev_snoc_cons. rewrite IHl.
    reflexivity.
Qed.

From Coq.Program Require Import Basics.
From Coq Require Import FunctionalExtensionality.
Open Scope program_scope.

Theorem rev_invol A : rev (A:=A) ∘ rev (A:=A) = id.
Proof.
  apply functional_extensionality.
  intro x.
  unfold compose, id. rewrite rev_rev.
  reflexivity.
Qed.

This Coq script proves that list reversal is an involution. So, concerning "involution", if you reverse a list and then reverse it again, you get the original list back. It is an irrefutable argument based exclusively on pure reason.

There are literally millions of irrefutable arguments. However, as I have pointed out already, none of your arguments are irrefutable. If you have one argument that is irrefutable, please, then paste it into the jsCoq window, so that we can verify it.

Do you even have the ability to just write and express, in the understandable "english" language, just one of these so-claimed 'irrefutable arguments', which 'this thing' supposedly informs you are 'irrefutable arguments'?

If yes, then why, exactly, have you not just done this, yet?

[Age]

So, 'this one' needs a machine to inform it of what is actually irrefutably True in Life.

Try to produce one argument, just one, that this machine will verify and confirm as irrefutable.

Again, unlike you, I do not rely on 'machines' to inform me of what is actually True, Right, Accurate, and/or Correct, in Life.

It is very, very easy and simple to distinguish between an 'irrefutable argument' from an argument that is refutable.

If you cannot, then absolutely none of your arguments are irrefutable.

Have you provided an argument, here, which is irrefutable?

If yes, then which one is 'that one'.

If you do not provide one, here, then what are you so scared or afraid of, exactly?

[godelian]

Do you even have the ability to just write and express, in the understandable "english" language, just one of these so-claimed 'irrefutable arguments', which 'this thing' supposedly informs you are 'irrefutable arguments'?

Yes, for example, Gödel's incompleteness theorems:

https://github.com/rocq-community/goedel

The most famous one is Gödel's first incompleteness theorem:

(Peano) Arithmetic is inconsistent or incomplete.

alternatively:

If (Peano) arithmetic is consistent, then it is incomplete.

alternatively:

In the language of (Peano) arithmetic, there exists a statement that is true and not provable or one that is false and provable.

I can definitely write the theorem in the language of first-order logic, and supply it to the vampire theorem prover, but it will unfortunately not discover the proof (it is not powerful enough). So, I have to use the manually discovered proof and supply it to the Coq proof verifier. The result is this : https://github.com/rocq-community/goede ... /goedel1.v. Copy/paste it in jsCoq and it will verify and confirm that it is irrefutable.

Machines are lousy at discovering proof but extremely efficient at verifying it.

[godelian]

It is very, very easy and simple to distinguish between an 'irrefutable argument' from an argument that is refutable.

Not true at all. I can provide you with an argument in Coq/Rocq syntax, and I am very sure that you will not be able to determine whether it is irrefutable or not. The jsCoq page can do it, but you cannot do it.

[Age]

Do you even have the ability to just write and express, in the understandable "english" language, just one of these so-claimed 'irrefutable arguments', which 'this thing' supposedly informs you are 'irrefutable arguments'?

Yes, for example, Gödel's incompleteness theorems:

https://github.com/rocq-community/goedel

The most famous one is Gödel's first incompleteness theorem:

(Peano) Arithmetic is inconsistent or incomplete.

alternatively:

If (Peano) arithmetic is consistent, then it is incomplete.

alternatively:

In the language of (Peano) arithmetic, there exists a statement that is true and not provable or one that is false and provable.

I can definitely write the theorem in the language of first-order logic, and supply it to the vampire theorem prover, but it will unfortunately not discover the proof (it is not powerful enough). So, I have to use the manually discovered proof and supply it to the Coq proof verifier. The result is this : https://github.com/rocq-community/goede ... /goedel1.v. Copy/paste it in jsCoq and it will verify and confirm that it is irrefutable.

Machines are lousy at discovering proof but extremely efficient at verifying it.

Once again you have completely and utterly missed and misunderstood what was being said and asked for, here.

And, once more, only those with actual interest will find out what you actually missed and misunderstood, here.