Logic - 2017-12-12 (page 1 of 3)

David Reed

00:51

@Secret where is the nowhere-dense property of the integers being used?

Do you mean that it uses the fact that there is no integer between a given integer and its successor?

user21820

02:01

@DavidReed In fact, in a vast number of applications of the DCT it turns out we could do it without, because we can use hard bounds instead. That is the most ironic part.

@DavidReed I second this. Spivak's calculus is my favourite recommendation for real analysis. =)

David Reed

hard bounds?

you talking about the generalized DCT for arbitrary measures or the lebesgue measure specifically?

I've never heard the term "hard bound", I've heard of "tight bound".

user21820

@LastIronStar Feel free to ask any question about forallx (my recommended introductory book) or other books here. from the screenshots that David posted here, Boolos' book seems quite good too, though it's not exactly introductory.

David Reed

I would consider it fairly introductory for FOL, it assumes no exposure at all to formal logic

user21820

Maybe it's because the screenshots you posted are of the later chapters.

Haha.

@DavidReed There's a distinction between soft and hard analysis, where hard bounds means like explicit asymptotic bounds.

David Reed

Although it does assume exposure to mathematical proofs

LastIronStar

02:08

@user21820 Right now i'm reading Roman's Intro to Cats and forallx: Cambridge

I will definitely take you up on this offer

user21820

@DavidReed Ah that's what I want an introductory book for, to not assume ability to write proofs but rather to teach a student a deductive system in which he can do all first-order logic reasoning.

That's what I call the first level of logic, which really means "no meta-logic".

LastIronStar

in Mathematics, 21 hours ago, by LastIronStar

Howdy Navigators, I am a wayfarer in the land of mathematics looking to set sail upon the ocean that is Category Theory. I needs me a hardy perspective so that I may weather the categorial elements. A Discrete Math/Combinatorial perspective to be precise. Know ye of tome(s) on category theory that speak with such perspective?

user21820

Haha.. category theory is for those who already know logic and set theory and for some reason want another different challenge. =P

I'm half-joking above, but I seriously don't think it's very useful for discrete mathematics.

LastIronStar

I know basic logic and set theory just not formally.

David Reed

If you haven't taken abs algebra there is no point in studing cat theory

LastIronStar

02:12

well, that perspective is precisely what's being challenged by Roman's pedagogical style

@user21820 Oh, so you don't think there are books on this connection already out therE?

David Reed

that abs alg is a prereq for cat theory or that its not useful for discrete math?

LastIronStar

that AA is necessary

David Reed

I just think it would be hard to understand the notion of morphism without having taken abs alg

LastIronStar

Here's the link to the lectures by the author himself

youtube.com/playlist?list=PLiyVurqwtq0Y40IZhB6T1wM2fMduEVe56

David Reed

like group isomorphisms are the morphisms in the category of groups

homeomorphisms are morphisms in the category of topologies

I think it would be very difficult to appreciate the notion w/o prior exposure

LastIronStar

02:15

I agree that examples from a consistent perspective is useful, in any case, there are now tons of books on CS perspective to Cats which i think is closer to my needs per se

David Reed

but I can only speak for myself

LastIronStar

but the ideal candidate would be one looking from a discrete/combinatorial perspective

David Reed

what are your needs?

discrete is kind of vague

what in particular are you hoping cat theory will open up for you?

user21820

@LastIronStar The problem is that I am reasonably confident that category theory has nothing to offer the field of discrete mathematics, just as much as ZFC set theory.

Anyway I'll be away for a bit.

LastIronStar

@DavidReed well, that's the thing, i am comfortable with discrete mathematics & probability as taught from CS perspective so a cat view of things from here would help survey the lay of the land in abstract terms is what i felt

@user21820 Oh! That's a strong statement to stand by

@DavidReed new techniques

David Reed

02:21

If you are interested in comp sci you should take abs alg anyways

LastIronStar

yes, I'm planning to take it the next cycle it's being offered

David Reed

I would hold off on cat until after that

LastIronStar

There are research reasons to understand cats right now.

David Reed

Ah. Well I can't really speak to comp sci apps of cat theory

I definitely don't think its fair to say its useless for discrete math

LastIronStar

It's mostly used in theory of programming from what i've seen so far

@user21820 ttyl

user21820

