Logic - 2017-11-30

Leaky Nun

01:03

somehow I managed to prove succ_inj

Leaky Nun

02:16

github.com/kckennylau/Lean/blob/master/ordinal.lean

axioms and theorems

user21820

04:49

@LeakyNun Yes we can't, and that's the ideal case unless we don't believe there is a model of PA.

We do have empirical evidence that PA has a very good approximate real-world interpretation, and so conceptually it seems that ACA is not only consistent but sound. It gets hairy beyond that, because it is not so clear how quantifying over subsets of N should be interpreted.

@LeakyNun What proof assistant is that?

user21820

05:14

@LeakyNun For classical systems, Godel's sentence is equivalent to Q' in my post.

Godel's+Rosser's Incompleteness Theorems and simple computability proofs here!

13

Good introductory texts for logic here!

13

@LeakyNun: If you star the above, it won't fall down the pinboard so quickly. =)

Note that if you look carefully at the proof that Q' is independent, you will see that it relies on soundness for program halting only to show that the system does not prove Q. That assumption is not needed to ascertain the truth value of Q'. Hence in the later section I stated the relation between Q' and consistency for classical systems without mentioning soundness for program halting.

Leaky Nun

07:59

@user21820 lean

@user21820 should I take this as a yes?

user21820

@LeakyNun Take what as a yes? I didn't say whether the answer to your question is "yes" or "no", because it depends.

Leaky Nun

on what?

user21820

Um my post shows exactly when Q' is true. Godel's sentence turns out to be equivalent to Q'.

It also turns out that Godel's sentence G for a classical system S is provably equivalent to Con(S), meaning that S |− G⇔Con(S).

The reasoning in my post is the same as the reasoning in standard textbooks needed to show that S is consistent iff N |= Con(S).

Leaky Nun

08:14

N?

user21820

Natural numbers.

Well I shouldn't say "same", because it's much clearer using programs than wading through representability of recursive sets in PA.

That's why I say you need to read it to understand the incompleteness stuff, unless you want to try the standard route. Godel basically constructed Q' but expressed in arithmetic.

He first encoded a program interpreter in arithmetic and then encoded the formal system as a program and then constructed a formula corresponding to provability and then diagonalized in the same manner as C against H.

Because of using arithmetic, there are some technical issues as well, so the underlying idea is thoroughly obscured.

I think Godel didn't find the clean way because he came before Turing.

MatheinBoulomenos

13:45

@user21820 okay, now I think I understood it, thanks

user21820

@MatheinBoulomenos: Hello! Great! Any other questions?

MatheinBoulomenos

But I think I'd still do case-splitting to show that the constructed set is linearly independent

I think the Peano axioms I learned as a freshman are not first-order

the induction axiom is quantifying over predicates

But isn't peano arithmetic really important? I thought that most theorems only work for first-order theories

user21820

@MatheinBoulomenos Why is there any case splitting? Unless I'm mistaken, it should be quite trivial.

Let me quote my proof sketch:

2 days ago, by user21820

We can take the simplest example of the existence of a basis of any given vector space V. By transfinite induction V can be well-ordered. Initialize S = {}, then enumerate the vectors in V in that order and at each stage add the current vector v to S iff S⋃{v} is linearly independent. At the end, clearly every vector in V is in span(S), and we just have to check that S is linearly independent, which you should be able to prove.

If S is not linearly independent, then there is a finite non-trivial linear combination of vectors in S that sums to the zero vector in V. Thus one of those vectors was added to S after all the rest (because finitely many of them). That one would not be added because at that point it is in the span of the previously added vectors.

Therefore S is linearly independent.

MatheinBoulomenos

Oh right

I somehow was confused because I thought that you had to use that ascending unions of linearly independent sets are linearly independent

but the induction axiom is a second-order axiom, right?

user21820

That's why I said earlier that I think any non-set-theoretic use of transfinite induction should not have to split cases between the successor and limit stages, and should not even have to care about ordinals. Otherwise it's very likely that the proof has taken an unnecessary detour.

@MatheinBoulomenos The induction axiom you may have been taught may not be the right one.

There is second-order induction, namely any set that has 0 and is closed under successors contains the natural numbers.

MatheinBoulomenos

13:58

yes, that what I was taught under the name "Peano axioms"

user21820

The problem with that is that it is simply useless, unless you also have set construction axioms. In particular, it seems that Peano's axioms have exactly this flaw; they were never sufficient to begin with.

MatheinBoulomenos

makes sense

So what's the "right" induction axiom?

user21820

The correct induction is an axiom schema (list), not a single axiom. This is why nowadays PA refers to this first-order system and not Peano's original. You have one axiom for each predicate over the language of arithmetic.

MatheinBoulomenos

Ah, this seems more reasonable

user21820

I use "predicate" not to mean "set" but "1-parameter sentence".

So you will have induction only for countably many predicates.

MatheinBoulomenos

14:01

But wait

Doesn't Löwenheim-Skolem imply that there are uncountable models of PA?

This is really weird

user21820

