Discussion:
What leads us to say "We don't know"
m***@wp.pl
2017-06-16 06:28:54 UTC
Raw Message
What Goedel did was mechanize the reasoning that
leads us to say "We don't know everything". He did
that by representing our reasoning with numbers
and arithmetic expressions, by fully mechanizing it.
Godel's formalism states it clearly - there is
no implication between (a is proven) and a. Right?
Tell me, do You often say "we've proven that all
consistent theories [of some kind] are incomplete,
so we can't know whether they are or not"
?
Somehow I've never meet a mathematician talking
this way. Maybe your reasoning isn't perfectly
mechanized yet and You should work harder at
Yourself.
David Bernier
2017-06-16 20:07:04 UTC
Raw Message
Post by m***@wp.pl
What Goedel did was mechanize the reasoning that
leads us to say "We don't know everything". He did
that by representing our reasoning with numbers
and arithmetic expressions, by fully mechanizing it.
Godel's formalism states it clearly - there is
no implication between (a is proven) and a. Right?
Tell me, do You often say "we've proven that all
consistent theories [of some kind] are incomplete,
so we can't know whether they are or not"
?
Somehow I've never meet a mathematician talking
this way. Maybe your reasoning isn't perfectly
mechanized yet and You should work harder at
Yourself.
Why don't you read up on Turing and the Unsolvability of
the Halting Problem for Turing machines ?

David Bernier
m***@wp.pl
2017-06-16 20:22:52 UTC
Raw Message
Post by David Bernier
Post by m***@wp.pl
What Goedel did was mechanize the reasoning that
leads us to say "We don't know everything". He did
that by representing our reasoning with numbers
and arithmetic expressions, by fully mechanizing it.
Godel's formalism states it clearly - there is
no implication between (a is proven) and a. Right?
Tell me, do You often say "we've proven that all
consistent theories [of some kind] are incomplete,
so we can't know whether they are or not"
?
Somehow I've never meet a mathematician talking
this way. Maybe your reasoning isn't perfectly
mechanized yet and You should work harder at
Yourself.
Why don't you read up on Turing and the Unsolvability of
the Halting Problem for Turing machines ?
Because it's off topic.
David Bernier
2017-06-17 05:42:18 UTC
Raw Message
Post by m***@wp.pl
Post by David Bernier
Post by m***@wp.pl
What Goedel did was mechanize the reasoning that
leads us to say "We don't know everything". He did
that by representing our reasoning with numbers
and arithmetic expressions, by fully mechanizing it.
Godel's formalism states it clearly - there is
no implication between (a is proven) and a. Right?
Tell me, do You often say "we've proven that all
consistent theories [of some kind] are incomplete,
so we can't know whether they are or not"
?
Somehow I've never meet a mathematician talking
this way. Maybe your reasoning isn't perfectly
mechanized yet and You should work harder at
Yourself.
Why don't you read up on Turing and the Unsolvability of
the Halting Problem for Turing machines ?
Because it's off topic.
Since the subject is: ``What leads us to say "We don't know" '' ,
I'd venture to say that the unsolvability of the Halting Problem
isn't off-topic:

<
https://en.wikipedia.org/wiki/Undecidable_problem#Example:_the_halting_problem_in_computability_theory
David Bernier
m***@wp.pl
2017-06-17 07:31:14 UTC
Raw Message
Post by David Bernier
Post by m***@wp.pl
Post by David Bernier
Post by m***@wp.pl
What Goedel did was mechanize the reasoning that
leads us to say "We don't know everything". He did
that by representing our reasoning with numbers
and arithmetic expressions, by fully mechanizing it.
Godel's formalism states it clearly - there is
no implication between (a is proven) and a. Right?
Tell me, do You often say "we've proven that all
consistent theories [of some kind] are incomplete,
so we can't know whether they are or not"
?
Somehow I've never meet a mathematician talking
this way. Maybe your reasoning isn't perfectly
mechanized yet and You should work harder at
Yourself.
Why don't you read up on Turing and the Unsolvability of
the Halting Problem for Turing machines ?
Because it's off topic.
Since the subject is: ``What leads us to say "We don't know" '' ,
I'd venture to say that the unsolvability of the Halting Problem
OK, let's try.
So, we have the halting problem.
And what leads us to say "we don't know"?
Godel's formalism states it clearly - there is
no implication between (a is proven) and a. Right?
Tell me, do You often say "we've proven that halting
problem is undecidable, so we can't know whether
it is or not"
?
Somehow I've never met a mathematician talking
this way.
David Bernier
2017-06-17 07:50:06 UTC
Raw Message
Post by m***@wp.pl
Post by David Bernier
Post by m***@wp.pl
Post by David Bernier
Post by m***@wp.pl
What Goedel did was mechanize the reasoning that
leads us to say "We don't know everything". He did
that by representing our reasoning with numbers
and arithmetic expressions, by fully mechanizing it.
Godel's formalism states it clearly - there is
no implication between (a is proven) and a. Right?
Tell me, do You often say "we've proven that all
consistent theories [of some kind] are incomplete,
so we can't know whether they are or not"
?
Somehow I've never meet a mathematician talking
this way. Maybe your reasoning isn't perfectly
mechanized yet and You should work harder at
Yourself.
Why don't you read up on Turing and the Unsolvability of
the Halting Problem for Turing machines ?
Because it's off topic.
Since the subject is: ``What leads us to say "We don't know" '' ,
I'd venture to say that the unsolvability of the Halting Problem
OK, let's try.
So, we have the halting problem.
And what leads us to say "we don't know"?
Godel's formalism states it clearly - there is
no implication between (a is proven) and a. Right?
Tell me, do You often say "we've proven that halting
problem is undecidable, so we can't know whether
it is or not"
?
Somehow I've never met a mathematician talking
this way.
Pretty good.