02:43

@DavidReed I didn't mean useless, just as ZFC can be taken as foundational for practically all modern mathematics. But nothing to offer beyond what other more intuitive foundations can offer, such as higher-order arithmetic or some kind of type theory.

@LastIronStar People always conflate the ability of X to do Y with the necessity of X to do Y, and that irks me, hence my 'strong' statement because I do think it's true!

LastIronStar

@user21820 I completely agree with your suspicions and have personally confirmed them as well. However, I landed upon category theory out of necessary considerations than an arbitrary flight of fancy.

unfortunately, i'm not at liberty to discuss my research proposal just yet. Official business and what not.

user21820

Ah, then I'm curious to know what necessary considerations you are talking about.

Oh.

Hopefully at some point in the future you can tell us. I definitely would be interested to know.

LastIronStar

I eager to discuss it as soon as we've published our progress.

user21820

=)

LastIronStar

thank you for understanding

@user21820 What do you do for a living? (if you don't mind me asking)

user21820

02:52

I'm a research student in CS.

LastIronStar

wow that's quite close to home!

PhD?

user21820

Yes. I also love logic and foundation of mathematics. This explains why I have a distinctive perspective on various important results, such as Godel's incompleteness theorems (see the pinned post on the right).

LastIronStar

If you can spare the time, can you walk me through it?

it's quite readable so nevermind

user21820

@LastIronStar I hope so! But feel free to ask anything here. I wrote that post after holding a short discussion-style class in this very room.

LastIronStar

@user21820 lol my ignorance has a low threshold apparently, I'm taking your word and gonna try to prove the halting problem :)

user21820

03:03

@LastIronStar Sure! I think you can.

LastIronStar

So I think some kind of contradiction is needed. suppose H is a halting program, i.e., $H(P,X)$ is $\mathsf{true}$ if program $P$ halts on input $X$ and $\mathsf{false}$ otherwise.

now I vaguely remember that halting problem proof is similar to a russell's paradox style construction

user21820

@LastIronStar Do you want a hint?

LastIronStar

yes!

user21820

If H exists, you effectively have a table of truth-values for whether P halts on X.

1 row for each program P.

1 column for each input X

And now, can you construct a program using H that forces H to be wrong?

LastIronStar

ok so the cells are $1$ if $P$ terminates on $X$ and $0$ o/w

user21820

03:12

Yeap.

LastIronStar

ok, so consider $H'(P,X)$, a program constructed from $H(P,X)$ where its output is flipped along the diagonal of the truth table of $H$ i.e., physically, if $H(P_i,X_i)$ is $1$, $H'$ is $0$ on this input and vice versa. Clearly, $H'$ is not an element of the table. Thus, $H$ cannot decide whether $H'$ will terminate or not. So there is not universal halting program. Is this it?

user21820

No if H is a program then your H' is also a program and it halts on every input pair.

LastIronStar

is this on the right track even?

the idea which should be apparent is to replicate a cantor's diagonalisation argument

user21820

Well, you need to produce a program that H is wrong about. H supposedly knows whether a program halts on an input or not, so you got to do something contrary to what H thinks.

LastIronStar

ok, consider program H'(P,X) which loops forever whenever H(P,X) correctly determines that P halts on X and viceversa.

user21820

03:21

Then what would H be wrong about?

LastIronStar

execute this H(H',(P,X))

user21820

What is P,X?

LastIronStar

the arguments to H'

user21820

They are undefined so you can't execute H on them.

LastIronStar

oh, i can sorta see what you are getting at

hmmm

user21820

03:23

If you want to diagonalize, you literally need the diagonal.

LastIronStar

oh! ok run H(H',H')!

since program and input are both strings this is valid

user21820

Then your definition of H' is problematic because your H' takes two inputs.

LastIronStar

ok, so make H'(P,P)

does that fix it?

now it needs only one argument

user21820

So H' expects input P and ?

LastIronStar

sorry, let me rephrase

H'(P) halts if H determines that P(P) runs forever and vice versa

user21820

03:26

Correct.

LastIronStar

YES!

user21820

Now run H'(H').

LastIronStar

i feel good :D

user21820

Now you could either go on to the next two sections, which defines some terms and then proves Godel's incompleteness theorem.

Or you could try to prove the 'harder' unsolvability theorem in the section after that, which I called zero-guessing.

LastIronStar

isn't former necessary for latter?

user21820

03:30

No. The halting problem unsolvability will be used to prove Godel's theorem. But Godel's theorem is not related to zero-guessing.

Zero-guessing unsolvability can be used to prove Rosser's theorem, which is stronger than Godel's theorem.

LastIronStar

Key definitions concerning formal systems - could you elaborate this? It's very terse in your answer.

user21820

Oh yes my answer assumes the reader knows roughly what a formal system is haha.. That's also why one has to know at least one formal deductive system such as the one in forallx.

Basically, a formal system with a proof verifier is one that you can verify any purported proof algorithmically.

Take any formal system T. We say that V is a proof verifier for T iff all the following hold:
  V is a program.
  Given any sentence φ over T and proof x:
    V(φ,x) decides (halts and answers) whether x is a proof of φ.

That's what this part effectively says.

LastIronStar

what happens when x isn't a proof of $\phi$?

user21820

It must say "no".

LastIronStar

so it halts in both cases

user21820

03:35

Yep.

LastIronStar

ok

go on

user21820

Can you see that first-order logic has a proof verifier?

LastIronStar

@user21820 Whaaa totally lost face

user21820

Hmm.. what does "lost face" mean?

LastIronStar

I think it is better if I spent some time reading forallx so that i may do justice to your answer and/or your explanations

@user21820 as in an expression of being lost on my face.

user21820

03:37

Oh. "lost face" is an English idiom with a totally different meaning haha..

I guess it would be good to go through forallx, yes, because it essentially shows a formal deductive system for first-order logic, and you can easily see that it can be verified by a program.

LastIronStar

@user21820 i thought the adjective totally would amply convey this alt meaning

user21820

That's why I got confused. =)

LastIronStar

oh lol, sorry 'bout that

user21820

Anyway if you can accept temporarily that every conceivable useful formal system designed by humans has a proof verifier, then you can continue.

If not, you could skim through forallx to get a feel for what a formal system is.

LastIronStar

this gives me more motivation to read forallx and i'm gonna seize that opportunity

user21820

03:41

You have mathematics background, right? Then you may be able to skip the first few sections that motivate logic (to beginners), and go straight to chapter 6−7 for the description of a deductive system.

LastIronStar

@user21820 yes, I'm mathematically literate

:D

brb breakfast

user21820

Sure.

LastIronStar

okie back

user21820

03:59

@LastIronStar So do you want to read those two chapters now? If you want to just get a rough idea of what Fitch-style natural deduction is like, you could see the examples linked under Natural Deduction on my profile.

It's slightly different format from forallx, but similar enough.

LastIronStar

@user21820 I'm reading the book in sequence since it's pretty well-written.

user21820

Ah okay that's great.

LastIronStar

I should be done in a couple of hours and gotten to 6-7

maybe one hour tops i guess

user21820

Sure; no hurry and just ask anything that seems unclear.

LastIronStar

like you said, first 5 chapters seem lightweight

@user21820 btw have you heard of Fermat's Library?

user21820

04:02

@LastIronStar Now I have. =P

Never seen it before, though.

LastIronStar

@user21820 OMG logic overload

@user21820 fermatslibrary.com/s/the-emperors-old-clothes

user21820

@LastIronStar You just gave me something to read while you read, eh? Clever. =)

