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

1:09 AM

@user21820 do you care about fast-growing hierarchy?

2:01 AM

@LeakyNun Why not? You want Y(f) = f(Y(f)), so that Y(f) = ¬⬜Y(f). You can write a 1-parameter sentence φ such that φ(x) is true (in standard model of TC/PA−) iff ¬⬜x is true. That is how you can represent f over TC/PA−. Similarly, you can write a sentence ψ that represents Y(f) over TC/PA−. That ψ is what you want, since you can show (in MS) that ψ ≡ ¬⬜ψ over TC/PA−.

ψ is also called Godel's sentence (for the system).

Leaky Nun

@user21820 I mean, I'm figuring out how to write Y in PA

user21820

Y = ( i ↦ ( x ↦ f(x(x)) ) ( x ↦ f(x(x)) ) ), which is essentially a function from strings to strings, so it would be represented by some 2-parameter sentence y such that y(i,j) is true iff Y(i) = j.

Can you do it now?

Leaky Nun

I should think about it

where is the i consumed?

I think you mean i(x(x))

user21820

Sorry, my mistake.

Yea change the i to f. =D

@DavidReed I don't yet believe transfinite induction up to the von Neumann ordinal ω[1] is meaningful, though I know how to do it in ZFC. You may be interested in what I had to say about the circularity of a popular purported justification for ZFC here:

1

A: Why is replacement true in the intuitive hierarchy of sets?

Suppose that as each stage $S$ is completed, we take each $y$ in $x$ which is formed at $S$ and complete the stage $S_y$. When we reach the stage at which $x$ is formed, we will have formed each $y$ in $x$ and hence completed each stage $S_y$ in $\mathbf S$. This is actually a circular justi...

That makes me also not (yet) believe in the existence of an ultrafilter on N, which is necessary to construct an ultraproduct.

David Reed

@user21820 Good evening sir! Yah I'll check it out. Ultrafilter existence generally comes from AOC via Zorn's Lemma. So you are certainly not alone in the universe of people that would reject that.

user21820

2:13 AM

@DavidReed I don't have to even blindly accept anything in school. I just am aware of what system I am in. And I can easily accept proofs over ZFC as showing that ZFC proves this and that. In other words, I can remain in my preferred foundational system, and still do proofs over ZFC, just that they do not translate to truths.

@DavidReed It's not axiom of choice that is the problem. If you read my post you will see why replacement is a bigger problem.

David Reed

I see. will do.

user21820

@DavidReed I say quite often that I think Godel would have found the easier proofs had computability been around at that time. He was working before computability theory even got invented, so naturally at a disadvantage.

Turing's halting problem undecidability came after Godel's incompleteness theorem, and according to some people he got inspired by Godel's ideas...

Leaky Nun

num(n,k) := n encodes the number k
sub(res,string,repl) := res encodes the result of substiting the only free variable in what is encoded by string with n where num(n,repl)
y(i,j)(x) := (∃k)(∃xx)(sub(j,k,k)∧sub(xx,x,x)∧sub(k,i,xx))

I'm not very sure

David Reed

@LeakyNun You know I actually have virtually all of these statements written down somewhere. I'll see if I can find them. May be helpful for you.

Leaky Nun

@DavidReed thanks, but I would like to figure them out for myself...

David Reed

2:21 AM

Me too! That's why I saved them, I deviated from the book

user21820

@LeakyNun That's always the problem. I solved it by deciding never to go down the syntactic rabbit hole.

Leaky Nun

@user21820 could you verify my solution?

also, you ignored this:

user21820

I'm more of the build-the-big-gigantic-contraption-first person, then use it for everything.

Leaky Nun

1 hour ago, by Leaky Nun

@user21820 do you care about fast-growing hierarchy?

user21820

@LeakyNun I didn't; can you see I am replying to the messages in order of when they were posted?

Leaky Nun

2:22 AM

oh, sorry

user21820

But prioritizing the ones you throw at me in real time. =)