I have a tangential (maybe off-topic...) philosophical question:

Suppose I speak only Mandarin Chinese and you and I are
on the phone.

Can you then make me understand what the Polish
word form napisał means?
And if so, how? Since I know no Polish...

David Bernier
David Bernier
2017-06-17 07:53:32 UTC
Raw Message
Post by David Bernier
Post by m***@wp.pl
Post by David Bernier
Post by m***@wp.pl
Post by David Bernier
Post by m***@wp.pl
What Goedel did was mechanize the reasoning that
leads us to say "We don't know everything". He did
that by representing our reasoning with numbers
and arithmetic expressions, by fully mechanizing it.
Godel's formalism states it clearly - there is
no implication between (a is proven) and a. Right?
Tell me, do You often say "we've proven that all
consistent theories [of some kind] are incomplete,
so we can't know whether they are or not"
?
Somehow I've never meet a mathematician talking
this way. Maybe your reasoning isn't perfectly
mechanized yet and You should work harder at
Yourself.
Why don't you read up on Turing and the Unsolvability of
the Halting Problem for Turing machines ?
Because it's off topic.
Since the subject is: ``What leads us to say "We don't know" '' ,
I'd venture to say that the unsolvability of the Halting Problem
OK, let's try.
So, we have the halting problem.
And what leads us to say "we don't know"?
Godel's formalism states it clearly - there is
no implication between (a is proven) and a. Right?
Tell me, do You often say "we've proven that halting
problem is undecidable, so we can't know whether
it is or not"
?
Somehow I've never met a mathematician talking
this way.
Pretty good.
Suppose I speak only Mandarin Chinese and you and I are
on the phone.
Can you then make me understand what the Polish
word form napisał means?
And if so, how? Since I know no Polish...
David Bernier
Also, I don't know the meaning of
W, dniu, sobota, and czerwca ...
m***@wp.pl
2017-06-17 08:34:44 UTC
Raw Message
Post by David Bernier
Post by m***@wp.pl
Post by David Bernier
Post by m***@wp.pl
Post by David Bernier
Post by m***@wp.pl
What Goedel did was mechanize the reasoning that
leads us to say "We don't know everything". He did
that by representing our reasoning with numbers
and arithmetic expressions, by fully mechanizing it.
Godel's formalism states it clearly - there is
no implication between (a is proven) and a. Right?
Tell me, do You often say "we've proven that all
consistent theories [of some kind] are incomplete,
so we can't know whether they are or not"
?
Somehow I've never meet a mathematician talking
this way. Maybe your reasoning isn't perfectly
mechanized yet and You should work harder at
Yourself.
Why don't you read up on Turing and the Unsolvability of
the Halting Problem for Turing machines ?
Because it's off topic.
Since the subject is: ``What leads us to say "We don't know" '' ,
I'd venture to say that the unsolvability of the Halting Problem
OK, let's try.
So, we have the halting problem.
And what leads us to say "we don't know"?
Godel's formalism states it clearly - there is
no implication between (a is proven) and a. Right?
Tell me, do You often say "we've proven that halting
problem is undecidable, so we can't know whether
it is or not"
?
Somehow I've never met a mathematician talking
this way.
Pretty good.
Suppose I speak only Mandarin Chinese and you and I are
on the phone.
Can you then make me understand what the Polish
word form napisał means?
No.
And, returning to the subject,
Godel's formalism states it clearly - there is
no implication between (a is proven) and a. Right?
Tell me, do You often say "we've proven that all
consistent theories [of some kind] are incomplete,
so we can't know whether they are or not"
?
Somehow I've never meet a mathematician talking
this way.
Post by David Bernier
Also, I don't know the meaning of
W,  dniu,  sobota, and  czerwca ...
They are irrelevant, but I can tell You.
"w" is usually translated as "in" or "at"
"dniu" is one of gramatic cases of "dzień" i.e
"day"
"sobota" is "saturday"
"czerwca" is a gramatic case of "czerwiec"
i.e. "june".