@MatheinBoulomenos It does, but why is it weird?

MatheinBoulomenos

intuitively, natural numbers should be countable

and PA should axiomatize natural numbers

user21820

You only get to control predicates that you can write down in the language of arithmetic.

MatheinBoulomenos

Okay, I still think it's weird

user21820

@MatheinBoulomenos: You will probably be interested in the following posts:

14

A: How do we know what natural numbers are?

How do the mathematicians that write standard natural numbers have formal consensus on what they are talking about? Mathematicians work in a meta-system (which is usually ZFC unless otherwise stated). ZFC has a collection of natural numbers that is automagically provided for by the axiom of ...

9

A: What are the arguments for and against "one true arithmetic"?

In short: The so-called definition of natural numbers as those that can be obtained from 0 by adding 1 repeatedly is circular, but there is no viable alternative, which already makes it impossible to uniquely pin down natural numbers mathematically. Worse still, there does not seem to be ontologi...

MatheinBoulomenos

14:06

Does a model of a theory have to be set or can it be proper class?

user21820

(which is another one having overlapping content but slightly different focus)

@MatheinBoulomenos In ZFC, a model is defined as a set that ...

MatheinBoulomenos

So the class of all sets in ZFC is itself not a model of ZFC?

user21820

It can't be constructed in ZFC, so you can't say anything about it.

However, it is possible to talk in MK set theory about class models.

MatheinBoulomenos

But are there models of ZFC that are a set?

I think you probably just need some really large cardinal for that

user21820

That question is equivalent to asking whether ZFC is consistent, by the semantic-completeness theorem.

It does not need large cardinals.

MatheinBoulomenos

14:09

Oh right, so it's undecidable if ZFC is consistent

by the second incompleteness theorem

user21820

Right, but we need to go outside and use the first incompleteness theorem.

Not the second.

Otherwise we are stuck one level deeper.

And regardless of incompleteness, within ZFC you can prove that if ZFC is consistent then ZFC has even a countable model (by Henkin construction).

MatheinBoulomenos

But wouldn't a model of ZFC inside ZFC mean that ZFC can prove its own consistency?

countable model of ZFC sounds weird

user21820

If ZFC is consistent then ZFC has a countable model.

ZFC never proved that it has a model.

Do you get it? You need to be careful of which system you are working in. Suppose we work in a relatively simple meta-system MS that only knows the basic properties of strings and natural numbers and programs, and can define the halting problem and define sets based on the solution to the halting problem.

You can think of this as MS being able to construct programs that can call an oracle that gives the answer to the halting problem for any program and input.

MatheinBoulomenos

Yeah, I get that I have to be careful

user21820

Then MS is strong enough to prove that every consistent first-order theory S has a countable model.

Note that the notion of consistency already requires the halting problem to be well-defined.

So that you can talk about whether there is a proof of contradiction or not.

Incidentally, I explained the fact that I just claimed to LeakyNun not long ago, starting here:

Nov 18 at 4:57, by user21820

@LeakyNun: I'll elaborate on my point that we can in fact perform that process using the first Turing jump H(1), also known as the halting oracle. There are many programs using H(1) that are proof verifiers for a complete consistent extension of any consistent formal system. You just use any computable enumeration of all sentences, and at each step you use H(1) to find out whether that current sentence is consistent with the previous ones and if so then add it but otherwise add its negation.

NL: To be really precise, I sometimes label everything I say with the system I'm talking in, such as NL for natural language.

MS: ZFC is consistent implies ZFC has a model.

MatheinBoulomenos

14:27

@user21820 given a group $G$, would you define the transfinite derived series of $G$ without case splitting as well?

I'd just say for a succesor ordinal, we take the commutator subgroup and for limit ordinals we take an intersection

but maybe that's clumsy as well

user21820

@MatheinBoulomenos I am not actually familiar with the derived series, but it appears that at each stage you can simply take the commutator subgroup of the intersection of the preceding groups. Like with the vector space basis construction, this creates a monotonic sequence, so it will work out.

In algorithmic terms, at each stage you shrink the group to its commutator subgroup. At limit stages, the earlier shrinking steps would have ended up producing the intersection already, and in the original definition you stop there while in my definition you would take the commutator subgroup again.

MatheinBoulomenos

14:43

your definition seems to be slightly different, but I don't think the difference matters

user21820

Yea I think so too.

Because the goal is just to get down to a 'fixed-point' of the commutator subgroup operation.

@MatheinBoulomenos: You may also be interested in the difference between the first-order and second-order axiomatizations of the reals:

22

A: Is the real number structure unique?

To paint a more complete picture, you are right in that an axiomatization may very well have no model. An axiomatization is meaningless if nothing satisfies it. But if we can prove that there is a model, and the axioms are the only properties we care about, then we can happily work within the axi...

MatheinBoulomenos

is it always true that second-order axioms are meaningless without set theory?

user21820

@MatheinBoulomenos I wouldn't say that, since there are type theories.

However, what I said earlier is that second-order axioms only make sense if you have rules permitting you to construct those second-order objects.

