On 27 Jan 2014, at 17:30, Brian Tenneson wrote:
Some basic.questions. When you say PA, do you mean the set of all
theorems entailed by the axioms of Peano arithmetic?
Yes. In some context it means only the axioms, but often I use the
same expression to denote the axioms and its logical consequences
(theorems).
Does this include the true (relative to PA of course) wffs that are
not provable from PA alone?
No.
How can it be that PA+con(I) can prove its own consistency because
it is inconsistent?
PA+con(I) is inconsistent, because it can prove its own consistency
(in one line), and that makes it inconsistent by the second
incompleteness theorem (no consistent Löbian theory can prove its own
consistency).
Then, being inconsistent, it can prove its consistency, like it can
prove any proposition.
Do you mean that it is consistent relative to itself but
inconsistent in the "metalanguage"?
No, it is totally inconsistent. It proves f by its own axioms and the
modus ponens rule.
Or else how can we have it be both consistent and inconsistent?
No. That would made us inconsistent.
This is probably way off the subject (hope that's ok with you):
isn't all mathematical truth relative to the formal system one is
operating in?
Why? I doubt this for some theories, like those who specify logically
a Turing universal system. In all case a machine will stop or not
stop, independently of the description and language used to describe
the system. But I can imagine that you are partially right for richer
theories.
"all mathematical truth is relative to the formal system one is
operating in" is relative to the formal system I call "rational
discourse" in which "mathematical discourse" and "machine-level
discourse" are sub-systems.
Hmm.... Above arithmetic, I can make some sense on this. But to just
define formal system, I need some absolute part, and I use the (second
order) distinction between finite and infinite to do this, at the
metat-level.
Bruno
On Mon, Jan 27, 2014 at 7:41 AM, Bruno Marchal <[email protected]>
wrote:
On 27 Jan 2014, at 16:12, Brian Tenneson wrote:
Yes, some day a computer might be able to figure out that the set
of rationals is not equipollent to the set of real numbers.
A Lôbian machine like ZF can do that already.
I saw somewhere that using an automated theorem prover, one of
Godel's incompleteness theorems was proved by a computer.
Boyer and Moore, yes, but that is not conceptuallydifferent than ZF,
except that the Boyer-Moore machine uses more efficient sort of AI
path.
Gödel discovered that PM already proves his own incompleteness
theorem. All Lôbian machine proves their own Gödel's theorem. They
all prove "If I am consistent, then I can't prove my consistency".
The question I raised initially was this: will there ever be a
machine or human who can correctly answer all questions with a
mathematical theme that have answers?
All? No, for any machine i in the phi_i.
But that is less clear for evolving machines, whose evolution rule
is not part of the program of the machine. Of course, at each moment
of her "life", she will be incomplete, but if her evolution is
enough "non computable", or using some special oracle, it might be
that the machine will generate the infinitely many truth of
arithmetic, but not in any provable way.
I didn't think so in my original post but now I'm starting to
wonder. It's the existence of undecidable statements that would
probably lead to the machine or human not being able to do it in
general. This reminds me of the halting problem.
Those are related. Undecidable is always relative. Consistent(PA) is
not provable by PA, but is provable in two lines in the theory PA
+con(PA). Of course PA+con(PA) cannot prove con(PA+con(PA)).
What about PA+con(I), with I = PA+con(I). It exists as we can
eliminate the occurence of I by using the Dx = "xx" method. Well, in
this case PA+con(I) can prove its own consistency, but only because
it is actually inconsistent.
The good news is we will never run out of mathematical territory to
think about.
Yes indeed, even if we confine ourselves on elementary (first order)
arithmetic. There is an infinity of surprises there.
Bruno
On Mon, Jan 27, 2014 at 6:58 AM, Gabriel Bodeen
<[email protected]> wrote:
FWIW, under the usual definitions, the rationals are enumerable and
so are a smaller set than the reals. I'd suppose that if people
can figure that out with our nifty fleshy brains, then a well-
designed computer brain could, too.
-Gabe
On Friday, January 24, 2014 1:23:40 AM UTC-6, Brian Tenneson wrote:
There are undecidable statements (about arithmetic)... There are
true statements lacking proof. There are also false statements
about arithmetic the proof of whose falsehood is impossible; not
just impossible for you and me but for a computer of any capacity
or other forms of rational processing. We'll never have a computer,
then, that will work as a mathematically-omniscient device. By that
I mean a computer such that every question that has a
mathematically-oriented theme having an answer truthfully can be
answered by such a device. Calculators demonstrate the concept but
are clearly not mathematically-omniscient: you ask the calculator
what is 2+2 and press a button and "presto" you get an answer. What
I'm talking about would be questions like "is the set of rational
numbers equal in size to the set of real numbers", and get the
correct answer. So we will never have such a computer no matter
what its capacities are, even if computer encompasses the entire
human brain. Unfortunately, that means that even for humans, we
will never know everything about math. Unless something weird would
happen and we suddenly had infinite capacities; that might change
the conclusions.
--
You received this message because you are subscribed to a topic in
the Google Groups "Everything List" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/everything-list/xabA-SKxTHM/unsubscribe
.
To unsubscribe from this group and all its topics, send an email to [email protected]
.
To post to this group, send email to everything-
[email protected].
Visit this group at http://groups.google.com/group/everything-list.
For more options, visit https://groups.google.com/groups/opt_out.
--
You received this message because you are subscribed to the Google
Groups "Everything List" group.
To unsubscribe from this group and stop receiving emails from it,
send an email to [email protected].
To post to this group, send email to everything-
[email protected].
Visit this group at http://groups.google.com/group/everything-list.
For more options, visit https://groups.google.com/groups/opt_out.
http://iridia.ulb.ac.be/~marchal/
--
You received this message because you are subscribed to a topic in
the Google Groups "Everything List" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/everything-list/xabA-SKxTHM/unsubscribe
.
To unsubscribe from this group and all its topics, send an email to [email protected]
.
To post to this group, send email to [email protected].
Visit this group at http://groups.google.com/group/everything-list.
For more options, visit https://groups.google.com/groups/opt_out.
--
You received this message because you are subscribed to the Google
Groups "Everything List" group.
To unsubscribe from this group and stop receiving emails from it,
send an email to [email protected].
To post to this group, send email to [email protected].
Visit this group at http://groups.google.com/group/everything-list.
For more options, visit https://groups.google.com/groups/opt_out.
http://iridia.ulb.ac.be/~marchal/
--
You received this message because you are subscribed to the Google Groups
"Everything List" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To post to this group, send email to [email protected].
Visit this group at http://groups.google.com/group/everything-list.
For more options, visit https://groups.google.com/groups/opt_out.
