Logical arguments for the death of God.

[Age]

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

Not true at all.

Obviously it is not true, for you, at all.

you have proved over and over again, and again, just how often you miss and/or misunderstand things, here.

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.

Obviously if you do not present some thing in an 'understandable language' to some thing, then that thing will not be able to determine any thing, let alone whether it is irrefutable or not.

The jsCoq page can do it, but you cannot do it.

And, it can not determine whether what is written in understandable "english" language is irrefutable or not, as well.

[godelian]

And, it can not determine whether what is written in understandable "english" language is irrefutable or not, as well.

English is not necessarily a suitable language to express irrefutable arguments in.

ChatGPT: Which language is the most suitable one to express irrefutable arguments in, English or Coq?

If your goal is to express truly irrefutable arguments, Coq is the more suitable choice.

Why Coq?

Coq is a formal proof assistant based on type theory.

It allows you to construct mathematically rigorous proofs that are machine-checked for correctness.

No room for ambiguity or rhetorical flair—just strict logic.

Why not English?

English is great for persuasion, explanation, and communication with humans.

But it's inherently imprecise and open to interpretation.

Even the clearest English arguments can be misunderstood or challenged due to linguistic ambiguity.

Summary:

Use Coq when you want a computer-verifiable, airtight proof (e.g., proving the correctness of algorithms or mathematical theorems).

Use English when you want to communicate ideas, convince people, or discuss concepts informally.

[Age]

And, it can not determine whether what is written in understandable "english" language is irrefutable or not, as well.

English is not necessarily a suitable language to express irrefutable arguments in.

Once again, when you can not refute, or, can not support, you turn to 'trying to' deflect and deceive.

If a so-claimed 'irrefutable argument' can not be expressed in a human language, then is there any point, or purpose, at all to the so-claimed 'irrefutable argument'?

If yes, then what is that point, or that purpose, exactly?

ChatGPT: Which language is the most suitable one to express irrefutable arguments in, English or Coq?

If your goal is to express truly irrefutable arguments, Coq is the more suitable choice.

Why Coq?

Coq is a formal proof assistant based on type theory.

It allows you to construct mathematically rigorous proofs that are machine-checked for correctness.

No room for ambiguity or rhetorical flair—just strict logic.

Why not English?

English is great for persuasion, explanation, and communication with humans.

But it's inherently imprecise and open to interpretation.

Even the clearest English arguments can be misunderstood or challenged due to linguistic ambiguity.

Summary:

Use Coq when you want a computer-verifiable, airtight proof (e.g., proving the correctness of algorithms or mathematical theorems).

Use English when you want to communicate ideas, convince people, or discuss concepts informally.

If you and some machine still do not the difference between an 'irrefutable argument' and just 'an argument', then so be it. But, for the 'rest of us' 'irrefutable arguments', expressed in human being understood languages, is what produces the 'proofs' needed, in order to learn, understand, and reason what is Truly Right, and Wrong, in Life.

[godelian]

But, for the 'rest of us' 'irrefutable arguments', expressed in human being understood languages, is what produces the 'proofs' needed, in order to learn, understand, and reason what is Truly Right, and Wrong, in Life.

Coq has 277 contributors:

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

That's just the development team. The number of users:

ChatGPT

Here’s a rough comparison of estimated active user bases for major proof assistants:

1. Coq

Estimated users: 2,000 – 10,000

Primary use: Formal verification, mathematics, software correctness

Community: Strong in academia, moderate open-source contributions

2. Lean (especially Lean 4)

Estimated users: 5,000 – 20,000+ (rapidly growing)

Primary use: Formal mathematics, theorem proving, programming (Lean 4)

Community: Exploding growth due to mathlib and high-profile support (e.g., Microsoft)

Trend: Lean is gaining traction among mathematicians and formal method enthusiasts faster than others

3. Isabelle/HOL

Estimated users: 1,000 – 5,000

Primary use: Formal logic, systems verification, academic research

Community: Stable, more conservative growth, widely used in some formal methods programs in Europe

4. Agda

Estimated users: 500 – 2,000

Primary use: Type theory, dependently typed programming, education

Community: Niche, mostly researchers in type theory

5. HOL4 / HOL Light / Other HOL variants

Estimated users: 200 – 1,000 each

Primary use: Hardware verification, formal logic

Community: Small, but influential in specific domains (e.g., ARM processor proofs)

