Godel/Rosser's Incompleteness Theorem from a computability perspective

user21820

Oct 22, 2017 11:02

Okay. Hello everyone!

user400188

Hello @user21820 :)

Raute

Hi there! :-)

user21820

My plan is to first ensure that everyone understands the theorems and the proofs, then after that move on to the side remarks or further questions.

So does anyone have any questions to clarify the theorems and their proofs?

Raute

Not yet, please bear with my silent presence.

user400188

The theorems and proofs of what? The computability based proof you gave earlier?

user21820

Oct 22, 2017 11:05

Yeap.

Meaning what is called Godel's and Rosser's incompleteness theorems in the write-up.

user400188

I have yet to the end of it unfortunately.

user21820

Basically the key idea is the same in both proofs. We search for a proof of either some sentence or its negation, in order to solve the corresponding problem.

If the formal system is consistent, then we do not have to worry that it proves both. And if it is complete, then we know we will eventually find one of them.

So to get straight to the stronger incompleteness theorem, on input (P,X) we search for a proof of "The program P halts on X and outputs 0." and its negation.

Now if P really halts on X, then a sufficiently strong formal system (this is called "can reason about programs" in the write-up) will be able to prove that fact of halting as well as prove the correct output and disprove all incorrect outputs.

user400188

how should I treat "on input (P,X)"? Can i consider it as H(P,X)? Also, when it outputs, can I think of this as H(P,X) implies True?

Mathmore

Hello. Sorry for being late.

user400188

also, what is meant by a sufficiently strong formal system?

I'm not sure how familiar you are with the text; but is it similar to the systems described in "Knight Knave Island"?

user21820

Oct 22, 2017 11:14

@user400188 Yes when we run H on (P,X) it is the same as running H(P,X).

@user400188 I do not know that text, but my above comments are not meant to be rigorous but an intuitive commentary on the write-up. You still need to look at the rigorous definitions in the write-up.

Where I defined "can reason about programs".

user400188

sure

Mathmore

@user21820 I am still thinking about rosser's trick.

user21820

We say that T can reason about programs iff:
For every program P that halts on an input X and outputs Y, we have that T can prove the following for any string Z distinct from Y:
The program P halts on input X.
The program P halts on input X and outputs Y.
It is not true that the program P halts on input X and outputs Z.
---

I don't get why the indentation does not appear.

Gah never mind. Refer to the write-up.

That is precisely what I mean by "sufficiently strong".

@user400188 I'd wager that the incompleteness theorems described and proved in my write-up are far more general than in most texts. =)

@Mathmore Rosser's trick is not stated in my write-up, and is much more complicated than the zero-guessing problem. I can describe it later if we have time.

Secret

P halt X -> T
P not halt X -> F
H(P,P) = F if not halt H(P,P) not F if halt with haha
H(C,C) = not F give haha

But H(C,C) ≠ "false" iff C(C) does not halt, by definition of H.
I don't see how this last phrase follows from H, since H(P,X) must halt for any P and X as it is assumed to solve the halting problem?

user21820

@Secret Argh. I clearly messed up that.

user400188

Oct 22, 2017 11:20

I was just reading that part myself

Mathmore

@user21820 Oh I meant zero-guessing problem only.

user400188

and had the same problem i think

user21820

Given any program H that solves the halting problem:
  Let C be the program that does the following on input P:
    If H(P,P) = "false" then output "haha" otherwise infinite-loop.
  Then C(C) halts iff H(C,C) = "false", by definition of C.
  But H(C,C) = "false" iff C(C) does not halt, by definition of H.
  Contradiction.
Therefore there is no program that solves the halting problem.

I don't understand why mistakes always befall my notes.

Mathmore

It's ok @user21820. You are not alone.

user21820

@Secret @user400188: The proof that halting problem is unsolvable is such a simple well-known diagonalization that I... messed it up... Lol...

Is the above fixed proof satisfactory to you now? =)

Secret

Oct 22, 2017 11:24

analysing as you know I am bad at reading nested structures...

user21820

I also want to point out that my definitions of "consistent" and "complete" only concern sentences about programs.

This shows that even if the formal system is inconsistent and incomplete for other sentences, it cannot escape inconsistency or incompleteness for sentences about programs!

user400188

I was the process of symbolizing it in a way I can understand on paper. I think I understand it now.

Secret