Now, returning to the subject...
David Bernier
2017-06-18 14:02:28 UTC
Raw Message
Post by m***@wp.pl
Post by David Bernier
Post by m***@wp.pl
Post by David Bernier
Post by m***@wp.pl
Post by David Bernier
Post by m***@wp.pl
What Goedel did was mechanize the reasoning that
leads us to say "We don't know everything". He did
that by representing our reasoning with numbers
and arithmetic expressions, by fully mechanizing it.
Godel's formalism states it clearly - there is
no implication between (a is proven) and a. Right?
Tell me, do You often say "we've proven that all
consistent theories [of some kind] are incomplete,
so we can't know whether they are or not"
?
Somehow I've never meet a mathematician talking
this way. Maybe your reasoning isn't perfectly
mechanized yet and You should work harder at
Yourself.
Why don't you read up on Turing and the Unsolvability of
the Halting Problem for Turing machines ?
Because it's off topic.
Since the subject is: ``What leads us to say "We don't know" '' ,
I'd venture to say that the unsolvability of the Halting Problem
OK, let's try.
So, we have the halting problem.
And what leads us to say "we don't know"?
Godel's formalism states it clearly - there is
no implication between (a is proven) and a. Right?
Tell me, do You often say "we've proven that halting
problem is undecidable, so we can't know whether
it is or not"
?
Somehow I've never met a mathematician talking
this way.
Pretty good.
Suppose I speak only Mandarin Chinese and you and I are
on the phone.
Can you then make me understand what the Polish
word form napisał means?
No.
And, returning to the subject,
Godel's formalism states it clearly - there is
no implication between (a is proven) and a. Right?
Tell me, do You often say "we've proven that all
consistent theories [of some kind] are incomplete,
so we can't know whether they are or not"
?
Somehow I've never meet a mathematician talking
this way.
[...]

Goedel and others who think about incompleteness
study arbitrarily powerful First Order Logic
theories, with , in principle, an arbitrarily large
collection/set of axioms, and axiom schemas.