These numbers are rough estimates based on GitHub activity, mailing list/forum engagement, citations, and conference presence.

That is an estimate for what I call "the rest of us" when it is about just the most popular proof assistants. There is lots of other similar but more specialized software.

Someone like me is actually not really counted in that lot because I do not even participate in things like the mailing list or conferences.

You obviously don't want to use the right tool for the right job, because what you call "the rest of us" don't either. That's fine. That's indeed one way of going through life. Everybody obviously has his own opinion on that.

[Age]

But, for the 'rest of us' 'irrefutable arguments', expressed in human being understood languages, is what produces the 'proofs' needed, in order to learn, understand, and reason what is Truly Right, and Wrong, in Life.

Coq has 277 contributors:

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

That's just the development team. The number of users:

ChatGPT

Here’s a rough comparison of estimated active user bases for major proof assistants:

1. Coq

Estimated users: 2,000 – 10,000

Primary use: Formal verification, mathematics, software correctness

Community: Strong in academia, moderate open-source contributions

2. Lean (especially Lean 4)

Estimated users: 5,000 – 20,000+ (rapidly growing)

Primary use: Formal mathematics, theorem proving, programming (Lean 4)

Community: Exploding growth due to mathlib and high-profile support (e.g., Microsoft)

Trend: Lean is gaining traction among mathematicians and formal method enthusiasts faster than others

3. Isabelle/HOL

Estimated users: 1,000 – 5,000

Primary use: Formal logic, systems verification, academic research

Community: Stable, more conservative growth, widely used in some formal methods programs in Europe

4. Agda

Estimated users: 500 – 2,000

Primary use: Type theory, dependently typed programming, education

Community: Niche, mostly researchers in type theory

5. HOL4 / HOL Light / Other HOL variants

Estimated users: 200 – 1,000 each

Primary use: Hardware verification, formal logic

Community: Small, but influential in specific domains (e.g., ARM processor proofs)

These numbers are rough estimates based on GitHub activity, mailing list/forum engagement, citations, and conference presence.

That is an estimate for what I call "the rest of us" when it is about just the most popular proof assistants. There is lots of other similar but more specialized software.

Someone like me is actually not really counted in that lot because I do not even participate in things like the mailing list or conferences.

You obviously don't want to use the right tool for the right job, because what you call "the rest of us" don't either. That's fine. That's indeed one way of going through life. Everybody obviously has his own opinion on that.

As you said, you are not yet able to actually distinguish between an 'irrefutable argument' from just 'an argument'.

[godelian]

As you said, you are not yet able to actually distinguish between an 'irrefutable argument' from just 'an argument'.

Distinguishing between an 'irrefutable argument' and 'an argument' amounts to verifying proof.
For the 'irrefutable argument', the proof verification should return 'yes'.
For a refutable argument, the proof verification should return 'no'.

For some irrefutable arguments, I can do that. For example, when arguing that "2+1=3", the irrefutable argument is:

ChatGPT

Let's now express the proof that 2+1=3 in formal first-order logic notation using Peano Arithmetic (PA).

Notation
0: constant symbol for zero
S(x): the successor of x
+: a binary function defined recursively

We'll write:
1=S(0)
2=S(S(0))
3=S(S(S(0)))

Axioms of Addition in PA:
(Add-0): ∀x(x+0=x)
(Add-S): ∀x ∀y (x+S(y)=S(x+y))

Goal:

Prove:
S(S(0))+S(0)=S(S(S(0)))

Step-by-step Formal Proof

Let’s denote:
a=S(S(0)) (i.e., 2)
b=S(0) (i.e., 1)

We want to compute a+b:

Use Add-S with x=S(S(0)),y=0:
S(S(0))+S(0)=S(S(S(0))+0)

Use Add-0 with x=S(S(S(0))):
S(S(S(0))+0)=S(S(S(0)))

Therefore:
S(S(0))+S(0)=S(S(S(0)))

Which is:
2+1=3

Final Statement:
⊢PA  S(S(0))+S(0)=S(S(S(0)))

That’s the formal proof in Peano Arithmetic.

I have verified ChatGPT's argument. He correctly uses Peano's axioms to argue that 2+1=3. The proof is flawless and therefore irrefutable.

[Age]

As you said, you are not yet able to actually distinguish between an 'irrefutable argument' from just 'an argument'.

Distinguishing between an 'irrefutable argument' and 'an argument' amounts to verifying proof.
For the 'irrefutable argument', the proof verification should return 'yes'.
For a refutable argument, the proof verification should return 'no'.