Oh I got to go. Should be back in an hour or so.

@LeakyNun I care about it in the sense that I am interested to know the limit of my own type theory, and so of course I would want to know how long a well-ordering I can create, and relatedly how fast-growing a function I can construct and prove total.

Leaky Nun

@user21820 github.com/kckennylau/ordinals/blob/master/ordinals.py

user21820

2:58 AM

@LeakyNun Can I assume this is just for ordinals below ε0? Because I see a str function that only has powers of some unicode character.

Leaky Nun

@user21820 yes

user21820

Did you see my 256-char Python program that reaches the large veblen ordinal level in the FGH before?

Leaky Nun

is that gamma_0? I forgot

user21820

No Γ0 is teeny weeny compared to even the small veblen ordinal.

in This is the Realm of Simply Beautiful Art, Mar 27 at 17:13, by user21820

@Deedlit @amWhy @SimplyBeautifulArt: I now have 256-char programs for the small and large Veblen ordinals. First I'll post the bare programs. Both are in the same style as my super-tree programs, though surprisingly the one for the large Veblen ordinal was shorter before diagonalizing. Their growth rate in terms of the initial value of c should be at least f[v*ω] in the FGH, where k is the small or large Veblen ordinal respectively.

Click to see the following messages, with golfed code for both small and large veblen ordinals, as well as the explanation of the encoding.

David Reed

Your frame in general should be elastic but also strong. Don't be a giant ball of putty for your environment to shape you into whatever it wants. Believe me when I tell you once you’ve lost track of who you are it can be quite a journey reacquiring your sense of self

Sent from my Windows 10 phone

wtf

sry

not sure how that happened

user21820

3:11 AM

@DavidReed But who wrote the paragraph?

David Reed

Me

user21820

Lol.

Was it for an essay?

David Reed

No I was typing it on my phone regarding a conversation I was having with him about elements of him that have changed since getting married.

somehow it went from my phone to my computer

user21820

That's crazy...

David Reed

I wonder if i'm logged into chat on my phone

Leaky Nun

3:14 AM

52 mins ago, by Leaky Nun

@user21820 could you verify my solution?

user21820

@DavidReed Still, it shouldn't be doing something you didn't actually ask it to do...

@LeakyNun I think I can, I think I can...

Leaky Nun

@user21820 could you?

user21820

The Little Engine That Could

The Little Engine That Could is an illustrated children's book that became widely known in the United States after publication in 1930 by Platt & Munk. The story is used to teach children the value of optimism and hard work. Based on a 2007 online poll, the National Education Association named the book one of its "Teachers' Top 100 Books for Children". == Background == The story's signature phrases such as "I think I can" first occurred in print in a 1902 article in a Swedish journal. An early published version of the story, "Story of the Engine That Thought It Could", appeared in the New-York...

Just kidding.

David Reed

The google drive folder on my comp just randomly opened as well....

user21820

@DavidReed Is it possible you have a virus? Try MBAM on your computer. I don't know what is a good anti-malware for smartphones as I don't have one...

@LeakyNun Patience is a virtue. I'm not really in math-mode yet. =)

David Reed

3:19 AM

I think I'm losing my mind

Leaky Nun

@user21820 a virtue I lack :P

@DavidReed the virus became physical :O

and @DavidReed could you share with me your formulas?

David Reed

lol I mean I'm in a state of utter perplexion

user21820

@DavidReed Seriously: malwarebytes.com

I think it's one of the more trustworthy anti-malware software available.

I hate some others that behave like rootkits themselves.

David Reed

where are you in the process? Are you showing the set of formulas to be recursive? Sentences? provability relation to be semirecursive?

user21820

@LeakyNun Logically, patience is a good thing to learn, besides logic.

Leaky Nun

3:22 AM

@DavidReed the y-combinator; aka the diagonalization operator

@user21820 how is that logical?

user21820

@DavidReed He already has formulae for syntactic manipulation. He just needs to put them together to implement the diagonalization.

