Logic - 2018-03-17

« first day (577 days earlier) ← previous day next day → last day (2254 days later) »

user21820

6:22 AM

@Seriy: Hello! I noticed you've been here quite a bit. Interested in mathematical logic?

8 hours later…

Seriy

2:41 PM

@user21820 Hi! Yes, some questions arise in my mind from time to time and I seek answers in different places, including Math.SE and MO. One day I've found this room and wondered what is going on here and what are SE rooms at all.

user21820

3:30 PM

@Seriy: Hello! I just posted an answer to your question on the main site:

A: Candidates on proved false arithmetic statements

As described here you can construct over any practical $Σ_1$-sound formal system $S$ a sentence $Q$ such that $S$ proves $Q$ and also that ( if $S$ is $Σ_1$-sound then $Q$ is true but whose shortest proof over $S$ has at least on the order of $2^{10000}$ symbols ). However, I can say with complet...

There are many different rooms. Any user with a bit of reputation can create their own room, so some people have their own personal chat-room. This room was created for discussion about mathematical logic. You can find a list of some of the major chat-rooms related to Math SE here:

Q: List of chatrooms

This is a place where we could collect list of chat rooms associated with this site. There are several rooms which have potential to be useful if more users were aware of them or more users visited them. Collecting a list of such rooms here could increase their visibility. This was previously dis...

Seriy

4:13 PM

@user21820 Cool, thank you. Extremely large proofs is not a serious problem and is quite expected for me as it can be regarded as a "price" for the ability of constructing arbitrarily large numbers and having no "the biggest number". What I'm concerned about is the extension from math of finite numbers to infinite sets and doing operations on them (essentially, introducing infinitary means) adds new provable statements about finite numbers, and these are somewhat "suspicious".

user21820

@Seriy I don't actually understand your distinction. This kind of speedup theorem is mirrored in various extensions of theories of arithmetic, such as going from PA to ACA0 despite ACA0 being conservative over PA.

There is a similar speedup going from ZFC to NBG, yet NBG is conservative over ZFC.

And it's of the same flavour; the extension basically allows definitional expansion over the original.

Seriy

@user21820 Even if infinitary math proofs that the extremely large finitary proof exists, it's still doubtful until we doubt in infinitary math arithmetical soundness

user21820

You're not getting the point? ACA0 could be considered one of the weakest possible ways of extending from just natural numbers to being able to do operations on infinite sets of naturals.

Similarly, there is full second-order arithmetic Z2, which is so strong as to make many logicians worry, and still nowhere near ZFC.

Seriy

Ok, and does ACA0 proofs, say, TREE(3) exists?

I mean with not extremely large proof

user21820

But that's exactly my point; you cannot distinguish that kind of proof from the kind that I described in my post.

Ultimately, the strength of a system is closely related to the rate of growth of provably total functions over that system.

Seriy

4:22 PM

But if I could actually get it, I can be sure that it exists

user21820

Get what?

Seriy

The finitary proof of TREE(3) exists

user21820

How can you be sure that TREE(10) exists when its size is larger than the observable universe?

What does it even mean for it to exist?

Seriy

That PA can it prove

user21820

Sorry your sentence does not seem grammatical to me, and I can't understand it.

Seriy

4:25 PM

PA can prove it

With infinite sets it was proven that PA proves that TREE(3) exists. But as I doubt in arithmetical soundness, I doubt that even this large proof actually exists.

Say, it can be omega-inconsistent

user21820

@Seriy You're actually supporting my point. My post applies to any practical formal system, including PA.

You need Godel's trick to express exponentials in PA, but that's basically the only hard part.

Seriy

@user21820 Ideed, sorry, I've got it wrong. I need some time to investigate your post on the sentence construction.

user21820

It's a neat but 'cheap' trick:

Gödel's speed-up theorem

In mathematics, Gödel's speed-up theorem, proved by Gödel (1936), shows that there are theorems whose proofs can be drastically shortened by working in more powerful axiomatic systems. Kurt Gödel showed how to find explicit examples of statements in formal systems that are provable in that system but whose shortest proof is unimaginably long. For example, the statement: "This statement cannot be proved in Peano arithmetic in fewer than a googolplex symbols" is provable in Peano arithmetic (PA) but the shortest proof has at least a googolplex symbols, by an argument similar to the proof of Gödel...

In fact, now that I look at the Wikipedia article, it mentions the TREE sequence as a 'natural example'!

Anyway I need to go.

See you!

Seriy

@user21820 Thank you for your response. Have a nice day!

7 hours later…