Logicians have studied formal theories or
large cardinal axioms that lead to
inconsistent theories (Frege and the
set of all sets...

" In a 1902 letter,[6] he announced the discovery to Gottlob Frege of
the paradox in Frege's 1879 Begriffsschrift and framed the problem in
terms of both logic and set theory, and in particular [...] "

Let's say mathematicians and logicians *hope* or
*believe* that ZFC set theory is consistent,
but have no expectation of proving consistency
in a simple manner.

If you polled mathematicians on whether they
KNOW/believe that ZFC set theory *is* consistent,
I think some would be cautious and say:
" I believe ZFC is consistent, but I can't say
that I can prove it ... ".

Does that seem on-topic?

David Bernier
m***@wp.pl
2017-06-18 15:37:40 UTC
Raw Message
Post by David Bernier
Post by m***@wp.pl
Post by David Bernier
Post by m***@wp.pl
Post by David Bernier
Post by m***@wp.pl
Post by David Bernier
Post by m***@wp.pl
What Goedel did was mechanize the reasoning that
leads us to say "We don't know everything". He did
that by representing our reasoning with numbers
and arithmetic expressions, by fully mechanizing it.
Godel's formalism states it clearly - there is
no implication between (a is proven) and a. Right?
Tell me, do You often say "we've proven that all
consistent theories [of some kind] are incomplete,
so we can't know whether they are or not"
?
Somehow I've never meet a mathematician talking
this way. Maybe your reasoning isn't perfectly
mechanized yet and You should work harder at
Yourself.
Why don't you read up on Turing and the Unsolvability of
the Halting Problem for Turing machines ?
Because it's off topic.
Since the subject is: ``What leads us to say "We don't know" '' ,
I'd venture to say that the unsolvability of the Halting Problem
OK, let's try.
So, we have the halting problem.
And what leads us to say "we don't know"?
Godel's formalism states it clearly - there is
no implication between (a is proven) and a. Right?
Tell me, do You often say "we've proven that halting
problem is undecidable, so we can't know whether
it is or not"
?
Somehow I've never met a mathematician talking
this way.
Pretty good.
Suppose I speak only Mandarin Chinese and you and I are
on the phone.
Can you then make me understand what the Polish
word form napisał means?
No.
And, returning to the subject,
Godel's formalism states it clearly - there is
no implication between (a is proven) and a. Right?
Tell me, do You often say "we've proven that all
consistent theories [of some kind] are incomplete,
so we can't know whether they are or not"
?
Somehow I've never meet a mathematician talking
this way.
[...]
Goedel and others who think about incompleteness
study arbitrarily powerful First Order Logic
theories, with , in principle, an arbitrarily large
collection/set of axioms, and axiom schemas.
Logicians have studied formal theories or
large cardinal axioms that lead to
inconsistent theories (Frege and the
set of all sets...
" In a 1902 letter,[6] he announced the discovery to Gottlob Frege of
the paradox in Frege's 1879 Begriffsschrift and framed the problem in
terms of both logic and set theory, and in particular [...] "
Let's say mathematicians and logicians *hope* or
*believe* that ZFC set theory is consistent,
but have no expectation of proving consistency
in a simple manner.
If you polled mathematicians on whether they
KNOW/believe that ZFC set theory *is* consistent,
" I believe ZFC is consistent, but I can't say
that I can prove it ... ".
Does that seem on-topic?
David Bernier
Yes.
Jim has claimed "What Goedel did was mechanize the reasoning that
leads us to say "We don't know everything". "
I'm claiming: no, Godel's play with a paradox of strange
properties is irrelevant to anything generally and
to the way we say "we know/we don't know" specifically.

Now: According to Godel, "x is proven"
doesn't imply x. I.e. after proving x we
still don't know - x or not x.
Is it really the way mathematicians don't
know?

David Petry
2017-06-18 04:15:22 UTC
Raw Message
Post by m***@wp.pl
What Goedel did was mechanize the reasoning that
leads us to say "We don't know everything". He did
that by representing our reasoning with numbers
and arithmetic expressions, by fully mechanizing it.
Godel's formalism states it clearly - there is
no implication between (a is proven) and a. Right?
Tell me, do You often say "we've proven that all
consistent theories [of some kind] are incomplete,
so we can't know whether they are or not"
?
Somehow I've never meet a mathematician talking
this way. Maybe your reasoning isn't perfectly
mechanized yet and You should work harder at
Yourself.
I think you've brought up a valid point. Humility alone leads us to say the we don't know everything, and Gödel's formal reasoning does nothing to increase our understanding of that. What Burn's wrote is basically poetic nonsense.
m***@wp.pl
2017-06-18 07:39:51 UTC
Raw Message
Post by David Petry
Post by m***@wp.pl
What Goedel did was mechanize the reasoning that
leads us to say "We don't know everything". He did
that by representing our reasoning with numbers
and arithmetic expressions, by fully mechanizing it.
Godel's formalism states it clearly - there is
no implication between (a is proven) and a. Right?
Tell me, do You often say "we've proven that all
consistent theories [of some kind] are incomplete,
so we can't know whether they are or not"
?
Somehow I've never meet a mathematician talking
this way. Maybe your reasoning isn't perfectly
mechanized yet and You should work harder at
Yourself.
I think you've brought up a valid point. Humility alone leads us to say the we don't know everything, and Gödel's formal reasoning does nothing to increase our understanding of that. What Burn's wrote is basically poetic nonsense.
And I think it's something much worse. It's another
philosophy of the kind "let's replace thinking with
obeying incredibly-wise-guru-invented rules".
g***@gmail.com
2017-06-18 04:22:18 UTC
Raw Message
Post by m***@wp.pl
What Goedel did was mechanize the reasoning that
leads us to say "We don't know everything". He did
that by representing our reasoning with numbers
and arithmetic expressions, by fully mechanizing it.
IN 2ND ORDER LOGIC!

AND NO... HIS DEFINITION OF PROOF WAS WRONG

"THERE IS NO GPROOF() OF THIS" by the definition of GPROOF
Post by m***@wp.pl
Godel's formalism states it clearly - there is
no implication between (a is proven) and a. Right?
of course PROOF(<ABC> , A) -> A
Post by m***@wp.pl
Tell me, do You often say "we've proven that all
consistent theories [of some kind] are incomplete,
so we can't know whether they are or not"
?
NO BECAUSE G IS BY DEFINITION NOT IN ANY AXIOMATIC THEORY

SO THERE IS A SIMPLE COMPREHENSION SCHEMA (THEOREMS MUST HAVE AXIOMS) FOR COMPLETE AXIOMATIC LOGIC
Post by m***@wp.pl
Somehow I've never meet a mathematician talking
this way. Maybe your reasoning isn't perfectly
mechanized yet and You should work harder at
Yourself.
WELL BILL GATES HAS A SPELL CHECKER NOT A THEOREM PROVER