David Reed

oh that's easy man

one sec

user21820

@LeakyNun Because if you have no patience, then you can't learn anything, much less logic.

Leaky Nun

@user21820 I see

user21820

But I'm being only half-serious here; don't worry. =)

Leaky Nun

3:24 AM

@user21820 how long do I need to understand why goodstein function is f_epsilon_0?

user21820

You need to just syntactically convert the iterated base representation into a ordinal by replacing the base with ω.

David Reed

i hate not being able to see rendered output prior to posting

user21820

Then the Goodstein sequence clearly translates to a decreasing sequence of ordinals less than ε0.

Leaky Nun

@user21820 oh, that wasn't what I mean

I mean, let n be a number, and let f(n) be the step at which the Goodstein sequence starting at n terminates, i.e. vanishes

how do I see that f is f_epsilon_0 in the FGH?

David Reed

$\exists x (x = num(A) \land A(x))$ is called the diagonalization of A

user21820

3:28 AM

It is the same reasoning, because the Goodstein function grows faster than every function in a level below ε0.

Leaky Nun

@DavidReed that's extremely unrigorous :P

David Reed

atm I'm making sure that this is what you're talking about

Leaky Nun

and how do I know that?

user131753

@user21820 Regarding (1) I would like to mention that modern interpretations of type theory differs from Russell's own ideas significantly (I remember seeing a paper on it once, probably by Landini but can't find the link now).

user21820

@user170039 There are hundreds of different modern type theories, so yes trivially true.

Though in that remark I was referring to the fact that there are other writings that express Russell's theory of types much more cleanly than Russell himself.

user131753

3:30 AM

@user21820 For example?

David Reed

Leaky Nun

@DavidReed the y-combinator is a function that takes in, informally, formulas with one free variable, say φ, and gives you ψ such that "ψ iff φ(ψ)" is provable in PA

David Reed

Leaky Nun

right, 17.1 is what I'm looking for

David Reed

glad to help :)

user21820

3:33 AM

@user170039 Well I can't recall all the good writings I've seen, but it looks like SEP's article is a reasonable starting point. You can see that it makes use of modern syntactic notions like BNF, things which simply didn't exist at the time of Russell.

user131753