LastIronStar

@user21820 oh no, the jig is up :P

user21820

> the design of a program and the design of its specification must be undertaken in parallel by the same person, and they must interact with each other

I totally subscribe to this.

LastIronStar

Yes, what is a program if not its impeccable specification in situ and what is a specification if it doesn't account for externalities of actually implementing a program!

David Reed

04:17

@LastIronStar a "diagonal argument" has become a blanket term for any argument that involves self-reference

LastIronStar

Some people may disagree that externalities are not to be worried about since they can be abstracted away - but i feel this is precisely the reason to be cognisant of them if one is to abstract the program effectively! @user21820

@DavidReed Are you talking about my proof-with-help of Halting Problem up this thread?

David Reed

yes

LastIronStar

@DavidReed ok, so how would you classify the proof we arrived at?

user21820

@DavidReed Nah it's not self-reference. It's just constructing some sequence that disagrees with everything on the list of sequences at some point, and the easiest way is to use the diagonal. =)

David Reed

I would classify it as diagonal as it involves a program deciding things about itself

user21820

04:22

No it doesn't.

LastIronStar

Broadly speaking, Diagonal arguments fall into the class of proofs where you acknowledge constructive arguments are Force majeure in arriving at required contradiction as opposed to normal deductive contradictions

David Reed

