(one of the ones I was part of said something like "these are all of them except in these few cases where there are some more. We don't know how many")

Question: Do Gödel's Incompleteness Theorem's account for potentially infinite lists of axioms?

If there's an algorithm that tells you whether a given statement is an axiom or not, you're good

If your set of axioms is "the set of all true statements about arithmetic in the language of PA" then Gödel doesn't apply

and also that's trivially complete

@Rithaniel

PA has infinitely many axioms anyway

The axiom of induction is actually a set of axioms

(axiom *schema of induction, technically, for that reason)

"If phi(0), and for all x phi(x) implies phi(x+1), then for all x phi(x)"

^Repeat that for all statements phi expressible in the language of PA

Well, my thought is this: Suppose that, for every statement, there is a set of axioms which can decide that statement. Then could you collect together a list of all these axioms such that every statement is decidable? It might be an infinite list of axioms, but supposedly it would be complete. This seems to imply that there exist statements that no set of axioms could ever decide.

(Note that if any statement about the integers is not expressible in the language of PA, then there's no induction axiom for it)

(which is why nonstandard models of PA can exist)

(Otherwise we could induct on phi(x):="x is a standard number")

PA stands for?

Peano Arithmetic

A set of axioms describing how arithmetic works

The standard model of PA is $\Bbb N$

(including zero)

It uses $S(x)$ to mean "the successor of $x$" (aka $x+1$), so one of the axioms is $\forall x,0\ne S(x)$

There's also $\forall x,y,x+S(y)=S(x+y)$

There's a list on Wikipedia

Alright, that gives me something to read up on.

It's a neat exercise to show that $\forall x,y,x+y=y+x$ from the axioms. You need induction for it

(Instead of proving 2+2=4, you would prove S(S(0))+S(S(0))=S(S(S(S(0)))), since 2 and 4 aren't in the "alphabet" of symbols allowed)

(You also need the axiom $\forall x,x+0=x$ to do that)

Strange thought: the group axioms are incomplete

You can't prove or disprove $\forall a,\forall b,ab=ba$ from the axioms

Clearly the reason for this is because it's true in some "models" of the group axioms (aka "groups") and false in others

Hmmm, I clearly need to take a course on set and model theory, because that kind of blew my mind.

@AkivaWeinberger That's not strange, groups would be very rigid if they all satisfied the same first-order properties

Speaking of first-order properties

@Rithaniel Consider the ordered set $(\Bbb Q,<)$

What are some true statements you can make in that system?

$\forall x\exists y,x<y$ (there is no highest rational)

$\forall x\forall y\exists z,x<z<y$ (the rationals are dense)

etc

The only symbols we can use are logical symbols, $=$, and $<$

Well, how about $\frac{x}{y+1}<\frac{x}{y}<\frac{x+1}{y}$?

We don't have division

or arithmetic

Just $<$

We can also say something like $\forall x\forall y\forall z,x<y\land y<z\implies x<z$

and $\forall x,\lnot(x<x)$

Is there any statement we can make about $(\Bbb Q,<)$ that's not true of $(\Bbb Z,<)$? @Rithaniel

Absolutely, you already gave one.

What about a statement about $(\Bbb Q,<)$ that's not true of $(\Bbb Q,\ne)$?

You also gave one of those.

$\neq$ is not transitive.

What about a statement about $(\Bbb Q,<)$ that's not true of $(\Bbb R,<)$?

That one is a bit more tricky. I actually want to say there are none because the reals necessarily contain the rationals.

So, if it's true about the rationals, then it's true for a dense subset of the reals.

You know, I don't think I actually have a proof

but I'm pretty sure that this is true of all dense linear orders without endpoints

They're indistinguishable

Simplified systems are not where my mind is at the moment.

The point is, there's no axiom system that can uniquely describe $(\Bbb Q,<)$

I think there's a theorem in model theory that says, if a theory has an infinite model, it has a model of any infinite cardinality

("Theory" = "collection of axioms")

(wait no I don't think that's the right definition)

https://en.wikipedia.org/wiki/Theory_(mathematical_logic)

"Theory" = "collection of statements"

"including but not limited to the axioms"

@AkivaWeinberger Löwenheim-Skolem

@AkivaWeinberger It's a complete theory

@Rithaniel So

Consider the structure $(\Bbb N,S,0,+,\cdot)$

($S$ is the "successor" operation: $S(x):=x+1$)

One would hope that there's a set of axioms that defines that structure uniquely

and that's what PA tries to do

but in fact, because of Gödel, there will always be other models

and there will be statements that are true for $(\Bbb N,\dots)$ that are false for those models

The easy way to show that $\mathsf{DLO}_-$ is complete is to show that is $\aleph_0$-categorical I think

@AlessandroCodenotti isn't that models, not axioms?

@Rithaniel In fact, I can prove part of that right now

Lowenheim-Skolem, that is.

@anakhro What do you mean?

I thought that you were responding to "there's no axiom system that can uniquely describe $(\Bbb Q,<)$".

But maybe I misjudged.

No, click on the arrow

@Rithaniel I can prove that there's a structure $(M,S,0,+,\cdot)$ that's not isomorphic to $(\Bbb N,S,0,+,\cdot)$ but such that any statement true about one is true about the other

Oh this fancy arrow function I always overlook

Oh

OH

@anakhro Well I mean that's also a consequence of LS if you want

What's the model-theoretic lingo for "indistinguishable in terms of first-order statements"

I'm sure there's a word

Don't models model axioms, not are axiomatic systems themselves?

@AkivaWeinberger define the same 1-type?

That is quite intriguing. What does the outline of the proof look like?

@anakhro I'm not sure what you mean with axiomatic system

@AkivaWeinberger Oh wait are you talking about elements of a structure or structures of the same language?

Well that's why I am myself a little confused.

About the statement "there's no axiom system that can uniquely describe $(\Bbb Q,<)$".

In the first case they define the same type, in the latter the structures are called elementary equivalent

It just means a set of axioms I assumed

@Rithaniel Let's say I add something to our language

a constant, $c$

So then what is $(\Bbb Q,<)$?

So now we have $(\Bbb N,S,0,+,\cdot,c)$

Hm wait

No I don't want a model just yet

$(S,0,+,\cdot,c)$

That's our language^

S is a unary function, + and x are binary functions, 0 and c are constants ("0-ary functions")

and let's make a set of axioms

the axioms are: any statement that's true in $\Bbb N$, plus the statement $c>0$

This has a model, right?

@anakhro A structure in the language $\{<\}$ (which is also a model of $\mathsf{DLO}_-$)

Make the symbol $S$ mean the successor function, make the symbols $0$, $+$, and $\cdot$ mean the integer zero and the operations addition and multiplication, and make $c$ any integer bigger than 0

(Be careful to distinguish between the symbol $0$ in our language and the number $0$ in our model)

@Rithaniel Make sense so far?

And because these axioms have a model, they're consistent

So, this "$\mathbb{N}+c$" is just $\mathbb{N}$ with a single number relabeled to $c$?

Yep

Now let's add lots of new axioms

Our new axioms are: all statements that are true about $\Bbb N$, and the following infinite list of axioms

$c>0$, $c>1$, $c>2$, $c>3$, …

I want to convince you that this set of axioms is consistent

@AlessandroCodenotti what does DLO stand for?

Note first that it's not obvious what a model of this could be

Okay, so $c$ is analogous to the first infinite ordinal?

@anakhro Dense linear orders (and the subscript $-$ means without endpoints)

So far, $c$ is just a symbol.

We don't yet have a model, so it doesn't represent anything yet.

But also: any finite subset of these axioms has a model

So what makes there be multiple axiom systems?

An axiom system is just a theory

@Rithaniel Why does any finite subset of this set of axioms have a model?

Well an axiom system could be an axiomatization of a theory I guess if we want to be picky?

Because it's the model for $\mathbb{N}$ which was already given. (Not being super thorough at the moment because I am tired.)

What would $c$ be?

If we only had finitely many of those axioms

Aren't the DNO_-'s characterized by axioms themselves

DLO is a list of sentences: the axioms

(By the way: when I wrote $c>1$, I really meant $c>S(0)$

because $1$ isn't in our language

That's the part I was not being thorough on. It would be one of the integers which are greater than all the integers listed in your "bonus axioms"

(people might have different opinions here, some would say that DLO is a collection of sentences: the axioms and everything that follows from them)

so it's really $c>0$, $c>S(0)$, $c>S(S(0))$, etc)

@Rithaniel Yeah. Take the largest $n$ where $c>n$ is ak axioms and make $c$ anything bigger

@AlessandroCodenotti so are they uniquely characterized?

So now I said that I would show that the full (infinite) list of axioms is consistent

The reason is this:

all proofs have finite length

Sure, but what Akiva was saying is that if you have a theory in the language $\{<\}$ that has $(\Bbb Q,<)$ as a model, then it also has other models

(Note that I said "consistent", not "complete")

$(\Bbb Q,<)$ is the thing that can't be characterized in this language

(just to avoid confusion 'cause those words look similar)

@AlessandroCodenotti okay, so I was thinking O.K. that it was supposed to be a comment about models.

An axioms system is inconsistent iff you can prove both $A$ and $\lnot A$ from the axioms

@anakhro Oh, yes, sorry for the confusion

But any proof has finite length, which means any proof will only use finitely many of the axioms

No worries. I was intrigued for the time being. :P

Since all finite subsets of the axioms have a model, all finite subsets of the axioms are consistent

therefore, since any proof uses finitely many of the axioms, it cannot prove $A$ and $\lnot A$

(Subtle point: $\forall x,c>x$ is not an axiom)

@Rithaniel Does it make sense so far?

'Cause now I need to invoke Gödel's completeness theorem

which says that any consistent set of axioms has a model

Now I can talk about what this model looks like

So, what about proof by induction?

?

Isn't that a method of proof which is technically infinite in length?

No

We can always write down a proof by induction using finitely many symbols

No, you have an axiom saying $(\phi(0)\land\forall x(\phi(x)\rightarrow\phi(S(x))))\rightarrow(\forall x\phi(x))$

You're showing that the hypothesis of the $\rightarrow$ hold, which uses finitely many steps

Yeah. Whatever $\phi$ is, if you prove $\phi(0)$, and you prove $\forall x(\phi(x)\implies\phi(S(x))$, then you can invoke the axiom of induction and conclude $\forall x\phi(x)$

We've only invoked finitely many axioms: whatever it took to prove $\phi(0)$, plus whatever it took to prove $\forall x(\phi(x)\Rightarrow\phi(S(x))$, plus one (the induction axiom)

and our proof is of finite length as well because its length is just the length of the first two things plus one, also

So in the end we have a model (let's call it $M$) such that

any statement you can write in $(S,0,+,\cdot)$ that's true in $\Bbb N$ is true in $M$

but also we can view $\Bbb N$ as a proper subset of $M$

and there's an element of $M$ which is larger than any element of $\Bbb N$.

Well, I'm currently hung up on the notion that a proof has to necessarily have finite length. What is stopping us from using finite symbols to represent an infinite number of steps?

which we call $c$.

@Rithaniel A "proof" is essentially a list of sentences

@Rithaniel that sounds like something in the realm of transfinite induction (though I know nil about it)

each one with a derivation from the prior sentences and the axioms

We want our notion of "proof" to be so rigid, we could enter it into a computer and the computer could tell us if our proof is correct.

That's the level of rigor we're at right now.

The rules of logic are essentially just rules that tell the computer what manipulations of the symbols are allowed.

The computer doesn't know what the symbols "represent".

Only the mathematician, who has created a "model", has any idea what the symbols should represent

If the proof were infinitely long, we could never finish inputting it into the computer.

As an analogy: Suppose I write a complicated program, and then realize that I want to reuse a certain part of that code. Ok, I build a separate function that’ll perform that operation, and I just have the original program call said function.

Keep in mind that I am quite tired at the moment, but I'm still not 100% convinced. You've allowed that you can define a structure with infinitely many statements but that a proof directed towards a statement about that structure cannot use infinitely many statements.

And also that any finite subset of those statements is consistent

and I've concluded that that means the whole set of statements must be consistent

("consistent" meaning "we can't prove a contradiction")

Have I simplified the program? Well, at one level the answer is clearly yes: my program includes fewer lines and is easier for me to understand what’s going on

After that, I invoked Gödel's completeness theorem, which says that if a theory is consistent, is has a model

But nevertheless the actual amount of work for the computer must do has certainly not decreased. The computer still has to execute the function after all

By the way, the statement $\forall x\exists y:(y+y=x)\lor(y+y+1=x)$ is true in $\Bbb N$

I've basically just described $\forall x\exists y:y=\lfloor x/2\rfloor$ in a complicated way

So as convenient as it is to black-box that part of the program when understanding its purpose, I clearly can’t neglect that if I want to know whether said program will ever finish computing!

So now let $x$ be $c\in M$

This essentially means that there's an element of $M$ that deserves to be called $\lfloor c/2\rfloor$

Fair, so to truly truncate infinitely many steps I need something like the axiom of induction?

Yeah

I don't know how to describe $M$ explicitly, except to say $\{0,1,2,3,\dots,c-2,c-1,c,c+1,c+2,\dots\}$

but that description doesn't mention $\lfloor c/2\rfloor$

so maybe I should say $\{0,1,2,\dots,\lfloor c/2\rfloor-1,\lfloor c/2\rfloor,\lfloor c/2\rfloor+1,\dots,c-1,c,c+1,\dots\}$

but for similar reasons, $\lfloor\sqrt c\rfloor$ also exists

You presumably could consider theories of logic (not sure that’s the best word) in which certain hard algorithms (e.g., those which require infinite steps) are taken to require finite resources, and explore the consequences of that

and $\lfloor c\sqrt2\rfloor$ exists (why?)

That seems roughly analogous to how complexity classes work in comp sci

(because $\forall x\exists y:y^2\le 2c^2<(y+1)^2$)

(technically $<$ isn't part of our language)

($x<y$ is a shorthand for $\exists a:y=a+x+1$)

Well, I'm still caught on the fact that infinite axioms are used to define an object but you aren't allowed to use infinite statements to talk about the object. Also, just because something is true about all finite subsets of an infinite set doesn't mean that it's true about the entire set. Just because they're all consistent doesn't mean the full collection is consistent.

(or I suppose $\exists a:y=S(a+x)$, really)

@Rithaniel We can use all statements to talk about it. Just, no single proof can.

There are proofs that use 5 of the axioms, and proofs that use 50 of the axioms, and proofs that use 500 of the axioms

Every axiom will be used by some proof

Just, no proof will use all axioms

Yes, I follow that part.

Let's say we wanted to find a contradiction in these axioms

Let's say we wanted to find an inconsistency

Maybe we should start by proving $\lnot(\forall n:c>n)$

That's not too hard. $\forall x,\lnot(\forall y:x>y)$ is true in $\Bbb N$, so it's one of our axioms by definition

Now, letting $x=c$, we conclude $\lnot(\forall n:c>n)$.

So now what?

Maybe rewrite it as $\exists n:\lnot(c>n)$

There's some $n$ that $c$ isn't larger than

OK well we also know that $c>0$. Yeah?

That rule, that no single proof can be infinitely long, seems arbitrary. It is a logical thing that we can't reference every axiom by name, but I also didn't write out infinitely many axioms when defining my object.

Try to get a contradiction though

I mean, $\exists n:n\ne0\land n\ne1\land n\ne2\land\dotsb$ looks like a contradiction

but we can't have infinitely long statements, and even if we could, why would that make a contradiction?

It would only make a contradiction if we could also prove its negation

Its negation is, $\forall n:n=0\lor n=1\lor n=2\lor\dotsb$

but who said that's true?

Now, I'm okay with accepting that.

With accepting that $\forall n:n=0\lor n=1\lor n=2\lor\dotsb$ can be false?

I said that all statements in our language that are true in $\Bbb N$ will be in our set of axioms. I guess I should've specified, only statements of finite length

I really should've distinguished between the symbol $\forall$ and the logical quantifier $\forall$

The former is just a symbol, and it can be manipulated by rules, and a computer can learn those rules and perform those manipulations

The latter means "for all"

Our proofs are made of symbols

So, the notion is that the definition of natural numbers is inherently nebulous and can potentially have a region which is poorly defined?

Any possible first-order definition of the natural numbers ("first-order" meaning it's made out of symbols like this) will describe things that are not the natural numbers

Sorry, chat didn't scroll for a moment.

Even if the computer had access to a magic oracle that told it if any random statement was true or false in $\Bbb N$, there could be a mathematician standing next to you who says, those symbols on the screen don't really refer to natural numbers, they refer to elements of a completely different, larger, set

Now Gödel's incompleteness theorem tells us something slightly different

I'm okay with accepting that comparing infinitely many statements with infinitely many statements can potentially fail to ever arrive at a decision, even "after" all infinite statements have been checked.

Take away the oracle: the computer now only has access to a limited number of axioms (the first eight axioms of PA plus the "axiom schema" of induction)

and it's deducing as many statements as it can from the axioms, algorithmically

Basically the least efficient proof software imaginable

Trying to see if a statement $A$ is true or false by trying all possible logical deductions to see if it eventually arrives at $A$ or $\lnot A$

Gödel tells us two things, Turing tells us another thing

One: there are statements $A$ such that the computer will never arrive at $A$ and $\lnot A$

(They're independent)

Two: there could be a mathematician next to you who says that the symbols on the computer don't refer to $\Bbb N$, they refer to some other set, $M$. Not only that, but if $A$ is independent but true in $\Bbb N$, then there's some model $M$ in which $A$ is false.

@AkivaWeinberger what logic did I miss?

It's like the statement $\forall a,\forall b,ab=ba$ from the group theory axioms

There are models where it's true, and models where it's false

Now, Turing wanted to solve the "decision problem"

Basically: can we improve this algorithm?

Clearly if $A$ is independent then we can't decide one way or another from the axioms (regardless of if it's actually true or not in $\Bbb N$)

But maybe, there could be an algorithm that at least tells us if $A$ is true, false, or independent

hullo dudes

death note is op

Turing discovered that that's impossible

He also had to define what an "algorithm" is

how many of you watched death note ?

'cause that wasn't really done yet

(probably because no one needed a definition for it before)

(but if you want to prove that no algorithm exists to do something, you need a definition)

@cdt I did

I think Balarka did also

it's cool right ?

but i didn't like the ending

after l died

Oh also I lied

eh ?

It's not called the decision problem @Rithaniel

It's called the Entscheidungsproblem

My sleepy mind sees the words "ent" and "dung" in that word

Oh also Alonzo Church independently proved it was impossible the same year Turing did

He had a different definition of algorithm

but it turned out they're equivalent

@Rithaniel Ent = de

scheidung = cision

s = ?

problem = problem

I don't know German

and I'm 80% sure what I said makes no sense

but I'm 20% sure what I said does

@ÍgjøgnumMeg Can you confirm^

Confirmed

"Entdeckung" is literally "Un-covering" for another example

which is "Discovery"

the "s" has a specific name

but it comes from the genitive case I guess

It's strange, the difference between "discover" and "uncover"

'cause from the parts that make them up, it seems like they should be the same

As it stands they're pretty similar

@Rithaniel dungs problem

@cdt yeah after l died it was meh

Right OK

so that was a long lecture on logic and model theory

by someone not entirely qualified to teach either logic or model theory

death note is cool but overhyped

i like the idea

didn't feel as invested as other anime i have watched (and i have watched very few animes tbh)

Does Avatar count

ducks

spongebob best anime

A book about ancient Scottish peoples

"Picts or it Didn't Happen"

lol

I'm very willing to believe that the Picts' only language was Pictionary

It took me a while to realize what the arrows were doing

It should be a GIF

Weird game idea

Using a weird "perception is reality", "apparent size vs real size" mechanic that allows you to resize objects

@Secret I think you'd find that trailer interesting

$-2-\tau < - \sqrt{(\tau)^2 - 4\delta} < 2 - \tau$ imples $1+\tau + \delta > 0$ ?

after squaring the first inequality

Any idea, m not gettig how

dynamical resource allocation problems anyone?

@BalarkaSen someone asked Fernando Marques what adding chains means

I don't know what that means either lol

@Ultradark (flat) chains are defined to be (formal) sums of polyhedra

The problem is not Trump, the problem is what created the environment encouraging the people to elect Trump

what does Trump have to do with this

@RyanUnger nevermind just a random thing

Hey everyone!

any number theorists abound?

How do i put bunty on a question?

Hey @Perturbative, @Sandhi ask your number theory question and if someone knows how to help you they will

bounty

@Sandhi did you just post the question? Because you have to wait $2$ days before being able to put a bounty on a question

aha okay

but you can post it here if you want

It is a pretty big post and the questions are embedded in it.. If you are interested do take a look

Why are you saying "we posted a question" Did you collaborate with someone?

that's a long question

We = Me..The issue is that I refer to the original author who lived about 1000 years ago and did not get due recognition I feel.. So I write we.. :-)..

and it feels odd to write 'I'

because all the papers I came across, I have never seen anyone use 'I'

@RyanUnger It is more of a methodology with questions embedded in bold

Neat interactive essay

https://meltingasphalt.com/interactive/going-critical/

All of you should put that in a new tab so you can play it later

Or play it now

that's very neat, I'm reading through it

hot cats

anyone have any knowledge on T-nets?

only tensors I know are the $v_{ijkl\mu\rho\sigma}^{\epsilon\pi xyz}$ kind

@RyanUnger probably it’s more properly “tensor product network”

Though that’s about where my knowledge ends

The intro here seems decent: windowsontheory.org/2018/12/20/…

@RyanUnger how did he respond lol

The mobile version of this chat is so crap

@Ryan how is the thing

@AkivaWeinberger It's technically not new (see video below), but it seems this game makes that mechanic more smoothly into the puzzle solving environment. In practice, that resizing is done by some kind of portals and perspective projection, but it will be interesting to see how to use mathematics to model the underlying non euclidean space as a seamless whole