Obviously, but again you continually 'trying to' deflect and deceive is not one of your best qualities nor is it helping you in any way, here.

Once more, that you are not yet able to distinguish between an 'irrefutable argument' and just 'an argument' "yourself", and that you, still, need a machine to do it for you, explains a lot about 'the way' you speak and write, here.

For some irrefutable arguments, I can do that. For example, when arguing that "2+1=3", the irrefutable argument is:

ChatGPT

Let's now express the proof that 2+1=3 in formal first-order logic notation using Peano Arithmetic (PA).

Notation
0: constant symbol for zero
S(x): the successor of x
+: a binary function defined recursively

We'll write:
1=S(0)
2=S(S(0))
3=S(S(S(0)))

Axioms of Addition in PA:
(Add-0): ∀x(x+0=x)
(Add-S): ∀x ∀y (x+S(y)=S(x+y))

Goal:

Prove:
S(S(0))+S(0)=S(S(S(0)))

Step-by-step Formal Proof

Let’s denote:
a=S(S(0)) (i.e., 2)
b=S(0) (i.e., 1)

We want to compute a+b:

Use Add-S with x=S(S(0)),y=0:
S(S(0))+S(0)=S(S(S(0))+0)

Use Add-0 with x=S(S(S(0))):
S(S(S(0))+0)=S(S(S(0)))

Therefore:
S(S(0))+S(0)=S(S(S(0)))

Which is:
2+1=3

Final Statement:
⊢PA  S(S(0))+S(0)=S(S(S(0)))

That’s the formal proof in Peano Arithmetic.

I have verified ChatGPT's argument. He correctly uses Peano's axioms to argue that 2+1=3. The proof is flawless and therefore irrefutable.

That you actually believe that to be 'an argument', let alone an 'irrefutable argument', and that you still needed to use a machine to verify, for you, says and explains explains a lot about 'you', personally, and about 'the way' that you speak and write, here

[godelian]

That you actually believe that to be 'an argument', let alone an 'irrefutable argument'

The argument is irrefutable. There is no reasonable opposition possible to the claim:

PA ⊢ 1+2=3

you still needed to use a machine to verify, for you

Wrong!

1) I proposed the claim.
2) The machine produced an irrefutable argument for the claim.
3) I verified the machine's argument.

says and explains explains a lot about 'you', personally, and about 'the way' that you speak and write, here

You misunderstand the notion of "provability".

That is why you fail to collaborate with machines as well as with humans in the realm of discovering and verifying irrefutable arguments. You simply lack structure in what you do.

Instead of wasting your time on producing silly word salads, why don't you try to collaborate with one of the teams that manage the development of a proof assistant or a theorem prover?

You would learn a lot more by doing that.

That would require you, however, to understand that you don't know everything better than these people.

These people know a lot better than you what "provability" means. Their software exemplifies their deep knowledge on the matter. It is a constructive witness of their understanding. What exactly do you have to show for? Where is your software?

[Age]

That you actually believe that to be 'an argument', let alone an 'irrefutable argument'

The argument is irrefutable. There is no reasonable opposition possible to the claim:

PA ⊢ 1+2=3

you still needed to use a machine to verify, for you

Wrong!

1) I proposed the claim.
2) The machine produced an irrefutable argument for the claim.
3) I verified the machine's argument.

So, 'now' it is 'you' verifying 'machine's', whereas before 'you: needed 'machines' to verify if 'your: arguments were irrefutable or not.

says and explains explains a lot about 'you', personally, and about 'the way' that you speak and write, here

You misunderstand the notion of "provability".[/quote]

Yes 'we' already know that 'this' is what you believe is absolutely true, and right.

That is why you fail to collaborate with machines as well as with humans in the realm of discovering and verifying irrefutable arguments.

But, you "yourself" have not yet written a single 'irrefutable argument' that has been verified as so by any machine, as well.

You simply lack structure in what you do.

Instead of wasting your time on producing silly word salads, why don't you try to collaborate with one of the teams that manage the development of a proof assistant or a theorem prover?

I can not even get you to 'see' that one can produce 'proof' by observing things, like in the actual two examples that I have already provided, because of your 'current' belief, here.

So, again,

While one is believing some thing is true, then they are not open to what is actually irrefutably True.

When one is not open, then they can not learn.