MatheinBoulomenos

14:58

Ah, okay, so we need a more powerful metatheory

actually, a more expressible metalanguage

user21820

Sort of.

Leaky Nun

how many models does second order PA have?

user21820

@LeakyNun In what meta-system?

Leaky Nun

eh... you decide?

user21820

In most (such as anything at least as strong as ACA) there is one up to isomorphism.

Leaky Nun

15:06

then isn't it complete?

user21820

Uh? Think very carefully where the argument fails...

Leaky Nun

I see, completeness fails

user21820

Yes compactness and semantic-completeness hold for first-order logic, not for full second-order logic.

Leaky Nun

could you give me examples where completeness fail?

user21820

15:27

Sorry I must amend my claim.

Compactness here means ( finitely satisfiable implies satisfiable ).

It is still true that for second-order logic we have ( finitely consistent implies consistent ).

@LeakyNun Just extend second-order PA by a constant c and add axioms stating that c is greater than each standard numeral. Then the resulting theory is finitely satisfiable, but has no model in full second-order semantics.

Leaky Nun

do you have more examples?

also, how do we know that there is no model?

user21820

Because we already proved (we are in MS remember?) that there is only one model of PA and it doesn't have any element that is greater than each standard numeral...

Leaky Nun

alright

user21820

As for more examples...

@LeakyNun Take the language of graphs with the edge relation and the second order theory of connected graphs, which can be axiomatized by simply ( every connection-maximal set contains everything ).

Just to finish the earlier example, since there is no model of the extended theory in full second-order semantics, it fails completeness because there is no proof of a contradiction (since it is actually consistent).

To continue the example of the theory of connected graphs, we can do the same trick, I think.

Leaky Nun

15:45

i.e. there is no 1-path from A to B, there is no 2-path from A to B, etc.?

user21820

Yea.

Leaky Nun

do you have a more "real-life" example?

user21820

Lol you're asking about compactness man! That's not real-life...

Leaky Nun

oh, the real-life interpretation is that you can either prove something or construct a counter-example

user21820

Then these examples fit the bill. I have explicitly described two second-order theories in which you cannot prove something that is true about all models (because there are no full semantics models).

Or you want some theory that actually has models?

So demanding! =P

Leaky Nun

15:55

@user21820 but those aren’t “real-life” examples

those are sentences which nobody cares about

MatheinBoulomenos

Asking for real-life examples in mathematical logic, lol

Leaky Nun

@MatheinBoulomenos well we have groups and rings and fields

and graphs and arithmetic and set theory

MatheinBoulomenos

these are first-order

Leaky Nun

I mean, these are real-life examples

user21820

@MatheinBoulomenos @LeakyNun: Okay okay I satisfy you both at one go. Let PA2 be PA plus the second-order induction axiom. PA2 has essentially one full-semantics model, but PA2 does not prove Con(PA), since PA2 is conservative over PA. This is trivial to see because PA2 cannot use the induction axiom since it has no set-construction axioms! But of course every model isomorphic to N satisfies Con(PA).

Happy now? =D

I changed PA− to PA but it actually doesn't make a difference to the resulting theory. Just easier to justify my claims later.

user21820

16:21

Hey where did you two go? I'm going off now. See you!

MatheinBoulomenos

See you!

Leaky Nun

"real-life"

user21820

16:36

@LeakyNun You could use fields to get another example that has nothing to do with the incompleteness theorems. Take the first-order theory F of fields with characteristic 0. Then every model of F has an infinite subfield. This can be stated as an existential second-order sentence, but of course cannot be proven by F since F has no set-existence axioms.

Leaky Nun

@user21820 how would you state that?

user21820

You can state "infinite" by stating "exists non surjective injection" or "exists linear ordering without endpoints".

Okay that's your homework; I'm really going off.

Leaky Nun

@user21820 there's something I want clarification of

there's various sources saying that the Godel's sentence must be true

(but if it's true then it's provable!)

user21820

16:52

Both your comments are wrong.

Leaky Nun

an objective fact can't be false

user21820

6

A: How could a statement be true without proof?

Your confusing stems from the way many articles about Godel's incompleteness theorems are extremely imprecise. Here is a proper definition. $\def\nn{\mathbb{N}}$ We say that a sentence $φ$ over a language $L$ is true in an $L$-structure $M$ iff $M \vDash φ$. For convenience, when $L$ is ...

Leaky Nun

there is literally various sources

user21820

More homework for you.

Leaky Nun

I mean, those sources are imprecise

but you can't say that it's wrong that there are many sources saying that

user21820

16:54

There are various sources stating that the world is supported by a giant turtle. There are many believers saying that their religion is true.

Leaky Nun

yes, I'm saying that the claim that there are various sources saying that is true

user21820

Lol.

Sorry based on your second comment I took it to mean that you accepted what those various sources said.

Since they are both meaningless claims as explained in the linked post.

Transcript for

♦ $Mathematics$ Logic

Transcript for

♦ Logic

♦ $Mathematics$ Logic