russel's paradox is diagonal because it involves asking whether the set of all sets contains itself

user21820

@DavidReed: Look at the proof closely. It applies to any actual program H.

It constructs a real program H'.

And this construction itself can be implemented via another program!

Nowhere do we actually have self-reference or self-application.

LastIronStar

Could someone star my last comment!? I think it's redditgold :P

David Reed

the halting problem in general involves self-reference, I assumed that was what you were discussing

Alan Turing proved in 1936 that a general algorithm to solve the halting problem for all possible program-input pairs cannot exist. A key part of the proof was a mathematical definition of a computer and program, which became known as a Turing machine; the halting problem is undecidable over Turing machines. It is one of the first examples of a decision problem.

Informally, for any program f that might determine if programs halt, a "pathological" program g called with an input can pass its own source and its input to f and then specifically do the opposite of what f predicts g will do. No …

I apologize for not reading through carefully enough

user21820

04:24

@DavidReed That blurb is misleading.

Which I'm sure you'll agree after processing my above remarks.

Namely there is no quining going on in the proper proof.

LastIronStar

@user21820 Do you think this definition is too strict? Personally it is appealing to me as well but still...

David Reed

Wikipedia lists the halting problem as an example of a diagonal argument

I will read through your results more carefully, but I've never seen a resolution of the halting problem that doesn't use self-reference

LastIronStar

@DavidReed My first proof approach on this thread could be classified as a potential diagonal style argument but the actual proof that accomplished the resolution of the problem was not diagonal in any meaningful sense i fear

user21820

@LastIronStar Quining is a non-trivial thing. It is not obvious that programming languages support quining, and so using the ability to quine must be justified. That is why the blurb is misleading, if not wrong. We do not need quining to prove the halting problem unsolvable, and using quining is 100 times harder than the 'proper' proof.

LastIronStar

1 hour ago, by LastIronStar

@user21820 lol my ignorance has a low threshold apparently, I'm taking your word and gonna try to prove the halting problem :)

^ that's where it started

user21820

04:29

@DavidReed Diagonal arguments do not imply self-reference. Even Godel's sentence is not a matter of self-reference, if you think very very carefully about it.

LastIronStar

@user21820 Well put, I think I completely agree on this point.

David Reed

@LastIronStar if you are familiar with the idea of a diagonal argument that was my only intention--it was not argumentative, just educational

LastIronStar

@DavidReed Oh! Sorry, didn't mean to come off as rude or aggressive. apologies once again

I appreciate your interest in bettering our understanding :)

btw @DavidReed your Gravatar is not displaying

user21820

@LastIronStar It is displaying for me. Yours isn't.

David Reed

@user21820 what is your understanding of godel's sentence? I used the diagonal lemma so granted I've never constructed it, but my understanding of it was basically constructing a sentence that made statements about its own provability

LastIronStar

04:31

OMG you troll hard, your DP is just a blank white ocean of pixels!

David Reed

the diagonal lemma most definitely uses self reference

user21820

Nope.

David Reed

it involves substituting a formulas own godel number into itself

Wikipedia: In mathematical logic, the diagonal lemma or fixed point theorem establishes the existence of self-referential sentences in certain formal theories of the natural numbers—specifically those theories that are strong enough to represent all computable functions. The sentences whose existence is secured by the diagonal lemma can then, in turn, be used to prove fundamental limitative results such as Gödel's incompleteness theorems and Tarski's undefinability theorem.[1]

More likely you and I have differing definitions of self-reference. I'm not calling you wrong

user21820

A true self-reference is if something states something about itself.

Godel's sentence does not actually do that.

David Reed

what does godel's sentence say?

to my recollection it was something like : there does not exist a proof of the sentence with godel # x

the above sentence itself having godel number x

As I said, I never explicitly constructed it, but that was my understanding of it

user21820

04:37

That is a popular account of it, which is misleading.

Godel's sentence is equivalent to Q' in my post.