P halt X -> T
P not halt X -> F
H(P,P) = F if halt with haha H(P,P) not F if not halt
H(C,C) = F give haha
H(C,C) = F not halt
...
C halt on C then H give T but then C not halt on C then H give F but then C halts...
C halt on C iff C not halt on C.

Ok, looks fine now

user21820

Great. Any other questions about that proof or the next proof?

Secret

Currently re-reading the section: === Godel's incompleteness theorem via the halting problem ===

NB: C is such a weird program which it halts only if it does not halt on itself (i.e. if H said it cannot halt)

user21820

Oct 22, 2017 11:32

@Secret C is only a program if H is a program that does as assumed. The contradiction shows that H is not, and hence C also is not.

I think I shall repost the write-up whenever someone finds a mistake so that anyone who is late won't get confused. Hopefully it won't happen too many times. =)

=== Godel/Rosser's incompleteness theorem and simple computability proofs ===

Here I shall present very simple computability-based proofs of Godel/Rosser's incompleteness theorem, which require only basic knowledge about programs. Both proofs are by contradiction, and hence do not give an explicit independent (neither provable nor disprovable) sentence. In contrast, there are proofs that give an explicit independent sentence by using essentially a fixed-point combinator applied to provability, but that are quite a bit harder to understand than the unsolvability of the halting problem. It s…

Secret

I am currently reading the whole thing line by line because I cannot digest paragraph and need to convert it into weird symbols that I can understood (but not necessary others can)

However, if I spot a mistake, I will make sure I will say in a way that others can understood

user21820

Sure. Let's see how sharp eyes you all have.

user400188

I'm working along the same lines as @Secret .

user21820

@Raute @Mathmore @Albas: Do you have any questions?

Mathmore

@user21820 currently I am writing down zero-sum problem on paper.

Raute

Oct 22, 2017 11:41

Still no questions, just ignore me. ;-)

Mathmore

"Then C halts on every input because G does. " Disn't understand this.

@user21820

user21820

C calls G(P,P).

So the reason we know that C halts on every input is because G supposedly halts on every input of the form (P,X).

Mathmore

ah okay

gotcha

user21820

We could be pedantic and say that my statement is incorrect because I only said it halts on every input pair...

So... In the final version I will amend it.

user400188

Just to clarify can I take "output "haha"" as H(P,P) and "infinite-loop" as "not H(P,P)"?

if so then my symbolization is probably correct.

Secret

Oct 22, 2017 11:47

V(φ,x) = T/F if x |- φ
T reasons (soundness?) P for Z=/=Y iff P(X,Y)=T/F then T |- H(P,X)= T and P(X,Y) = T/F and P(X,Z) = null

T consistent iff T not |- φ and not φ
T complete iff T |- φ or not φ (alternately, T not |- null φ)

Let H
V(H(P,X)=T,s)=T
V(H(P,X)=F,s)=F

T complete, consistent sound
T |- H(P,X)=T/F
s |- H(P,X)=T/F

(break)
Question:

How do we distinguish between P halts on X after some insanely long time (longer than we can be patient of thus effectively forever) and P does not halt on X?

user21820

@user400188 Not sure what you mean. C is literally a program that does a conditional branch based on the result of the call H(P,P). If the result is "false" then C outputs "haha" else C does an infinite loop.

Secret

or is the result of halt or not halt depends on the program and input involved and not so much about practically how long it runs?

Mathmore

I am wondering if G(P,X)=0 but actually P did not halt at X. Because as you say,"If P does not halt on X, then any answer is fine."

user21820

@Secret Please don't post your scratch work here just to avoid cluttering the conversation. Thanks!

@Secret Every particular program on an input will either halt or not halt. This is assumed to be the case in the foundational system where we are performing this entire proof.

Mathmore

That "arbitrary non-sense" is a good explanation that G(P,X)=0 won't happen if P doesn't halt at X

I hope it is so

user21820

Oct 22, 2017 11:53

However, I should point out that the above-mentioned assumption is only used in the proof of the weaker theorem. If I'm not mistaken, the stronger theorem holds even if we do not assume LEM for the halting problem. But this is a foundational concern that I don't want to get into at the moment. We can return to it later.

user400188

By that I meant:
outputting "haha" meant it halted and "infinite loop" meant it did not halt.

So "H(P,P)" would be true in the first case and "not H(P,P)" true in the second.

user21820

