Logic - 2017-12-10 (page 3 of 3)

moving unrelated msgs in philosophy chatroom

@Secret this observation is also the same one that is made about what computers really compute!

@LastIronStar: Well those are just fancy ways of saying you can only store finite information in finite spacetime.

=)

3:10 PM

haha true that, although now that you've phrased it this way, i am led to question whether spacetime is a fundamental resource as we might be led to extrapolate from our sensation of time.

that bears remarkable resemblance to the infinite energy machine/theorem that the person in here the other day was talking about

user131753

@DavidReed I see. Sorry for the confusion.

@LastIronStar Empirically, my statement is true. It may not be, of course, but we haven't seen any way of violating it.

@DavidReed Yeap I guess so.

@user21820 This leads me to question if "reason" is as fundamental as we think it is or is it another faculty not merely bounded by evolution but also evolved as necessary to tackle a local problem and is just that - a local way of looking at our reality rather than its current perception as a global, independent facet of looking at reality that evolution luckily picked up as an ideal to shoot for and refine

ofc, the disclaimer being that so far it seems the latter view has enjoyed much success in terms of advancing civilisation. perhaps.

Most neurosci profs would tell you that reason is inexorably tied to language

3:15 PM

@DavidReed: By the way, I think I forgot to say that in the ideal program model the fact that there is no surjection from obj to func(obj,bool) is the same fact as that there is no program to decide the set of deciders.

So it's a completely natural phenomenon.

Ok. I will likely need to refresh on computability for a lot of our discussions I think.

@LastIronStar I can't recall whether you were present last time, but I sort of said that it's quite clear that the entire real world obeys classical logic.

The only way I was able to interpret the presence of bool was you referring to surjections from a set onto its powerset

@user21820 Given today's my first day here, you can presume I've not seen any discussion barring from today :)

@DavidReed Yes that's the typical set-theoretic view. But I think you can now easily understand the whole type theory business from a computability view.

3:19 PM

@user21820 Also, the entire world? I would be interested to read the arguments for this claim.

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

@LastIronStar Entire meaning that as a whole.

See this:

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

We accept that there is the real world, whatever it is. Consider the entire real world, meaning literally everything.

Then any sentence about it has to be either true or false and not both.

Of course this is necessarily imprecise because I'm using natural language, and you can argue what is meant by "sentence about it".

But you should get the point.

but how do you argue this standing outside temporality -as in, what is true at one moment maybe false at another.

so implicitly you are invoking the concept of a "moment" of time to establish the truth value of a statement.

@LastIronStar When I say "sentence" I do mean it must be sufficiently precise, so that it is absolute and not something that changes with context.

For example, "Something exists." is reasonably precise and no one will doubt it.

@DavidReed: Well so suppose we extend the nice ideal program model a bit by simply adding the finite Turing jumps.

And furthermore we add induction, which means that not only can we construct ideal programs that can use the jumps, we can reason about them classically with induction.

Then this immediately gives a system equivalent to ACA.

If you measure the probability that an axiom is true by the degree to which it proves counter-intuitive statements I would argue AOC has a low probability of being true

3:34 PM

@DavidReed Indeed just by its logical structure alone, the vastly generic claim that every set of sets has a choice function ought to be false somewhere.

But that is if it is a meaningful question to begin with.

I am of the opinion that ZFC is consistent but as I said before lots of things are consistent and we know that most of them are meaningless.

So the burden lies on the one proposing some system to be meaningful, and not on the one objecting. =)

Are you familiar with Banach-tarski paradox

Yeap.

That one actually does not use any transfinite induction, if I recall correctly.

Those are the types of theorems I am referring true. I would treat any axiom that proves statements like that with a healthy degree of skepticism

I certainly would not characterize them as "obviously true"

6 hours ago, by user21820

@LeakyNun The issue here is that you need to know that you can determine whether "φ(g) = n for some g ∈ func(N,bool)". Depending on your personal philosophical view, this may or may not be justifiable.

6 hours ago, by user21820

If you take a strict constructive view, then this is probably not justifiable, since you are now (you hope) constructing a member of func(N,bool) and ought not to be able to ask questions about the whole type func(N,bool).