Therefore, while you are believing what you are,here, 'godelian" you are not open to learning, and comprehending and understanding, the actual Truth of things, here, which, by the way, is in direct opposition if what you 'currently' believe is the absolute truth.

You would learn a lot more by doing that.

That would require you, however, to understand that you don't know everything better than these people.

These people know a lot better than you what "provability" means. Their software exemplifies their deep knowledge on the matter. It is a constructive witness of their understanding. What exactly do you have to show for? Where is your software?

What you are 'trying to' claim is that because one professes to being a "theologian" or a "scientist", then they have a deep knowledge of who and/or what created the whole Universe, because 'they', supposedly, know a lot more about the 'Creator' than 'me'.

'This one' is absolutely joking if it actually believe that 'those' who created some so-called 'provability machine' know a lot better about 'provability', itself, than others do, for the sole reason that is was them who built the so-called 'provability machine'.

What can be clearly seen that 'this one' has a line way to go in order to comprehend and understand 'arguing: and producing sound and valid, or, irrefutable arguments.

[godelian]

So, 'now' it is 'you' verifying 'machine's', whereas before 'you: needed 'machines' to verify if 'your: arguments were irrefutable or not.

Both humans and computers can both be provers and verifiers.

Yes 'we' already know that 'this' is what you believe is absolutely true, and right.

Truth and provability are not the same. A claim can be true. That does not mean that it would be provable. Look around you. Everything you see is true. None of it is provable.

But, you "yourself" have not yet written a single 'irrefutable argument' that has been verified as so by any machine, as well.

I actually do it quite regularly. When I send some Bitcoin to a cryptocurrency exchange, I must prove to the Bitcoin blockchain that I own them. But then again, I usually let my wallet software write the proof. I could do it by myself, but it takes a lot of work.

I can not even get you to 'see' that one can produce 'proof' by observing things, like in the actual two examples that I have already provided, because of your 'current' belief, here.

Your examples are invalid. You did not manage to produce a proof, if only, because that is impossible to do from a physical observation.

While one is believing some thing is true, then they are not open to what is actually irrefutably True.

What you can see, is true. However, it is never provable. You don't seem to understand that, do you?

[godelian]

You would learn a lot more by doing that.

That would require you, however, to understand that you don't know everything better than these people.

These people know a lot better than you what "provability" means. Their software exemplifies their deep knowledge on the matter. It is a constructive witness of their understanding. What exactly do you have to show for? Where is your software?

What you are 'trying to' claim is that because one professes to being a "theologian" or a "scientist", then they have a deep knowledge of who and/or what created the whole Universe, because 'they', supposedly, know a lot more about the 'Creator' than 'me'.

These people do not call themselves "theologian" or "scientist".

In fact, I don't know how the contributors to the Rocq/Coq software call themselves. I actually tested the Vampire theorem prover more extensively than Rocq/Coq. Theorem provers happen to be a lot easier to use than proof verifiers. I just limited myself to the fof part of the TPTP language. FoF stands for first-order form. It is just an easily typable version of the first-order logic language. I managed to pick up the TPTP/fof language in 10 minutes or so:

https://github.com/vprover/vampire