It is a concrete sentence that does not explicitly say anything about itself.

David Reed

Well concretely it would simply be a statement about natural numbers

user21820

It is, and if you know the proof of the fixed-point lemma you will see that it is not self-referential in any ordinary sense.

David Reed

By saying something about provability I mean by in the context of definability

defining recursive relations within the theory of arithemtic

or in this instance semi-recursive

user21820

I'm not sure what you're talking about now.

It's easier to first understand more simple instances of the diagonal argument.

David Reed

arithemetical definability

user21820

04:41

Besides the halting problem, the diagonal argument used by Cantor is equally constructive and has no self-reference. Let D = ( f ↦ ( n ↦ ¬f(n)(n) ) ).

This D is trivially implemented in any suitable programming language such as Javascript.

David Reed

you spend forever showing that the notion of provability is definable in arithmetic

user21820

I know how it is done, and there is no self-reference.

David Reed

I agree with you that theres no concrete self reference

user21820

Just think about the Cantor diagonal argument first.

David Reed

but I do think there is "effective" self reference

ok. what about it?

user21820

04:43

D is an actual program. It witnesses the fact that if you have any program f, representing a computable sequence of functions on naturals, then D(f) is a function on naturals that is not enumerated by f.

You can see that this need have nothing to do with reals, even though that is the typical application of this.

David Reed

My exposure to that argument was not in the context of computability

user21820

That's my point.

I'm trying to show that the underlying diagonal argument is purely constructive.

Sorry this is for functions from naturals to booleans.

David Reed

My exposure was both to the powerset of the naturals and to decimal reps of the reals

it was constructive

you literally plucked off the diagonal elements to get one that wasn't on the list

user21820

Yes, and there is no self-reference. See, only if you assume that the original list was the whole lot of functions from naturals to booleans, does it seem like you're creating a member that refers to the whole collection.

If you don't assume that, in the constructive view, then there is no self-reference.

David Reed

It was self-referential to me in that you were using your own purported enumeration to show that it couldn't be an enumeration

user21820

04:47

That is why I never said it was purported.

4 mins ago, by user21820

D is an actual program. It witnesses the fact that if you have any program f, representing a computable sequence of functions on naturals, then D(f) is a function on naturals that is not enumerated by f.

You can literally feed in any real program f and you will get a brand new function not enumerated by f.

David Reed

As mentioned, my own history with computability was a very brief study of complexity years ago. I'm not going to be able to process any argument involving computability notions without refereshing it for myself

It's becoming clear to me that I'm going to need to do this, as I enjoy talking to you and this is your preferred approach

user21820

Hmm.. you know programming, right?

David Reed

Yes and no, I shall tell you my history:

user21820

Consider the Javascript function function D(f) { return function(n) { return f(n)(n)+1; }; }

You can run this declaration in any browser (console).

It succeeds in defining a function D. You can then apply D to any function f you care to define. For example define function simple(n) { return function(k) { return n*k; }; }.

David Reed

during undergrad I took a c++ programming course, I found that I enjoyed it. I became obsessed with understanding how a computer worked. So I dived into assembly, then digital logic design, then I studied grammars and compiler design, then worked briefly on systems programming (windows) and op systems, Later when I took physics and chemistry I returned briefly to transistors.

As mentioned, when it comes to memory what you don't use you lose

I remember almost none of it

not even c++ :(

user21820

04:53

Oh well.

Do you understand the above two functions?

David Reed

nope

f(n)(n) is also throwing me

user21820

"f(n)(n)" when run will first see if "f" is a procedure, and if so it will execute "f(n)", and then it will check whether the result is a procedure, and if so it will execute it on "n".

If at any point it fails, then it results in an error. We don't care about that case here, so I won't bother to prevent such errors.

David Reed

so kind of like f^2(n) in a way?

nope nvm

user21820

It's "(f(n))(n)".

David Reed

[f(n)](n)

yah

LastIronStar

04:58

i think what he is doing is currying

sort of?

user21820

No it's just standard Javascript syntax.

No currying needed.

LastIronStar

my bad

David Reed

I should mention that I'm still very ill, it would be better if we could discuss this more tommorow

Transcript for

♦ $Mathematics$ Logic

Transcript for

♦ Logic

♦ $Mathematics$ Logic