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).

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

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?

where is the i consumed?
I think you mean i(x(x))

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

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.

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.

I see. will do.

@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))
I'm not very sure

@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.

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

2:21 AM
Me too! That's why I saved them, I deviated from the book

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

@user21820 could you verify my solution?
also, you ignored this:

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

1 hour ago, by Leaky Nun
@user21820 do you care about fast-growing hierarchy?

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

2:22 AM
oh, sorry

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.

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.

@user21820 yes

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

is that gamma_0? I forgot

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.

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

3:11 AM
@DavidReed But who wrote the paragraph?

Lol.
Was it for an essay?

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

That's crazy...

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

3:14 AM
52 mins ago, by Leaky Nun
@user21820 could you verify my solution?

@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...

@user21820 could you?

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.

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

@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. =)

3:19 AM
I think I'm losing my mind

@user21820 a virtue I lack :P
@DavidReed the virus became physical :O
and @DavidReed could you share with me your formulas?

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

@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.

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

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

3:22 AM
@DavidReed the y-combinator; aka the diagonalization operator
@user21820 how is that logical?

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

oh that's easy man
one sec

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

@user21820 I see

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

3:24 AM
@user21820 how long do I need to understand why goodstein function is f_epsilon_0?

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

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

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

@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?

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

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

@DavidReed that's extremely unrigorous :P

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

and how do I know that?

@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.

3:30 AM
@user21820 For example?

@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

right, 17.1 is what I'm looking for

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.

@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.

@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).

@user170039 Sure.

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

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

@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.
For example you may go through this article (although I must say that this is not the article about which I was talking earlier).

@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).

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

T or F: There are exceptions to every rule.

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

3:50 AM
one sec. I'll give you more context:

@DavidReed Very funny.
Do you know my answer to that quine of question?
6

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....

* refers to concatenation btw
lol
I came up with that one time when I was going through this

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

It's not necessarily contradictory though, its false.
if its true then its both true and false, if its false then its just false.

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

3:57 AM
lol

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.

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.

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

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

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))?

4:03 AM
Oh

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

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

yes, but how to represent the composition?

@user21820: I think that this was the article.

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.

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

thanks

@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...

@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

@user21820 was it that gigantic?

let me see.

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

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

what?

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

what you gave me was what I needed

ah ok

4:07 AM
@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.

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

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

I don't care about the formula for sub

Lol why?

I have that one
if you want it

4:09 AM
Hahahaha..

was a bitch

@user21820 because I know it is doable
@DavidReed sure

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

@user21820 but I imagine I can actually write it down

No need to actually get hands dirty doing it.
Oh so you imagine it's short enough for you to dirty your hands?

4:10 AM

Interesting.

@user21820 yes

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

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

4:11 AM
--- user21820

you have to define an auxiliary function
I'm trying to remember what type of recursion this is called...

Primitive recursion.

course-of-values recursion! that's it

Oh that.

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

4:13 AM
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.

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

Let me see if I can remember how i did it

> it makes life easier

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?

4:18 AM
right

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

4:34 AM
what's the difference between Godel number and Godel numeral?

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

yes

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))))

oh...

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

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

right

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
As for my first name, well...
"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... @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 4:53 AM @DavidReed At least mine would. I would have to use a pseudonym to avoid that. I've actually taken it two steps further, albeit unintentionally What do you mean? Your username is not your real name? no it is automatically went through that way since I did the "sign up through facebook" option So nobody can find you on facebook now? anybody can find me on facebook 4:55 AM Unless they knew who to look for? that's my fb picture there as my avatar Then what two steps are you referring to? step 1: provide authentic first name step2 : provide authentic last name How is that unintentional? 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 4:58 AM Hmm... have you run MBAM yet? 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. If MBAM finds any malware, you're going to have to clean them out first before changing your important passwords. @DavidReed Oh I see. I noticed the other day that my profile has been accessed about 130 times in six weeks, which also gave me some pause 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). 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? 5:07 AM hmm, how long is it 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 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$. @DavidReed ok, thanks Computability stuff is more 221892's area than mine I haven't looked at languages/grammars/complexity in nearly a decade @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. 5:18 AM I didn't realize I had sent you a private msg I just meant last night regarding uncountable languages Lol I thought you meant the accidentally sucked over message. Which I agree with. You expressed interest in discussing it. I'm curious what your response would be Haha.. oh I see @DavidReed Yes it's a long story. It starts with noticing that a few things in ZFC do not seem philosophically justified. 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" 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. This is outside of ZFC for me, more inline with the construction of FOL. itself 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}$. @user76284: Oh hello! What's that? but I was doing a hyperreal construction, and the author basically said, assume we have a symbol in our language for every real number... 5:24 AM @user21820 I'm trying to get the correct formal statement of Rice's theorem. @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. Yes I touched on that earlier while you were gone. That makes me cringe a bit as well. @user21820 I thought logicians used weaker theories as their meta-theory? @user76284: Oh sorry I didn't see your message just now; it came during a period of time I got disconnected from Chat SE... But I think its a fair question, is the space of all graphical symbols uncountable 5:28 AM @DavidReed Wouldn't that require an infinite information capacity? Violating the Bekenstein bound. @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. @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. @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. @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). 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. 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? F is a subset of RE, so it's a set of languages? Let me take another look. 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! @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 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? @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! 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...." @DavidReed Technically it didn't assume. 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.

No that's what I WAS asked to assume

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.

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

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

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.

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.

@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.

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).

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.

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

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

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

Oh, okay

@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.

I'm not after ZFC here at all
This particular instance is arising in proving Robinsons transfer theorem

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?

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

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

@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! =)

6:42 AM