Logic - 2017-12-07

« first day (477 days earlier) ← previous day next day → last day (2321 days later) »

David Reed

6:19 AM

Oh I remember doing this

what a pain

@user21820 A good resource to add to your list is "computability and logic" by Boolos.

user21820

Haha..

@DavidReed If it is freely available online, please tell me the link and I will add it in.

And welcome here!

Do you want to discuss your interesting question?

Q: On the permissability of uncountable languages in constructions of FOL

To me it has always been a leap in allowing uncountable languages in constructions of first-order logic. I do my best to avoid them. Unfortunately this is not always possible. I was curious if anyone could show/justify/prove that it's possible to assign a unique symbol/graphic to each real number...

David Reed

Thanks. It's not free unfortunately, but it accomplishes quite a bit. Most of the results on the right are proved in there.

Oh lol. I'm glad you found that interesting. Someone else got quite aggressive with me after posting that.

i want to clarify the context my question is arising from before getting into it. I wasn't able to screenshot the theorem so I have to type it up.

You seem to be pretty passionate on the subject though, which is nice. Seems like most mathematicians these days don't pay much attention to it anymore.

David Reed

6:49 AM

@user21820 Reading up above more have you kept up with what they've been doing at Princeton with regards to homotopy type theory becoming a new foundation for mathematics

user21820

@DavidReed I have taken a look at homotopy type theory in the recent past, and have not been convinced that it is a better foundation. I'm a rather philosophically conservative logician; I don't like to assume things that don't seem to have any non-circular justification, unless absolutely necessary.

So while I think ZFC is quite elegant, I doubt its meaningfulness, especially in its specification and replacement schemas when used impredicatively.

David Reed

what do you mean by "doubt its meaningfulness"?

I just came across it last week or so. Haven't read it. I guess they've had problems with certain elements of category theory not being first-order expressable.

user21820

@DavidReed If you have time, could you take a look at the starred post on pure computability proofs of Godel/Rosser's incompleteness theorems, and let me know if that book contains most of the contents in my post? As far as I know, there isn't any book I've come across that comes close to, because I myself learnt these stuff from a whole variety of sources.

@DavidReed Well... this is going to be an even longer discussion than for your question. Suffice to say that consistency is hardly anything, compared to soundness. Of course foundations have to be consistent, but what we definitely want is soundness (of some sort).

Take any formal system S that can reason about programs and is (arithmetically) consistent. Then S' = S+¬Con(S) is also consistent but totally unsound (Σ1-unsound). Worse still, S' |− ¬Con(S'). We will never use S' because of this, but how do we even know that our current choice of foundational system is not like S'?

David Reed

I feel like you effectively lose soundness when you lose consistency, but we may be approaching those terms differently

user21820

@DavidReed This is correct, but my point is that there are many consistent unsound systems.

Asking for mere consistency is thus not meaningful in the goal of having a foundational system.

David Reed

7:02 AM

No btw, the book discusses computability and recursion, and shows different models of computability to be equivalent, but none of the proofs on the logical side rely on any of it other than showing formulas, sentences, proofs to be recursively decidable.

It has the completeness theorem as well, touches on models, definability, normal forms etc.

I'm going to see if I can screenshot the TOC

Wikipedia refers to it as a "classic text"

George Boolos

George Stephen Boolos (September 4, 1940 – May 27, 1996) was an American philosopher and a mathematical logician who taught at the Massachusetts Institute of Technology. == Life == Boolos graduated from Princeton University in 1961 with an A.B. in mathematics. Oxford University awarded him the B.Phil. in 1963. In 1966, he obtained the first Ph.D. in philosophy ever awarded by the Massachusetts Institute of Technology, under the direction of Hilary Putnam. After teaching three years at Columbia University, he returned to MIT in 1969, where he spent the rest of his career until his death from cancer...

user21820

@DavidReed I see. Anyway if you have any feedback or erratas for my post, please let me know. I make lots of careless mistakes, but for difficult topics there are hardly any users on Math SE who are capable of checking them...

David Reed

amazon.com/Computability-Logic-George-S-Boolos-ebook/dp/… be able to read the TOC here

user21820

I also found cambridge.org/gb/academic/subjects/philosophy/logic/…

Looks like he would use the same method as Godel's.

David Reed

For incompleteness, its basically godel numbering everything and showing it to be recursive. He never constructs the sentence though. Proves something he calls the diagonal lemma and a bunch of different theorems fall out all at once.

user21820

Yes that's the typical approach.

You may be surprised at the simplicity of the computability-based approach in my post, if you haven't come across it before.

David Reed

7:13 AM

I was fixing to say, with regards to your post on the right, I've never gone through a computability proof of it so I might not be the best to critique it.

Proving it once was enough for me. Couldn't write for weeks after that :)

Absolutely I will

Alright man, I have to get to bed. I appreciate you inviting me in here, and your genuine interest in getting to know me. Once I'm off this pain medication I'll likely be able to engage a little better. Have a good night.

user21820

@DavidReed Oh have a good night's rest and see you next time!

user21820

8:01 AM

@LeakyNun Just apply the fixed-point Y combinator to f = ( x ↦ ¬⬜x ), but express the result as a sentence. Actually, I showed you and Mathmore this before, but you can try to get it again yourself. =)

Leaky Nun

8:43 AM

@user21820 hmm

13 hours later…

Leaky Nun

9:14 PM

@user21820 is it in PA?

2 hours later…

David Reed

11:08 PM

@user21820 Well the that's the leap of faith one is making when one takes axioms. What bothers me is the way people use developments within the theory to act as models for the theory itself. Some of them are a little too abstract for my taste, like ultraproducts. It also bothers me when people insist on confusing metamath with math and do things like define functions and relations as ordered pairs in the metaarena. It pops up on this site a lot and I feel like screaming at their profs.

@user21820 I feel like you and I are at an advantage, in that when you study it in school, you go into "student" mode and are more willing to blindly accept the things that are being taught to you. When you buy a bunch of texts and go through them on your own for some reason (at least for myself) one can enter into it with a healthy degree of skepticism

David Reed

11:29 PM

@user21820 I glanced through your proof. I did want to mention that I still believe the original way is still effectively a computability proof, just in a different form. The original approach was to find a system by which one could "algorithmically" prove things. The Church-Turing thesis states that the class of "effectively computable" functions are exactly the recursive ones. It is EXACTLY like creating a compiler, good analogy. As to what my thoughts are as to what creates it...

@user21820 I think it's a consequence of the fact that you've created a system that is capable of talking about itself, self-reference seems to be a common theme in a lot of paradoxes in this case. You basically make the system write out its own version of the liar paradox.

« first day (477 days earlier) ← previous day next day → last day (2321 days later) »

all rooms