The main vampire guy is Michael Rawson (https://github.com/MichaelRawson). He calls himself a "computer scientist":

http://rawsons.uk/michael/

I am a computer scientist at the University of Southampton, UK. I am generally interested in computer reasoning systems, particularly automatic theorem provers. Google Scholar is quite good at tracking me, but I also keep a CV and a log of my academic activities, including copies of publications. You can contact me via e-mail.

These people do not claim to have "deep knowledge of who and/or what created the whole Universe". They demonstrate through their work that they have deep knowledge of provability, proof construction, and proof verification. I know that they have such deep knowledge, because otherwise, they would not be able to build this kind of software. The proof is always in the pudding. On the other hand, everything that you have said about "proof", is wrong.

You believe, however, that you know what you are talking about, even though you clearly don't. That is why I have advised you to work a bit with people like Michael Rawson. They can teach you what "proof" is. Unfortunately, you mistakenly believe that you know what you are talking about, even though you clearly do not. That is why I have advised you to work a bit with people like Michael Rawson. They can teach you what "proof" is.

[Age]

So, 'now' it is 'you' verifying 'machine's', whereas before 'you: needed 'machines' to verify if 'your: arguments were irrefutable or not.

Both humans and computers can both be provers and verifiers.

Yes 'we' already know that 'this' is what you believe is absolutely true, and right.

Truth and provability are not the same. A claim can be true. That does not mean that it would be provable. Look around you. Everything you see is true. None of it is provable.

But, you "yourself" have not yet written a single 'irrefutable argument' that has been verified as so by any machine, as well.

I actually do it quite regularly. When I send some Bitcoin to a cryptocurrency exchange, I must prove to the Bitcoin blockchain that I own them. But then again, I usually let my wallet software write the proof. I could do it by myself, but it takes a lot of work.

I can not even get you to 'see' that one can produce 'proof' by observing things, like in the actual two examples that I have already provided, because of your 'current' belief, here.

Your examples are invalid. You did not manage to produce a proof, if only, because that is impossible to do from a physical observation.

While one is believing some thing is true, then they are not open to what is actually irrefutably True.

What you can see, is true. However, it is never provable. You don't seem to understand that, do you?

That you, still, can not yet see your inconsistencies and contradictions, here, would be quite amazing, if it was not already known why you, still, can not yet 'see'.

[Age]

You would learn a lot more by doing that.

That would require you, however, to understand that you don't know everything better than these people.

These people know a lot better than you what "provability" means. Their software exemplifies their deep knowledge on the matter. It is a constructive witness of their understanding. What exactly do you have to show for? Where is your software?

What you are 'trying to' claim is that because one professes to being a "theologian" or a "scientist", then they have a deep knowledge of who and/or what created the whole Universe, because 'they', supposedly, know a lot more about the 'Creator' than 'me'.

These people do not call themselves "theologian" or "scientist".

In fact, I don't know how the contributors to the Rocq/Coq software call themselves. I actually tested the Vampire theorem prover more extensively than Rocq/Coq. Theorem provers happen to be a lot easier to use than proof verifiers. I just limited myself to the fof part of the TPTP language. FoF stands for first-order form. It is just an easily typable version of the first-order logic language. I managed to pick up the TPTP/fof language in 10 minutes or so:

https://github.com/vprover/vampire

The main vampire guy is Michael Rawson (https://github.com/MichaelRawson). He calls himself a "computer scientist":

http://rawsons.uk/michael/

I am a computer scientist at the University of Southampton, UK. I am generally interested in computer reasoning systems, particularly automatic theorem provers. Google Scholar is quite good at tracking me, but I also keep a CV and a log of my academic activities, including copies of publications. You can contact me via e-mail.

These people do not claim to have "deep knowledge of who and/or what created the whole Universe". They demonstrate through their work that they have deep knowledge of provability, proof construction, and proof verification. I know that they have such deep knowledge, because otherwise, they would not be able to build this kind of software. The proof is always in the pudding. On the other hand, everything that you have said about "proof", is wrong.

You believe, however, that you know what you are talking about, even though you clearly don't. That is why I have advised you to work a bit with people like Michael Rawson. They can teach you what "proof" is. Unfortunately, you mistakenly believe that you know what you are talking about, even though you clearly do not. That is why I have advised you to work a bit with people like Michael Rawson. They can teach you what "proof" is.

Once again you have completely and utterly missed the point, here.

But, this is not surprising at all considering you believe, absolutely, that 'proof' can not be 'seen' but is 'observed'. As well as 'proof' can not be 'observed' but is 'seen'.

[godelian]

But, this is not surprising at all considering you believe, absolutely, that 'proof' can not be 'seen' but is 'observed'. As well as 'proof' can not be 'observed' but is 'seen'.

Proof is something that proof assistant software can verify.

That does not include images or video files. Visual inputs are not considered irrefutable arguments. On the contrary, it is getting increasingly easy to fabricate deep fakes.

If the software accepts your argument as irrefutable, then I will too. Otherwise, I will not.

[Age]

But, this is not surprising at all considering you believe, absolutely, that 'proof' can not be 'seen' but is 'observed'. As well as 'proof' can not be 'observed' but is 'seen'.

Proof is something that proof assistant software can verify.

That does not include images or video files. Visual inputs are not considered irrefutable arguments. On the contrary, it is getting increasingly easy to fabricate deep fakes.

If the software accepts your argument as irrefutable, then I will too. Otherwise, I will not.

And, 'this' is, exactly, what happened to the 'ability' of adult human beings, in the days when this was being written. Some, like 'this one', literally, could not distinguish the difference of what is irrefutable, from what is refutable. That is, of course, unless some machines tells it which one is which.