@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).
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.
@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:
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.
@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.
@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.
@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...
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))
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.
@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.
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
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...
@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).
@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.
@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
@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).
@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).
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).
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))
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....
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.
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
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...
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.
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
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))))
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.
@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
"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...
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
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
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
$\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$.
@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.
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"
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.
@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.
@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.
@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).
@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: 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.
@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!
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.
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.
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).
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.
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 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
@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! =)
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.