@user21820 So far I can recall, Landini's point of attack was Church's version of Simple Type Theory and $\lambda$-calculus (he probably also mentions Gödel, but I can't remember precisely).

user21820

@user170039 I don't get your point; if you're claiming that simple type theory does not capture Russell's ideas accurately, well of course there's no axiom of reducibility, which is philosophically unfounded anyway. But what else is missing?

@LeakyNun Yeap what David showed you is following the standard approach, which is not to go straight to the fixed-point combinator but to split into two stages.

user131753

@user21820 I think that I will have to look for that article to give a detailed answer of this question. But for now I am slightly busy. I will do this when I get time (and if I don't forget).

user21820

@user170039 Sure.

David Reed

Ah ok. Sry if that's not what you are after

user21820

3:45 AM

It's equivalent, in a sense. Just not so clear why anyone should consider the smaller steps without the bigger picture.

user131753

@user21820 Although I think you will find Bernard Linsky's articles and book The Evolution of Principia Mathematica: Bertrand Russell's Manuscripts and Notes for the Second Edition to be interesting.

user131753

For example you may go through this article (although I must say that this is not the article about which I was talking earlier).

user21820

@DavidReed @LeakyNun: Basically, the diag representation in your book is doing the self-application of a string function x to itself to get x(x).

Leaky Nun

so Diag(x,y) := Sub(y,x,x)?

David Reed

T or F: There are exceptions to every rule.

Leaky Nun

3:50 AM

2 hours ago, by Leaky Nun

num(n,k) := n encodes the number k
sub(res,string,repl) := res encodes the result of substiting the only free variable in what is encoded by string with n where num(n,repl)
y(i,j)(x) := (∃k)(∃xx)(sub(j,k,k)∧sub(xx,x,x)∧sub(k,i,xx))

notations

David Reed

one sec. I'll give you more context:

user21820

@DavidReed Very funny.

Do you know my answer to that quine of question?

6

A: Is Godel's modified liar an illogical statement?

Your question has two main facets. The first is that you did not grasp the way logic does not fall to the liar paradoxes. The second is that there are deeper reasons as to why we have such apparently innocuous sentences in natural language that seem to defy assimilation into formal logic systems....

David Reed

* refers to concatenation btw

lol

I came up with that one time when I was going through this

user21820

It took me a few seconds to see through it heheh..

David Reed

It's not necessarily contradictory though, its false.

if its true then its both true and false, if its false then its just false.

user21820

3:57 AM

Yea, but the first line of thought is "It's true, right?"

David Reed

lol

user21820

But have you seen Quine's paradox?

If you haven't, you might enjoy trying to figure out what's wrong with it before reading my proposed resolution of it in the later part of my post.

David Reed

I pseudo glanced at it: Context: I come off of my pain medication every once in awhile to keep my tolerance low. One of the medications I will take to attenuate the symptoms is ambien. This has the effect of rendering my frontal lobe effectively worthless. My ability to absorb anything atm is extremely compromised.

user21820

I see.

Do you mind telling roughly what the pain medication is for?

David Reed

Repetitive stress injury in my hands...bilateral... Overuse of guitar and keyboard. Basically I ignored my body when it started to say no....now permantely damaged. Being a math major didn't help either

Leaky Nun

4:02 AM

let's say that for all x, if f(x)=m, then ⊢(∀y)(F(x,y)⟺y=m), and do the same for g to have G; how do I have a sentence H(x,y) that says y=g(f(x))?

David Reed

Oh

user21820

@DavidReed Does it get better if you totally rest for a week or two?

David Reed

So that's the definition of a function being representable in arithmetic

Leaky Nun

yes, but how to represent the composition?

user131753

@user21820: I think that this was the article.

David Reed

4:04 AM

earlier in the book its proven that for any recursive function one can find such a formula

Let me look really quick at where you are at.

user21820

@LeakyNun You do one at a time. ∃t ( y=g(t) ∧ t=f(x) ).

Leaky Nun

thanks

user21820

@user170039 I will read both when I'm free. Thanks.

@DavidReed I think he wants the actual gigantic expression and not a meta-theorem stating that it exists...

David Reed

@user21820 Not really. Have had it for years. It's more treatment-oriented now than curative in terms of approach.

ah

I actually think that may be in there in part two

Leaky Nun

@user21820 was it that gigantic?

David Reed

4:06 AM

let me see.

user21820

@LeakyNun It will be once you put in the formulae for the Godel encoding of the entire system.

David Reed

I know that they've actually come up with it and tested it in a computer.

Leaky Nun

what?

user21820

That's why I will never do it unless someone's life depends on it.

Leaky Nun

what you gave me was what I needed

David Reed

4:07 AM

ah ok

user21820

@LeakyNun Yes but it's using stuff that aren't formulae yet..

All the Godel coding hasn't been actually implemented.

Just shown/assumed to be doable.

Leaky Nun

@user21820 well, as I said, G(t,y) and F(x,t) is what you need

no coding needed

user21820

@LeakyNun Yes for this part. You haven't shown the formula for sub...

Leaky Nun

I don't care about the formula for sub

user21820

Lol why?

David Reed

4:09 AM

I have that one

if you want it

user21820

Hahahaha..

David Reed

was a bitch

Leaky Nun

@user21820 because I know it is doable

@DavidReed sure

user21820

@LeakyNun But then you should have known that composition is doable too, since composition of programs is also a program...

Leaky Nun

@user21820 but I imagine I can actually write it down

user21820

4:10 AM

No need to actually get hands dirty doing it.

Oh so you imagine it's short enough for you to dirty your hands?

Yah its not bad

Interesting.

@user21820 yes

I guess I'm at the lazy end of the logician spectrum.

David Reed

It just wasn't in the book so I had to figure it out myself. Was left as an excersize

user21820

4:11 AM

@DavidReed That book bad...

Leaky Nun

> That book bad

--- user21820

David Reed

you have to define an auxiliary function

I'm trying to remember what type of recursion this is called...

user21820

Primitive recursion.

David Reed

course-of-values recursion! that's it

user21820

Oh that.

David Reed

4:12 AM

Let me see if I can find it. It may be in my apartment in LA

user21820

Well the whole thing is primitive recursive, which is important if you want to get a Σ1-sentence over PA. Intriguingly it's trivial to get a Σ1-sentence over TC without worrying about primitive recursion.

Of course, LeakyNun said earlier that he doesn't care about the quantifier complexity...

David Reed

course-of-values is primitive recursion. Its kind of like the difference between single and multi-tape turing machines...there is no difference, but it makes life easier.

user21820

@DavidReed Yeap I know it's primitive recursive. I just didn't know you were looking for that specific term.

David Reed

Let me see if I can remember how i did it

Leaky Nun

> it makes life easier

David Reed

4:17 AM

so sub(s,c,d): the function that takes any occurrence of the number c in the sequence coded by s and replaces it with the number d

that's what you are after correct?

Leaky Nun

right

David Reed

ok, so you have to basically make a function sub(s,c,d,y) and then make sub(s,c,d):=sub(s,c,d,lh(s)) where lh(s) is the length of the sequence coded by s

I remember that much from the start

Gimme just a few min

did you do the proof that shows a piecewise function defined in terms of an exhaustive,mutually exclusive list of recursive relations is a recursive function

Ok. I need to know what coding scheme you are using for sequences of numbers

I use $(a_0,....a_{k-1})$ is coded by $2^k3^{a_0}5^{a_1}$ etc

Leaky Nun

4:34 AM

what's the difference between Godel number and Godel numeral?

David Reed

In terms of the language of the book I sent you?

Leaky Nun

yes

David Reed

So you have a formula A, let #(A) be the godel number for this formula, then godel numeral is the representation of #(A) in the system,...like s(s(s(....0))))

Leaky Nun

oh...

David Reed

the A with brackets at the top is then #(s(s(s(s...))))))

user21820

4:38 AM

@LeakyNun In other words, the Godel number is the actual natural number and the numeral is the corresponding term.

Leaky Nun

right

David Reed

The heart of this theorem lies in the fact that you are able to assign a number to each formula. Since the system is able to make statements about numbers, you've found a way for it to make statements about itself. That is the "behind the scenes" reasoning behind the diagonal lemma.

21820's halting approach effectively does the same thing.

@user21820 Can i get your first name. Typing 21820 is a little mechanically awkward in terms of being able to type.

user21820

@DavidReed Yes that's why I stated in my post that it's roughly equivalent to Godel's approach. Though strangely enough the zero-guessing problem is not equivalent to Rosser's trick. (At least I do not see a link.)

@DavidReed Typically typing @+u+2+Tab would give my username as the first choice. =D

As for my first name, well...

On the Internet, nobody knows you're a dog

"On the Internet, nobody knows you're a dog" is an adage about Internet anonymity which began as a cartoon caption by Peter Steiner and published by The New Yorker on July 5, 1993. The cartoon features two dogs: one sitting on a chair in front of a computer, speaking the caption to a second dog sitting on the floor listening to the first. As of 2011, the panel was the most reproduced cartoon from The New Yorker, and Steiner has earned over US$50,000 from its reprinting. == History == Peter Steiner, a cartoonist and contributor to The New Yorker since 1979, said the cartoon initially did not get...

David Reed

@user21820 yes seems to work, albeit no less awkward.

no worries

I respect your privacy, althought I would argue in a population of 7 billion, your first name doesn't really compromise your anonymity

user21820

4:53 AM

@DavidReed At least mine would. I would have to use a pseudonym to avoid that.

David Reed

I've actually taken it two steps further, albeit unintentionally

user21820

What do you mean? Your username is not your real name?

David Reed

no it is

automatically went through that way since I did the "sign up through facebook" option

user21820

So nobody can find you on facebook now?

David Reed

anybody can find me on facebook

user21820

4:55 AM

Unless they knew who to look for?

David Reed

that's my fb picture there as my avatar

user21820

Then what two steps are you referring to?

David Reed

step 1: provide authentic first name

step2 : provide authentic last name

user21820

How is that unintentional?

David Reed

Although some of the behavior with my confidential msgs somehow migrating to my computer and being plastered on chat have given me a moments pause regarding my decision to do that

user21820

4:58 AM

Hmm... have you run MBAM yet?

David Reed

It was unintentional in that I clicked sign up through facebook, and then it automatically migrated my full name and picture over from my profile.

user21820

If MBAM finds any malware, you're going to have to clean them out first before changing your important passwords.

@DavidReed Oh I see.

David Reed

I noticed the other day that my profile has been accessed about 130 times in six weeks, which also gave me some pause

user21820

The worrying part is that the message sent through this chat ends with "Sent from my Windows 10 phone".

So it is quite impossible that you accidentally copied it over or something.

Which is why I'm serious you should check your devices for malware.

It could be a bug in the malware that caused it (otherwise it would have remained a silent infection).

David Reed

Yah that's what I meant when I said "migrated to my computer" the only remotely plausible explanation is that it got sucked into chat through my phone somehow.

So.......... You read my post and didn't call me a heretic. Thank you for that

What were your thoughts on it

@LeakyNun did you still want the sub function?

Leaky Nun

5:07 AM

hmm, how long is it

David Reed

it's not long at all

Prereqs:

the function $\pi (n)$ that returns the nth prime number is recursive

the function that returns the exponent of the nth prime number is recursive

that's about it

Oh also definition by cases: a piecewise function that is defined in terms of a mutually exclusive, exhaustive list of recursive relations is a recursive function

ent(s,i) that returns the ith entry in the sequence coded by s as well

and that's it

user76284

Is this statement of Rice's theorem correct?

$\forall F \subseteq \mathcal{P}(\Sigma^*) \setminus \{\{\}, \text{RE}\} : \{M \mid \mathcal{L}(M) \in F\} \not\in \text{R}$, where $\Sigma$ is the alphabet, $\text{RE}$ is the set of recursively enumerable languages, $\text{R}$ is the set of recursive languages, and $\mathcal{L}(M)$ is the language recognized by a Turing machine $M$.

Leaky Nun

@DavidReed ok, thanks

David Reed

Computability stuff is more 221892's area than mine

I haven't looked at languages/grammars/complexity in nearly a decade

user21820

@DavidReed If you're referring to your private message, I don't comment on people's private conversations unless they want me to. But since you asked, I'm a strong supporter of free will as long as it does not conflict with morality and so I don't like it at all when people evaluate others or themselves based on what others think, rather than what they can justify to be good.

David Reed

5:18 AM

I didn't realize I had sent you a private msg

I just meant last night regarding uncountable languages

user21820

Lol I thought you meant the accidentally sucked over message.

Which I agree with.

David Reed

You expressed interest in discussing it. I'm curious what your response would be

user21820

Haha..

David Reed

oh I see

user21820

@DavidReed Yes it's a long story. It starts with noticing that a few things in ZFC do not seem philosophically justified.

David Reed

5:21 AM

No the second I posted it somebody was breathing down my neck. Finally later I get "I'm sorry if I came across as condescending, I'm just going to leave all these condescending things up for people that may know less about the topic"

user21820

Lol. I try to avoid posting too controversial stuff on Main. Even then, people downvote me for all sorts of useless reasons. For example they downvote my post on the incompleteness theorems for being too long.

David Reed

This is outside of ZFC for me, more inline with the construction of FOL. itself

user76284

Actually, I guess it should be $\forall F \subset \text{RE} : F \neq \{\} \rightarrow \{M \mid \mathcal{L}(M) \in F\} \not\in \text{R}$.

user21820

@user76284: Oh hello! What's that?

David Reed

but I was doing a hyperreal construction, and the author basically said, assume we have a symbol in our language for every real number...

user76284

5:24 AM

@user21820 I'm trying to get the correct formal statement of Rice's theorem.

user21820

@DavidReed But it's the same thing, because logic is always done in some meta-system MS, and modern logicians use ZFC for their MS.

That's why all the problems with ZFC will come along in modern logic. In other words, you are going to have to decide what MS you want before you can start doing logic.

David Reed

Yes I touched on that earlier while you were gone. That makes me cringe a bit as well.

user76284

@user21820 I thought logicians used weaker theories as their meta-theory?

user21820

@user76284: Oh sorry I didn't see your message just now; it came during a period of time I got disconnected from Chat SE...

David Reed

But I think its a fair question, is the space of all graphical symbols uncountable

user76284

5:28 AM

@DavidReed Wouldn't that require an infinite information capacity?

Violating the Bekenstein bound.

David Reed

@user76284 The frame of this discussion is how illogical profession logicians can be

Not familiar with the Bekenstein bound but it sounds like it supports my argument.

user21820

@user76284 I don't get what your version is saying. Here's mine: First we say that two programs have the same output behaviour iff on every input they either give the same output or they both do not halt. Next we say that P is a behavourial property (of programs) iff ( P(X)⇔P(Y) for every programs X,Y that have the same output behaviour ). Then for every behavioural property P and programs T,F such that P(T) and ¬P(F), there is no program that decides P.

David Reed

@user76284 Looking at it I don't think it applies here

I'm wondering if it's possible to assign a distinct symbol to each real number.

user76284

@user21820 $\Sigma$ is the alphabet, $\text{RE}$ is the set of recursively enumerable languages, $\text{R}$ is the set of recursive languages, and $\mathcal{L}(M)$ is the language recognized by a Turing machine $M$.

Yeah, you also have to add that P is non-trivial right?

@DavidReed What I meant is that assigning a distinct symbol to each real number is impossible, assuming each symbol cannot occupy an arbitrarily large region of space. At least that's what I think. I guess you would have to define what you mean by 'symbol'.

A similar idea was used by Turing to argue for his thesis (any computation is equivalent to unbounded memory manipulated by a finite-state controller).

David Reed

Oh ok, once I saw the term "energy" as being a constraint I delved off as I was trying to think of it in abstract terms and not the feasibility of it.

user21820

5:38 AM

@user76284 The existence of T,F gives that in my version. Your version looks wrong because your F is a set of set of strings... Do you understand my version?

user76284

F is a subset of RE, so it's a set of languages?

Let me take another look.

David Reed

Although I'm now tempted to adopt that being a good answer as the ultimate goal would be that these symbols be able to be placed on paper.

@user76284 Thank you!

user21820

@user76284: And the proof is trivial. Take P,T,F as given. If D decides P, let Q = ( x ↦ D( t ↦ x(x)(t) ) ? F : T ). Since D is a decider, Q(Q) must be equal to T or F. But ( t ↦ Q(Q)(t) ) has the same output behaviour as Q(Q), so immediately we get contradiction.

user76284

@DavidReed No problem

Yeah F is a subset of RE in my formula so it's a set of languages, not strings. I see what you meant with T and F now.

There is at least one program for which P holds and one for which P does not hold, am I correct?

user21820

@DavidReed It may be that there are uncountably many reals, and yet you can't make a symbol for every one of them.

@user76284 Yes.

By the way, my proof is different from most textbooks I've seen, but it's much cleaner in my opinion, and you can actually implement Q in any nice programming language like Javascript!

David Reed

5:43 AM

Yes, in the hyperreal context I was telling you about. "Assume for the moment that we have a symbol for every real number in our language...."

user21820

@DavidReed Technically it didn't assume.

user76284

Consider the following 'symbol' for $y \in \mathbb{R}$: Draw a $[-1,1]$ interval with a dot on the real number $x$ such that $\text{arctanh}(x) = y$. Of course it is physically impossible to construct such a symbol.

David Reed

No that's what I WAS asked to assume

user21820

Well it's working in ZFC, so since it already can construct the real numbers, it can use the real numbers as symbols in a new first-order theory.

Too bad that theory cannot be implemented on a computer.

David Reed

it can construct the real numbers, and symbolize a finite subset of them in any given statement proof.

user76284

5:45 AM

If physics is not relevant at all I suppose anything goes :P

user21820

Even if you throw away ZFC and go to a weaker meta-system (@user76284: Those who like weaker MS are usually in recursion theory, a subfield of logic) you will still be able to perform the same construction as your book.

As long as you can do real analysis.

David Reed

Also zfc is a finite language, I'm basically being asked to take the set of real numbers to be my language

and I'm not sure I by the approach he takes.

user21820

@DavidReed It does not symbolize a finite subset of them; it uses the reals as part of an alphabet for a first-order theory as viewed inside ZFC.

user76284

Maybe infinitary logic (en.wikipedia.org/wiki/Infinitary_logic) is relevant here? I believe you can construct infinitely long statements and proofs (in an abstract sense).

user21820

Not relevant.

In particular, if you have a problem with constructing a first-order theory using the reals as an alphabet, namely you are playing with finite strings over an uncountable alphabet, then you should already have a problem with the construction of the reals.

user76284

5:50 AM

A formula in infinitary logic can have an uncountable number of junctions and quantifications, no?

David Reed

I don't have a problem with constructing the reals from a finite language, I have problems in the area of proving things like independence, forcing, transfer theorem etc in the manner that is presented to me

user21820

@user76284 Depends on which infinitary logic, but it's not relevant to David's inquiry about first-order logic.

user76284

Oh, okay

user21820

@DavidReed The problem does not lie with the construction of the first-order theory with uncountable symbols.

It comes only with transfinite induction.

I can justify it, but it would be too long to fit into a chat message.

David Reed

I'm not after ZFC here at all

This particular instance is arising in proving Robinsons transfer theorem

user21820

5:53 AM

You don't get it.

You cannot even construct the ultraproduct without an ultrafilter on N, and you cannot get that without transfinite induction.

Are you familiar with the basics of ordinals and cardinals?

David Reed

This one works around the ultraproduct construction, which is a large reason I chose it

user21820

Then please specify your construction of the hyperreals that does not need an ultrafilter on N.

David Reed

@user21820 I'm starting to get the idea I'm rubbing you the wrong way. As mentioned I am heavily sedated, maybe I've been a little overexpressive in chat tonight. I think I'm going to table this discussion until I'm clearer headed and better restrained. Have a good night man

user21820

@DavidReed Sure. Though I see nothing wrong with your statements except that you haven't shown me a way to get hyperreals without transfinite induction, which I was certain was necessary. Indeed, I just did a search and found this post:

Never mind, it didn't give what I thought it did.

Anyway if you use the compactness theorem at any point for a first-order theory with an uncountable language, then you need transfinite induction on an ordinal of the same (uncountable) cardinality. So there is no escaping replacement.

@DavidReed: Anyway hope you will have had a good night's rest when you see this! =)

David Reed

6:42 AM

Got your msg

It uses an ultrafilter, does not use an ultraproduct

@user21820 It was more the "you don't get it....are you familiar with the basics of ordinals and cardinals' that gave me the idea your patience was wearing thin

@LeakyNun you awake bud? I'm typing this up for you and hoping it stays up long enough for you to read it before its torn down.

Transcript for

♦ $Mathematics$ Logic

Transcript for

♦ Logic

♦ $Mathematics$ Logic