@user400188 Correct. I could perhaps make it clearer in the write-up. Thanks!

@Mathmore Yes this is possible if the formal system T was unsound for program halting.

Secret

> This implies that a solver is allowed to output arbitrary nonsense if P does not halt on X

rofl

in particular, nothing stops it from outputting 0 or 1 thus giving the wrong impression P halts on X

user21820

Correct.

Secret

hence the unsoundness

user21820

Oct 22, 2017 11:59

It's funny, but it's really the key to the stronger theorem. By only focusing on the halting behaviour, we can tackle formal systems that merely get it right for halting program executions.

In the later section I explicitly constructed a formal system that is consistent but unsound for program halting.

Mathmore

I couldn't understand soundness there.

user21820

We will get to that. Is everyone happy with the main theorems and proofs?

Mathmore

Going through " Rosser's incompleteness theorem via the zero-guessing problem"

user400188

"Given any sentence φ over T and proof x, we always have that V(φ,x) decides (halts and answers) whether x is a proof of φ"

Should I read the "V(φ,x) decides (halts and answers)" as H(V(φ,x)) or as something else?

I'm worried reading it as H(V(φ,x)) because if I did, then my definition of V would include V itself.

user21820

@user400188 We aren't defining V here. We're just defining what it means to say that a formal system has a proof verifier V.

In particular, every practical formal system ever invented by humans so far are of this type.

For example you can easily imagine a proof verifier for pure first-order logic, and also if you add axioms that can be decided by a program.

Here "axioms decided by a program" means that there is a program that always halts on every input and says whether it is an axiom or not.

@user400188: Does it make sense now?

Secret

Oct 22, 2017 12:12

A small question. What is the more technical logical term for "T can reason about programs". Is that term "independent of representations"?

user400188

I get the gist of it. It just that I prefer to symbolize things when I'm working with logic. I find it hard (near impossible) to apply an intuitive understanding (and have it work) to this subject.

Secret

I am semi opposite to you. Logic has too many nesting stuff going on that sometimes intuition is important for me to unravel the nested operations

user21820

@Secret Hmm my definition is so weak that it does not clearly imply the technical notions. Most standard texts only concern formal systems that extend PA. In the reference at the bottom I linked to a much more formal version of the stronger incompleteness theorem where in place of "can reason about programs" I use the equivalent "interprets PA−".

Secret

I see

user21820

There is a related fact that PA− is Σ[0]-complete, which means PA− can prove every true arithmetical sentence involving only bounded quantifiers.

Mathmore

Oct 22, 2017 12:17

@user21820 Why/how 'soundness' was eliminated in the proof of Rosser's incompleteness theorem via zero-guessing problem?

user21820

@Secret Together with Godel-coding to express halting of a given program execution, Σ[0]-completeness yields "can reason about programs".

@user400188 I understand. It's dangerous to rely too much on intuition. The write-up was an attempt at balancing between the intuitive and the rigorous.

@Mathmore If you understood the proof, you can 'see' that indeed it's gone. I'm not sure how to answer the philosophical question of why it can be gone. I earlier said that it's because we focus only on halting program executions.

But that may not be very satisfying; I don't know a better intuitive reason.

It's just that by focusing on things that the formal system already can do correctly (reason about any given program that actually halts on a given input), and asking whether we can decide between two behaviours, we are avoiding the need for the formal system to be sound for program halting.

Does it help?

Mathmore

Hmmm...oh

Secret

> === Encoding program execution in a string ===

Mathmore

In Rosser's we were not concerned whether P halts at X or not. We are concerned with the output of G(P,X) right?

Secret

Turing machines?

user21820

Oct 22, 2017 12:25

@Mathmore Not even that. Recall that to solve the zero-guessing problem, the solver given input (P,X) can output nonsense if P does not halt on X.

The solver only has to always halt and always 'guess right' when P actually halts on X.

Secret

I also have a suspicion that in the most general case: soundness < consistency < completeness. I had the feeling that incompleteness is the hardest one to remove from a formal system of the 3

but I had not figure out a problem in terms of programs that can demonstrate that

user21820

@Secret Nope. Read the section on soundness and consistency.

user400188

By the way @user21820; I'm not sure if you have found it already, but there is a squeal to "Forall x". Its called "Metatheory", and covers topics in logic up to completeness.

http://people.ds.cam.ac.uk/tecb2/Metatheory.pdf