Oh yes

Please tell me your exception to transfinite induction

or you're "taking exception to" rather

3:41 PM

@user21820 I'm still digesting these two important messages

I know it isn't constructive (because it uses excluded middle)

but what makes it not predicative?

@DavidReed I'll try to make it short and as little philosophical as possible, so that I can go soon haha.. Well in the cumulative hierarchy (which we can build in ZFC) V[ω+ω] satisfies ZFC minus replacement. Also V[ω+w] does not have the von Neumann ordinal ω[1] despite having the collection of all countable well-orderings.

So ZFC itself acknowledges that replacement is necessary to get ω[1], and that it is qualitatively different from just the collection of countable well-orderings.

Now if we are to accept ZFC over ZFC−R as foundational, we had better have some good philosophical justification for it.

As shown in my post, the typical justifications that many set theorists give for replacement are actually circular.

Honestly it's been 4-5 yrs since I went through an axiomatic construction of ZFC. I will need to skim back through this. I will definitely do so with an open mind to your criticism of it

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

@LastIronStar: I guess you haven't seen it before:

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

Just note that Boolos himself shared the same exact view, and I wrote my original post before I found his writing on the same exact topic.

@user21820 will I still not be able to prove it if I encode function as sets of pairs instead?

(pairs = product type, sets = type)

apologies, was running an errand

3:50 PM

did you mean to ping me for that link or ironstar 820?

so 820 is the surname of user21820 now? :P

Not you, because I already showed you that link before.

is user21 your name then

or just 21

@LeakyNun The point about the predicative viewpoint is that we must justify that something is predicative before we can assume it. In this case, it is acceptable to construct a program ( obj x ↦ x ∈ func(obj,bool) ? ¬x(x) ), as long as we don't assume anything too strong about func(obj,bool).

So if we merely assume that f is accepted by func(obj,bool) when we manage to prove it, and not assume that func(obj,bool) will reject everything that it does not accept, then it can be predicatively acceptable.

the main problem is that I don't know what predicative means

it's a term you throw around

3:53 PM

It's not a fixed terminology; you can search the internet and every logician has a slightly different view. But we mostly agree that ZFC's specification and replacement schemas are dangerously impredicative, and that ACA is nice and predicative.

The idea is just that predicative stuff are obviously well-defined.

Where again, obvious is a bit subjective.

I still have no idea what predicative means, but one thing is for sure:

you're defining predicative impredicatively

Yes that is right! I distinguish between entities and notions.

which makes it unable to decipher what you mean

is predicative a subset of constructive?

There are impredicative notions, which include "predicative", and there are predicative entities.

Constructing something that depends on the collection containing it is usually suspicious.

This is not the case if you already have the collection.

just a yes or no would do

3:56 PM

@LeakyNun Neither yes nor no, because "constructive" is another word that many people use with varying meaning, so you notice I have mostly avoided using that word.

constructive logic is classical logic done without LEM and DNE

To be slightly more precise, my version of predicative means that you can justify the well-foundedness of the definitions of the objects you wish to construct, in which case those objects are predicative.

So if you a priori accept that func(N,bool) exists and is fixed, then it is predicatively acceptable to construct a member of it that depends on quantifying over it.

@user21820 But that's the thing, the precision in specification that we can look for is limited by our perception and inference engines (read big brain).

could you define predicativity in a non-circular manner so that I can understand?

@LeakyNun I actually already defined a strict version earlier, which I called predicative higher-order arithmetic.

Starting from here:

6 hours ago, by user21820

Going this way leads to strictly predicative type theory, which is PA at 1st-order and ACA at 2nd-order and can easily be extended to higher-order.

This is the strictest, and most obviously sound, predicativism. Its main philosophical assumption is the existence of a fixed collection of natural numbers and their basic properties.

If you understand this notion of predicativism, you understand why we cannot really pin down what is 'safe' if we want to go beyond this strict version.

4:04 PM

I am out for $\frac{1}{2}$ hour.

@LastIronStar I will be away for much longer, soon, so see you next time!

@user21820 cool

@LeakyNun: Do you get the idea, at least for the strict one?