user21820

@user400188 I think I hadn't found it, so thanks for letting me know and I'll look at it later.

Secret

ok nvm, I have not read in detail

> Note also that even for non-classical T, soundness for program non-halting is equivalent to just consistency, because if a program P actually halts on input X in reality, then T can prove that fact, and so if T proves "The program P does not halt on input X." then T would be inconsistent.

Albas

Oct 22, 2017 12:31

sorry@user21820 I am still reading your write up. Is it fine to ask questions here once I finish reading it?

user21820

@Albas Yes it's fine.

@Secret: I guess the way I defined consistency and soundness the latter is always stronger than the first, simply because we are in a classical meta-system.

Secret

I am thinking about something more general that includes nonclassical logic, but I am not sure how general it has to be for soundness and consistency to no longer imply one another

meanwhile I don't think I saw anything that said either soundness or consistency implies incompleteness I think...

user21820

In the meta-system (which we are now working in), we already assume that every sentence about programs is either true or false and not both, so if T is sound for programs then it can't be inconsistent (for programs).

Secret

ok, I guess I am going way too meta :P

user21820

We have to start somewhere, and we are definitely assuming a meta-system where sentences about programs are not both true and false at the same time.

So if T is sound for programs it cannot prove both a sentence about programs and its negation.

Secret

Oct 22, 2017 12:37

> since it reveals severe fundamental limitations in any consistent formal system that can reason about finite program execution, which is a very concrete notion in the real world!

some tangential thought: I wonder if some kind of incompleteness theorem also exists if we allow the program to have countable executions...

but then that's the same as not halting, so...

anyway I digress...

user21820

@Mathmore: Back to the earlier comment about unsound formal systems...

Do you understand the construction or do you want to clarify any part?

Intuitively, we start with a classical formal system S that can (it is claimed) reason about programs, and then we purposely add an axiom that is unsound but consistent with the original system.

To find such an axiom we can use the proof of the (weaker) incompleteness theorem since my particular choice of S is actually (we believe) sound for programs.

Leaky Nun

someone give me a link

user21820

It's pinned on the right. Click the "1h ago" to get there.

Leaky Nun

thanks

Mathmore

Here is my understanding of the soundness part : T is sound if T proves that P halts on X if it actually halts at X and T proves that P does not halt at X when P actually does not halt at X. To remove soundness, Rosser focused on the output of P(X) part so that T actually does not focus on proving whether P halts on X or it does not.

@user21820

user400188

Oct 22, 2017 12:49

@Mathmore I'm fairly sure there is a difference between a sound system and one that possess soundness. So you might want to be careful how you use the terminology.

user21820

@user21820 <− @Secret: What I said here is correct for full soundness. But soundness for program halting is not enough to imply consistency.

@Mathmore No this is not soundness. See the definition of "sound for program halting":

> if T proves that a program halts on an input then it really does

It does not say anything about the converse.

Mathmore

I see.

user21820

Soundness always refers to not proving false statements.

So soundness for arithmetical sentences means not proving any false arithmetical sentence.

Soundness for program halting means not proving the halting of some program on some input when it actually didn't halt.

Secret

Some other thoughts:
So halting problem shows T is either incomplete, unsound or inconsistent
and zero guessing shows T is either incomplete or inconsistent
what about the other pairs?
e.g. Problem A shows T is either unsound or inconsistent
Problem B shows T is either incomplete or unsound?

user400188

@user21820 is there a name for the property: proves(proves(P) implies P) ?

user21820

Oct 22, 2017 12:55

@user400188 It turns out that this rule for arbitrary P is actually invalid!

Secret

Another random thought: What if we took a subcollection of all possible programs such that programs of the form similar to C in the pinned paragraph above (that always give the opposite answer to what is outputted by solvers) are excluded. Will that prevent the contradiction of the halting and zero guessing problem to arise since we will then be unable to find such a C to produce the contradiction in the proof?

user400188

oh I knew that, I was just wondering if it had a name

user21820

@user400188: Hmm.. it's just the first half of the internal Lob's theorem, and I don't know if it has a name.

Mathmore

@user400188 Sound system and system possessing soundness are different things?

user21820

@Mathmore I believe some people use them interchangeably but generally logicians do not use the latter terminology.

Mathmore

Oct 22, 2017 12:58

I see.

user400188