@user21820 lemme digest

It is because there is really no concrete notion of the powerset of N or equivalently func(N,bool), apart from the notion that if f decides "yes" or "no" on every natural number input, then f is in. That is precisely the reason that Lowenheim-Skolem paradox can work, because there are only countably many 'definable' things in some sense. From a philosophical viewpoint, there is no reason to suppose that there is some actual entity comprising every (in the sense of ZFC) subset of N.

Consider an impredicative example M = ( nat x ↦ ∀f∈func(nat,bool) ( f(0) ∧ ∀n∈nat ( f(n) ⇒ f(n+1) ) ⇒ f(x) ). This is a rather tame example, for certain reasons, but don't look closely. Just notice that M quantifies over func(nat,bool), so should that quantification have a boolean truth-value? If so, then M would be a member of func(nat,bool), and how do we know that M cannot somehow diagonalize, since its behaviour depends on the behaviours of all members of a collection that includes itself?

In general this worry cannot be eliminated unless func(nat,bool) is fixed already, and so this definition would merely identify something from that fixed collection. That is why most logicians consider such definitions to be impredicative. There is even a precise classification by logicians. This would be classified as Π[1,1].

As I mentioned to @DavidReed earlier, there is a field called Reverse Mathematics.

Reverse mathematics

Reverse mathematics is a program in mathematical logic that seeks to determine which axioms are required to prove theorems of mathematics. Its defining method can briefly be described as "going backwards from the theorems to the axioms", in contrast to the ordinary mathematical practice of deriving theorems from axioms. It can be conceptualized as sculpting out necessary conditions from sufficient ones. The reverse mathematics program was foreshadowed by results in set theory such as the classical theorem that the axiom of choice and Zorn's lemma are equivalent over ZF set theory. The goal of reverse...

And the strongest well-known system in that field (of the Big Five) is called Π[1,1]-CA, which almost all agree is impredicative.

I guess I missed a close-bracket in my example haha..

Q: Equivalence of different consistency sentences

4:37 PM

@LeakyNun: By the way, the question I posted after you asked me about the coding scheme now has an 'answer' by Peter Smith, saying that he asked this before on MO...

@DavidReed: You may be interested in it as well:

4

Take any formal system $S$ that has a proof verifier program and interprets TC or PA$^-$. $ \def\imp{\Rightarrow} \def\con{\text{Con}} $ Then the incompleteness theorems show that $S$ does not prove $\con_1(S)$, where the subscript denotes that it is based on a particular encoding of a particula...

4:49 PM

what complexity are those sentences?

I think it’s S1

@LeakyNun The ones in my post? Yes every program halting is Σ1.

So existence of a proof is Σ1.

Consistency would be Π1.

If you're comparing against second-order arithmetic, then in fuller form it is Π[0,1], where 0 indicates "no quantifiers over sets of naturals".

Written Π^0_1.

→ 2 messages moved to trash

It was splitting my train of messages anyway. =P

@LeakyNun Wait, if you're asking about the equivalence, it is neither Σ1 nor Π1.

no, not equivalence

Con1(S) and Con2(S) are individually Π1-sentences.

That's why the incompleteness theorem is very sharp. PA−/TC is Σ1-complete; it proves every true Σ1-sentence. It fails for Π1-sentences and hence there is nothing left 'in-between'.

Σ2-sentences includes Π1-sentences, so we essentially have fully characterized all these complexity classes concerning their 'completeness'.

@DavidReed: Oh by the way, I just remembered something. You said this:

9 hours ago, by David Reed

I would not feel comfortable even going to 2nd order

I responded by telling you about ACA. But I forgot to say that going to full second-order arithmetic is precisely what people who have predicative concerns are afraid to.

It's called Z2, and it's of course way stronger than Π[1,1]-CA.

5:06 PM

Ok, thanks man. Sry for on and off response

I am drifting in and out

@DavidReed If you haven't got your sleep, please do. I'll be offline soon.

See you!

It is very important that you understand that this chatroom/site is not what is keeping me awake. I don't want you to feel that you are in any way enabling that behavior

This is just a general side effect of an acute medication change