I was given that impression from a discussion in a youtube comment a long time ago. Unfortunately, Google seems to have removed the dialog for some reason. This is a shame because the other person seemed to really know there stuff.

user21820

@Secret Your first pair doesn't make sense, if you actually think about it. Your second pair is not much point because inconsistency implies unsoundness.

@Secret No such useful formal system exists.

Remember, the incompleteness theorems do not affect all formal systems, but they certainly affect all useful ones.

Here "useful" of course includes the ability to do basic arithmetic or string manipulation.

Secret

Why will useful formal systems will imply those programs C exists?

user21820

If you don't accept basic string manipulation as a necessary feature of a useful formal system, one could question why you even accept logic itself, which is all about symbolic strings. =)

And basic string manipulation is sufficient; the mention of programs is to make the proofs easier, but if you work through the later sections you will see.

Secret

but C are those programs that output results that are opposite to the solvers (e.g. it halts when the solver said it does not halt, and it give a value of zero when the solver said it gives a nonzero value)

It does not seemed obvious to me why they are necessary in a formal system

user21820

Oct 22, 2017 13:03

@Secret I think you need to actually study the proofs carefully before you make claims. There are no solvers for either problem.

Secret

> Given any program H that solves the halting problem:
Let C be the program that does the following on input P:
If H(P,P) = "false" then output "haha" otherwise infinite-loop.
Then C(C) halts iff H(C,C) = "false", by definition of C.
But H(C,C) = "false" iff C(C) does not halt, by definition of H.
Contradiction.

user21820

GIVEN any solver, THEN we obtain a contradiction. Therefore there is absolutely no solver in the first place.

Secret

Because we can have such program C, the contradiction arises. Why is C necessary in a useful formal system

user21820

@Secret Again, please don't claim something I did not say. We cannot have such programs.

Mathmore

@user21820 What do we mean by the word 'solver'?

user21820

Oct 22, 2017 13:06

> For a program to solve the halting problem, it must halt on every input (P,X), and also must output the right answer as specified in the problem.

> For a program to solve the zero-guessing problem, it must halt on every input (P,X), and also must output the right answer as specified in the problem.

@Mathmore Are the above (quoted from the write-up) sufficiently precise?

Notice that the problems are defined in the meta-system, which assumes that any program on an input either halts or does not halt.

Mathmore

@user21820 I feel this is precise.

user21820

The answers to the problems are hence well-defined, and then the question is whether or not there is a program that solves each of them.

Secret

What is the domain of discourse of P and X? and why we need to assume a program C "If H(P,P) = "false" then output "haha" otherwise infinite-loop. ", which then we plug that into H and hence conclude there are no solvers and hence no such programs?

If the domain of discourse does not assume to have C, then we cannot plug that into H and hence will be unable to show that a contradiction arises and hence H will exist in this smaller subcollection?

@LeakyNun Perhaps you can translate that into more readable english for me?

Leaky Nun

@Secret I just came here I know nothing

user21820

@Secret We never assume C. We construct C given G.

It is obvious that this can be done in any reasonable programming language.

I could be more precise, but precision always comes at the cost of obscuring the core ideas.

@Secret: If you don't know basic programming, I'm afraid you would need to experiment with a real-world programming language to really get a feel for the meaning of the halting problem.

One basic idea is that programs can call other programs.

So if the program G existed, we can easily construct the program C that calls G on some particular combination of inputs.

The resulting contradiction shows that G cannot have existed.

@Secret There is one more issue that you bring up, concerning the domain of P and X.

It is true that I was not 100% precise in my write-up, because it is common to treat all strings as programs.

If a string P is not a valid program, we can just define its behaviour arbitrarily. For example we could simply define that P halts on every input and outputs the empty string.

BAYMAX

Oct 22, 2017 13:19

sorry to interfere,but any help on [this](math.stanford.edu/~conrad/diffgeomPage/handouts/sinecurve.pdf) in this room if some one willing to help! sorry for such a sponser here.

Secret

From your two quoted message above, a solver must halt on every input (P,X), and also must output the right answer as specified in the problem.

But I suspect the "every" will include some underlying domain of discourse. Since we knew that C plugged into H will give a contradiction thus both C and H does not exist, then there is no C in the domain of discourse to begin with, hence H cannot have an input of the form C and thus H should survive the contradiction and continue to exist?
(NB I have no idea what kind of logic I am using here, but Leaky will recognise immediately that this is a ch…

Mathmore

@Secret Existence of C follows logically. Let p : H exists. and q : C exists. Constructed $C$ when we assumed that H exists. Thus we have $p \implies q$. But existence of $C$ gave us contradiction denoted by say $c$(lower case c). Thus we got $C \implies c$. Observe that $p \implies q$ is logically equivalent to $\sim q \implies \sim p$. and $C \implies c$ is logically equivalent to $\sim c \implies \sim C$. Now observe that $\sim c \implies \sim C \implies \sim H$. Thus $H$ does not exist.

user21820

@Secret The simple answer is that there is no such collection of programs. It is the same as claiming that there is a collection of all mathematical statements that do not contradict each other.

Mathmore

@user21820 Please look at my arguments.

user400188

@Secret @user21820 It seems to me that you two are confusing "A does not exist" with "A is false".

@user21820 If they are in fact the same thing, please correct me.

user21820

Oct 22, 2017 13:23

@Mathmore Actually the argument I gave is the better one, because it is constructively valid. Yours is valid in a classical meta-system of course, so you can stick to it.

Mathmore

Okay okay. I will go with the better one.

user21820

@user400188: I don't think the problem is that @Secret is confusing "does not exist" with "false". Rather he/she thinks that it could somehow be possible to allow talking only about programs that do not do tricks like C does.

But as I said, it's like saying it's possible to allow only making mathematical claims that do not contradict one another. There is absolutely no systematic way to do that, so @Secret please give it up.

@Mathmore However, I will now demonstrate how concrete the theorem is.

I will use Javascript to literally construct C given H (sorry earlier I said G).

Since no such H actually exists, what we will instead construct is a program that given any program H will output the corresponding C.

Mathmore

@user21820 Sure.

Secret

I don't understand why we cannot do that: We first start with a collection of statements that are T or F or contradiction ( or some other truth value). Now consider some meta-program that does the following. Let H and G be solvers of the halting and zero guessing problem, plug all possible pairs of programs in the collection to H and G, and then throw away any pair that will cause a contradiction with H or G. Rinse and repeat and you should left with a collection that consists of programs that does not contradict the halting and zero guessing problems.

user21820

function C(H) { return function(P) { if( H([P,P])=="false" ) output("haha"); else while(true){} }; }

Nobody can doubt that I have just defined a valid Javascript function, assuming output has been previously defined.

Secret

Oct 22, 2017 13:32

hmm..., so for any program H we can use the above to construct a C, and you said there is no systematic way to throw that program away to avoid the contradiction

user21820

Now if you have any program H that solves the halting problem, then C(H) actually returns you a Javascript function that disproves you!

@Secret The incompleteness theorems can be used to show what I claimed earlier, namely that there is no systematic way to avoid handling such programs.

It's however too off-tangent now to be worth going onto that.

user400188

I hate to be the devils advocate; but what about very weak systems?

never mind if its too off tangent

user21820

@user400188 How weak is weak? Can it prove basic facts about string operations?

4

A: How can Peano ever be proved consistent?

You ask: How can Peano ever be proved consistent? Firstly, Peano is a person, and I'm certain that nobody can prove that he is consistent. I assume you're asking for an absolute proof of consistency of (first-order) PA. That was more or less Hilbert's goal, namely to give a finitist proof...

user400188

Ive heard about the thoery of concatination suffering from incompleteness.

user21820

@user400188 @Mathmore: See the five axioms in the above post. If any formal system proves (a translation of) those axioms and also all the theorems that can be deduced classically from them, then you end up with the system being incomplete, and unpatchably so.

I believe but have not checked thoroughly that even intuitionistic TC will be as unpatchably incomplete.

By unpatchably I mean that you can't somehow add a recursively decidable set of axioms to make it complete.

Secret

Oct 22, 2017 13:36

...or systematically throw away those results that cause problems...

user21820

@Secret Cannot. I know you're not a crank, but that's a common idea by cranks haha..

The reason is that if you try to only discard a sentence when it leads to a contradiction, you cannot identify what to throw away.

If you just throw away the last sentence involved in the proof of contradiction, you get a completely useless system.

user400188

wouldn't throwing a sentence away make you unable to reason about it? Hence making your system incomplete?

or am I misunderstanding something?

Secret

I see, makes sense, because we want to be able to utilise proof by contradiction, if I understood correctly

user21820

Well I mean something like this:

4

A: A solution for Russell's paradox

Your point (3) makes no sense at all. What precisely are you forbidding? The Russel set is just $R = \{ x : x \notin x \}$. There is absolutely no mention of $R \in R$ in the definition of $R$ itself. You cannot say that you ban the definition of $R$ because it subsequently leads to a contradicti...

Specifically this paragraph:

> you cannot say that you disallow constructing a collection S={x:φ(x)} whenever it would lead to S∈S⇔¬S∈S, simply because that latter is true if and only if the collection is contradictory!

> That means that you are doing no better than (*), which is of course useless because we cannot do mathematics without any rule that prevents writing down contradictory statements before we discover the contradiction. That is in the first place the entire goal of formalization, which is to reduce reasoning to sound rules!

@Secret So it's not even the desire to use proof by contradiction. If you ban sentences that would lead to contradiction, you essentially ban everything.

And I felt that @Secret's proposal sounds similar to my last paragraph:

> In contrast, if you enforce consistency by saying that we can write anything as long as it remains consistent with what we have written down, then we are in big trouble.

Mathmore

I want to draw parallels with set theory. Existence of H is similar to defining a set by ANY way possible. And construction of C is russell's famous set $S=\{A | A \notin A\}$. But then we get contradiction that $S \in S \iff S \notin S$. Thus it is not possible that we can define a set in any way as we please.

@user21820

user21820

Oct 22, 2017 13:43

> Firstly, it means that we can never know what is allowed to be written down! Secondly, even if we did know what is allowed (say an omniscient being told us), we would under mild conditions be able to write down a certain sequence of allowed statements leading to a certain conclusion, and write down another sequence of allowed statements leading to the opposite conclusion! (This is due to Godel's incompleteness theorem.)

Secret

> Firstly, it means that we can never know what is allowed to be written down!

I agree with this point

> Secondly, even if we did know what is allowed (say an omniscient being told us), we would under mild conditions be able to write down a certain sequence of allowed statements leading to a certain conclusion, and write down another sequence of allowed statements leading to the opposite conclusion! (This is due to Godel's incompleteness theorem.)

user21820

@Mathmore Yes it is similar in that respect.

Secret

For this one, since we ban those contradictory sentence, then in principle we are unable to proof godel's incompleteness theorem (thus it will be consistent that it does not exist). However...

Mathmore

I am not claiming that H exists. I am saying assuming it's existence leads to contradictions.

user21820

@Mathmore Sorry I thought you were @Secret lol...

Secret

Oct 22, 2017 13:45

3 mins ago, by user21820

@Secret So it's not even the desire to use proof by contradiction. If you ban sentences that would lead to contradiction, you essentially ban everything.

I agree with this statement, so that means...

Mathmore

lol @user21820

user21820

There are interesting non-trivial ways to avoid the incompleteness theorems, but none that can be easily understood without much more background in logic.

The simplest way to avoid it is to reject the closure of binary strings under concatenation.

But then nearly all logic falls apart.

No longer can we know that if A is a true sentence then ( A and A ) is a true sentence, simply because we can't even assume we can construct the longer sentence.

Secret

Tbh, I actually like the incompleteness theorems (because the null value is interesting), but I also like to wonder about the wilderness where the incompleteness theorem is avoided.

and the incompleteness theorems tell us why computers cannot tell us every answer, which is a real life scenario

user21820

@Secret I understand that; but you're really going to have to grasp the 'basics' of proof theory first before trying to dabble deeper.

@user400188 And one more thing, if you want to ask how weak the meta-system can be, ACA will do.

Secret

Btw I want to quote something...

The kind of "monster barring" strategy you describe has a long history, sometimes ultimately not so successful (Russell/Whitehead) and sometimes extremely successful (Zermelo-Frankel Set Theory). — André Nicolas Mar 18 '16 at 16:09

user400188

Oct 22, 2017 13:52

What does ACA stand for?

user21820

It's basically a system with the axioms of PA for naturals plus the ability to construct sets of naturals defined by arithmetical sentences, described briefly here:

11

A: Are sets and symbols the building blocks of mathematics?

The things you actually write on the paper or some other medium are not definable as any kind of mathematical objects. Mathematical structures can at most be used to model (or approximate) the real world structures. For example we might say that we can have strings of symbols of arbitrary length,...

The linked PDF is a good introductory reference to these weak systems.

Secret

(this will be elaborated in more detail in Mathworks) my thinking, due to weird influence of high school bullyings and me fighting them back, means when I do maths, I do monster barring alot, it often takes revealing what will be the alternative will be (which as far I know is always more exciting when it exists because it is more weird), or a convincing reason why we cannot throw away something (such as the banning everything argument above) and then I will be convinced.

user21820

Basically all we need is the assumption that sentences about programs have well-defined truth value.

Secret

monster barring is also a reason why I like weak systems, because they are often the result after monster barring a strong system, lol

user21820

@Secret I'm sorry to hear of bullying. Apart from a few occasional past mistakes, I never condone it.

Secret

Oct 22, 2017 13:57

But user21820's concern is kinda valid, because of my tendency to monster barr, I can resemble a crank a lot, and this is why I need other people to prevent me falling into a crank

user21820

Also, it's fine to think up all sorts of 'monster-barring' strategies, but it's usually more efficient to learn at least a bit of what has already been done in similar ways (reverse mathematics concerns analyzing weak systems).

Mathmore

As a student can I ask you good places to pursue PhD in Mathematical Logic?

user400188

I have the opposite problem. I dont restrict (monster barr) much at all, so I need people to advise me on what not to consider, least I become a crack.

user21820

@Mathmore Honestly I have no idea about that. Most of my current knowledge was collected from various sources all over the internet such as that cited blog post and PDFs and helpful users on Math SE.

@user400188 Lol!

Secret

it is also the reason why whenever I discuss about my weird ideas, I do it openly so if anyone spot nonsense, they can instantly point it out and explain why, thus prevent whatever self belief or pet theory to reoinforce itself

user21820

Oct 22, 2017 13:59

@Secret You could make a better philosopher than most. But it's still better for you to stay in mathematics.

@Mathmore: Are you an undergraduate student now?

Mathmore

@user21820 Nah I have done graduation. (MSc)

user21820

Hmm I don't exactly recommend PhD unless one really really wants to do research.

But if you do want to, then my advice is to look for a school with professors that work in your preferred area of logic.

Mathmore

@user21820 I am enthusiastic about research.

Okay

Secret

protip: whatever you do (unless you love computers) don't do a phD involving coding hours of code

user21820

Recently I attended a talk by Slaman; he was really good.

Secret

Oct 22, 2017 14:03

though I guess it is unavoidable nowadays...

user21820

But my knowledge was too little and I only could follow a third of his 5-day talk.

Mathmore

Mathematical logic involves coding?

user21820

In modern logic, hardly any. My viewpoints are very computability-related because I'm from a CS background.

Slaman works in recursion theory, which studies the Turing jump operation and iterates and various related problems.

user400188

I have a book on modling semantic web servers rtight in front of me.

Mathmore

To be honest I am enthusiastic about whatever I have learnt till now. Sometimes I am attracted to Topology, sometimes to abstract algebra and now with this discussion I have started liking this subject too. Why this happens?

user21820

Oct 22, 2017 14:06

@user400188 That sounds like practical application to me. It is widely believed by most proof theorists that ACA suffices for nearly all practical mathematics. =)

user400188

because math is interesting

you never actauly told me what that stands for by the way

or maybe i missed it

oh wait I saw it

user21820

Note that the constructive incompleteness theorem (which we didn't discuss) shows that ACA can't prove its own consistency, which we should believe if we use it!

Secret

until we discovered an uncountable entity in our universe, I don't think we will ever need anything beyond second order arithmetic

user21820

Ok I got to go now. See you all! Feel free to post follow-up questions on the write-up.

user400188

Thank you for the class @user21820 . I appreciate it :)

Mathmore

Oct 22, 2017 14:09

@user21820 Thanks a lot for this discussion. Bye! :)

Raute

Thanks for letting me spy on you, guys. I'll invite myself another time. :-)

user400188

Bye everyone

Simply Beautiful Art

bye

user21820

Oct 22, 2017 14:34

@Raute You're all welcome to come by any time.

@SimplyBeautifulArt: Hey you come only after the class! Lol.

@user400188 Thanks for all your participation too!

Godel/Rosser's Incompleteness Theorem from a computability perspective

♦ $Mathematics$ Logic

Participants

Godel/Rosser's Incompleteness Theorem from a computability perspective

♦ Logic

Participants

♦ $Mathematics$ Logic