Logic - 2017-12-18 (page 1 of 2)

( y ↦ x(x)(y) ) is a program that takes input y and runs x on x and then the result on y. Such a program can be constructed programmatically from the code of x.

LastIronStar

Yeah I got that part

user21820

So you can say "y" here is a dummy variable.

If you understand Javascript:

10 hours ago, by user21820

function S(x) { return ( D( function(y) { return x(x)(y); } ) ? f : t ); }

Leaky Nun

@LastIronStar what language do you speak?

@user21820 by language i mean programming language, obviously

user21820

3:04 AM

English, clearly.

LastIronStar

I see, the program being checked is the function y -> x(x)(y)

Leaky Nun

yes

LastIronStar

cool

user21820

@LastIronStar Yup. And the answer is true/false, so S(S) must output either t or f.

@LastIronStar: Wait, not quite right.

LastIronStar

@LeakyNun I am comfortable with C++, need to learn a functional programming language :(

user21820

3:06 AM

S(S) runs D on ( y ↦ S(S)(y) ).

That is important. It's how the diagonalization works.

LastIronStar

no by D I meant

without the context of S

we are asking D to run a program namely y->x(x)(y) which is defined given an x

Leaky Nun

@LastIronStar int S(int x){ return D( [](int y) { return x(x)(y); } ) ? f : t; }

user21820

@LastIronStar D does not run any such program. It is run on that constructed program.

LastIronStar

@user21820 lol sorry, I meant D takes this as input

user21820

Yes. S(x) runs D on ( y ↦ x(x)(y) ).

LastIronStar

3:08 AM

@LeakyNun Lol, apparently I suck at C++. Thanks Leaky

user21820

@LeakyNun This doesn't really help, because ints cannot be run...

Leaky Nun

@LastIronStar that means you didn't get it?

LastIronStar

@LeakyNun I didn't know the syntax of x(x)(y) can be done on C++

Leaky Nun

@LastIronStar it can't

LOL

user21820

He's not writing valid code. Mine is valid code.

LastIronStar

3:10 AM

wait what?

Leaky Nun

integers are not callable

LastIronStar

OMG, leaky is massively trolling me lol

Leaky Nun

that's a loose analogy

int S(int x){ return D( [](int y) { return to_function((to_function(x))(x))(y); } ) ? f : t; }

user21820

@LeakyNun: I advise you to either let me explain or be precise enough to be correct...

Leaky Nun

where to_function is an encoding

LastIronStar

3:15 AM

I think the intuition is supposed to be that S(S) is nothing but a halting problem decider given D decides P

Is this right?

user21820

@LastIronStar No this undecidability has nothing to do with halting in particular.

Leaky Nun

@user21820 do you have other examples of "behavioural properties"?

user21820

The intuition is that if D truly can decide whether something satisfies P or not, then S(x) can diagonalize to produce an output against what D says about x(x), basically.

Now we cannot actually use "D(x(x))", because "x(x)" may not halt.

But we can use "D( y ↦ x(x)(y) )".

x(x) (if it exists) and ( y ↦ x(x)(y) ) are two different programs, but have the same output behaviour.

LastIronStar

Which book(s) would you recommend for picking up concepts such as decidability et al? @user21820 @LeakyNun

user21820

Anything from Boolos or Kleene should be good.

LastIronStar

3:19 AM

this is the second time i'm hearing Boolos, have to check it now

user21820

→ 11 messages moved to This is the Realm of Simply Beautiful Art

@LeakyNun For example, whether a program halts on at least one input?

Leaky Nun

@user21820 more examples :P

user21820

Or, whether a program either does not halt on any input or outputs 0 on some input?

Or, whether a program has the same output behaviour as q, where q is some fixed program?

In particular this implies that we cannot use a program to find a shortest equivalent program to an input program!

@LeakyNun: Do you see why?

Leaky Nun

hmm

user21820

To make sure the reduction works, use "length-lexicographically smallest equivalent program" instead of just "shortest equivalent program".

@LastIronStar: So did you figure out the proof, or do you want it step by step?

LastIronStar

3:30 AM

@user21820 I need time to figure it out

will probably do it a little later at leisure so that the ideas sink in

user21820

Okay sure!

LastIronStar

I have a question on Cats from what I'm reading. Are you (@LeakyNun @user21820 ) game to listen to my question?

user21820

@LastIronStar Sure, after @LeakyNun finishes thinking about this.

LastIronStar

cool

Leaky Nun

@LastIronStar just ask it

@user21820 I think I see it

user21820

3:34 AM

With the total ordering, it works easily because you could always find the smallest equivalent program of the input and of q and just test equality of strings.

LastIronStar

OK, so it is quite basic I suppose. Definition(Type1) for an isomorphism - a morphism that is two-sided invertible. Definition(Type2) for an isomorphism - a morphism that is bijective morphism

Author claims that second type needn't imply first type of definition.

i.e., a morphism which satisfies Definition 2 needn't satisfy definition 1

I'm having trouble seeing this

The example he uses is category of posets to justify this, but it's quite opaque to me.

Leaky Nun

what does bijective mean?

are you in a concrete category?

LastIronStar

so poset is concrete i think.

user21820

@LastIronStar A bijective morphism may not have an inverse.

The axioms for morphisms do not guarantee that.

LastIronStar

bijective in the sense of a function on sets.

Leaky Nun

3:38 AM

or, its inverse might not preserve the structural properties, so it might not be a morphism

"bijective" has nothing to do with category in general

it only works for concrete categories anyway

@user21820 have you read my sanity check?

38 mins ago, by Leaky Nun

@user21820 sanity check ^

user21820

I did, but found nothing quite sane there. Why on earth do you have to invoke category theory to deal with boolean equivalences? =)

Leaky Nun

@LastIronStar look at the one-object category (groupoid) of $\Bbb C^n$ for fixed $n$

with morphisms being polynomial maps

by Ax-Grothendieck, injective implies bijective

but the inverse may not be a polynomial map at all

LastIronStar

Leaky Nun

exactly

it's non-categorical as I said

a morphism of posets P -> Q is where a<b implies f(a)<f(b) for all a,b in P

the inverse of f would have to send 0 to a and 1 to b

since 0<1, we would have a<b, which is a contradiction (:P)

LastIronStar

nice thanks

user21820

3:44 AM

Off-topic: Cranks are annoying. But those who support cranks are worse...

Leaky Nun

what about those who support those who support cranks?

LastIronStar

crankshafts anyone?

I see huge potential for a pun

user21820

@LeakyNun Supporting is an action. So supporters of supporters of cranks are themselves supporters of cranks.

Leaky Nun

@user21820 so "supporting" is idempotent

user21820

@LeakyNun There are different kinds of supporting, so it's more accurate to call it an action of the monoid of supportings on cranks.

LastIronStar

3:46 AM

damn leaky is right.

user21820

Sorry not a group; no inverse.

Leaky Nun

@user21820 no identity either

oh right, a crank supports itself, so there is identity

LastIronStar

well, apart from that it's a group!

user21820

Have identity; it's the do-nothing action.

Well..

Not quite I guess.

Leaky Nun

@user21820 why do you know category theory?

user21820

3:48 AM

It's the base supporting action.

@LeakyNun I only know the axioms and can see why they are useful for simplifying some algebraic stuff, but I do not know much because I haven't found them actually more useful than just the standard way of shifting perspective.

It's just like you won't say that PA is more useful than ZFC in modern mathematics.

But it helps to work within PA and then step outside to apply the results you get to stuff in ZFC.

Leaky Nun

did anyone say that perspectives form a linearly ordered set under usefulness?

I think it's only a partially ordered set

user21820

Yea but in this case, the two are comparable. Reason being that category theory can be handled entirely in ZFC.

Unless you restrict category theory to be weaker, then you may argue that it is more meaningful than ZFC.

Then that may be one good reason to switch over.

Let me put it differently. Category theory is just like group theory. Of course as an axiomatized system it is extremely convenient when proving general stuff about groups, instead of working with the concrete groups themselves. But ultimately we still need to step outside to apply the stuff we proved.

David Reed

4:04 AM

nah its a directed set

that's the only possible way to get some meaningful net on it

user21820

@DavidReed How so? You're claiming that every two systems has an upper bound in terms of usefulness? What would that mean?

David Reed

no

user21820

Directed set

In mathematics, a directed set (or a directed preorder or a filtered set) is a nonempty set A together with a reflexive and transitive binary relation ≤ (that is, a preorder), with the additional property that every pair of elements has an upper bound. In other words, for any a and b in A there must exist c in A with a ≤ c and b ≤ c. The notion defined above is sometimes called an upward directed set. A downward directed set is defined analogously, meaning when every pair of elements is bounded below. Some authors (and this article) assume that a directed set is directed upward, unless otherwise...

David Reed

I'm claiming that I saw something absurd written about perspectives and usefulness and wrote an equally absurd counterremark

user21820

Actually LeakyNun and I both agree that it's a partial order.

I don't think he'd agree that it's directed. =)

David Reed

4:07 AM

I never even scrolled up, All I saw was the thing about partial order usefulness, persepctive

and felt like being a prick

user21820

Ah. Your typical self? =P

How are you feeling today, anyway.

David Reed

Was just fixing to see family dinner was a nightmare, so if you were actually doing something meanful with that I apologize

say*

user21820

Not really. LeakyNun just has taken a recent fancy to category theory.

Leaky Nun

@user21820 :P

user21820

And by all means, but please don't apply it to boolean equivalences! =)

Leaky Nun

4:10 AM

LOL

Premise: p implies q, p iff r, q iff s
Conclusion: r implies s
Proof: category theory

@user21820 give me a pair of proposition p and q such that (|- p) => (|- q) but not (|- p->q)

user21820

@LeakyNun The problem with that is the step of lifting the category theory proof out to apply it to the boolean implications, which force you to essentially prove what you would have done without category theory.

Leaky Nun

@user21820 I only have to prove that implication is transitive and reflexive :P

user21820

And I'm sure that isn't harder than truth-tables to check the desired theorem?

Leaky Nun

you're talking semantics here: what if I prefixed (forall x) in front of all my premises and conclusions?

user21820

Then Fitch-style proof!

I can do it in a jiffy, but you can too so I'm not going to.

x is unused so it doesn't matter.

Leaky Nun

4:15 AM

who said that?

x might be free in p =)

user21820

You mean inside the premises?

Leaky Nun

mmhmm

user21820

Well so what? Fitch-style proofs for first-order logic then.

Leaky Nun

but that's boring

user21820

@LeakyNun ( S |− ⬜false ) implies ( S |− false ) for any nice S that is Σ1-sound.

Leaky Nun

4:16 AM

I didn't permit S in that position

user21820

"|−" is meaningless without a system.

What system are you using?

Leaky Nun

let's say PA

user21820

Then use S = PA!

Leaky Nun

alright, fair enough

I misinterpreted S due to overloading of |-

user21820

Now a more interesting question is whether we need axioms...

It turns out that pure first-order logic succumbs if there are enough predicate-symbols or function-symbols with enough inputs.

But I've to go a while.

You can think about it.

Leaky Nun

4:19 AM

alright

user21820

Hint: PA− is finitely axiomatized.

user21820

4:35 AM

Better still if you use TC, since it only needs the language to have a single binary function.

@LeakyNun: I feel like I said something about this before in this room. Was it to you or someone else?

Leaky Nun

no idea

user21820

4:53 AM

@LeakyNun: Okay the idea is that the axioms of TC can all be put in conjunction as a single axiom TCA.

Leaky Nun

hmm

so p = TCA -> box false

user21820

Then in any language with one binary function-symbol, we know by deduction theorem that ( TC |− P ) iff ( |− TCA⇒P ).

Yeap!

Leaky Nun

q = TCA -> false

@user21820 descend :D

user21820

Very funny.

Leaky Nun

lol

user21820

4:57 AM

It's probably better not to try using that viewpoint here, because you still need to distinguish between the internal implication and the external one.

Leaky Nun

sure

user21820

And we do know that ( |− (TCA⇒⬜false) ) is false, because TC is sound.

Hence ( |− (TCA⇒⬜false) ) implies ( |− (TCA⇒false) ).

But ( |− (TCA⇒⬜false)⇒(TCA⇒false) ) is false because it implies ( |− TCA⇒(⬜false⇒false) ), which is false by the incompleteness theorem.

→ 8 messages moved to trash

Okay now correct.

Here ⬜P is the sentence over TC that says there is a proof over TC of P.

@LeakyNun: Correct?

Leaky Nun

yes

user21820

There are better results known, but I'm not sure where the MO post is.

Leaky Nun

I’m wondering whether there is incompleteness for intuitionistic logic

user21820

5:14 AM

Of course; remember that any system that can reason about programs falls.

And so in intuitionistic logic all you need is TCA plus LEM for the appropriate stuff.

I'm quite sure you only need finitely many instances of LEM, so we would be done.

Leaky Nun

LEM for what?

how do you know it is a provable LEM?

user21820

I did not say it is provable in intuitionistic logic, but rather you add enough instances of LEM to TCA to get a sentence that is powerful enough to reason about programs despite using intuitionistic logic.

Leaky Nun

oh

user21820

See, when I showed that TC can reason about programs, it does use LEM at some points, like that the first symbol of a string is either 0 or 1.

Things like that. So all you need to check is that you only need finitely many instances of LEM for that to work. If so, then the result still holds.

I think an alternative approach is to use the Gentzen negative translation to embed classical logic in intuitionistic logic.

Leaky Nun

right

user21820

5:27 AM

@LeakyNun: And one could even write the argument for incompleteness in an intuitionistically acceptable way.

@LeakyNun @LastIronStar: Can I ask your favour to flag this comment as rude and abusive? It is abusive in telling beginners not to waste time on other things besides PM. (Also see the user's profile.)

user21820

5:44 AM

Here is Peter Smith's comment about intuitionistic logic and incompleteness:

21

A: Are the Gödel's incompleteness theorems valid for both classical and intuitionistic logic?

The usual proof of Gödel's First Incompleteness Theorem is entirely constructive. We don't have to rely on excluded middle, or have to rely on proving an existential quantification for which we can't produce a witness. For recall: the proof consists in (a) giving a recipe which takes a suitable s...

LastIronStar

@user21820 I have literally 1 rep point in this community.

user21820

@LastIronStar Oh then never mind.

user21820

6:09 AM

@LastIronStar @LeakyNun: Curiously, the undecidability theorem I showed you above is not strong enough to imply the unsolvability of the zero-guessing problem, because the problem cannot be expressed as some behavioural property.

LastIronStar

6:26 AM

ok, so I am scouting other books besides Boolos, have you heard of Martin Davis' book?

@user21820 ^

user21820

@LastIronStar No I haven't heard of that author or book.

@HWalters: Hello and welcome! This room is for (mathematical) logic, so feel free to join in.

@LastIronStar Oh no wonder the name sounded vaguely familiar. He was one of those who resolved the MRDP problem!

Diophantine set

In mathematics, a Diophantine equation is an equation of the form P(x1, ..., xj, y1, ..., yk)=0 (usually abbreviated P(x,y)=0 ) where P(x,y) is a polynomial with integer coefficients. A Diophantine set is a subset S of Nj so that for some Diophantine equation P(x,y)=0, n ¯ ∈ S ⟺ ( ∃ m ¯ ∈ N ...

LastIronStar

6:44 AM

oh ok, so what do you think of the book?

computability & unsolvability

user21820

@LastIronStar I have not read his book before, but in general I think it's safe to read books by anyone who understands the incompleteness theorems, so you could try Martin Davis' book and let me know how you find it!

LastIronStar

@user21820 ok, i'll check it out and ask questions whenever I get one.

user21820

Sure! =)

@HWalters: Just curious; what is your background in mathematics/logic?

H Walters

Just a math minor and random bits picked up in addition from time to time, nothing fancy

LastIronStar

ok i'll pop in later. bye!

user21820

6:49 AM

Ok bye!

H Walters

I'm reading through your post, and find it fascinating. I still think you might be interested in that video; you had mentioned something along the lines that you didn't think it would teach you much about cardinals, but I think that might miss the point...

user21820

@HWalters Ah I see. You can take a look at some of my other posts linked from my profile, for some stuff I wrote related to logic. Or if you have any topic you're interested in, you can bring it up for discussion here.

H Walters

...the video helps make certain concepts a bit more concrete; so you could think of it as an "educational tool"

user21820

@HWalters There is a very easy way to construct concrete ordinals, that is still rigorous.

I am highly doubtful any popular science video will do it right, and I've seen some of those PBS videos before, so that is why I didn't want to sit through it. =)

@HWalters You are right if you consider my post non-concrete. It is written based on ZFC. Totally abstract.

Concrete ordinals have various kinds. The most concrete are obviously computable ordinals.

@HWalters: You sound like you are interested in ordinals. ε[0] is one of the tiniest computable ordinals there is, and there are various ways to grasp it, one of which is via Cantor normal form. If you would like to know more, I can explain briefly about computable ordinals.

H Walters

Well, thanks for the post; I'm not going to have a lot of time here, so I think I'm going to just spend it reading through the rest.

user21820

6:56 AM

Ah okay no problem. You can always ping me here if you have questions.

H Walters

I'd like that, but again short on time... I'm going to leave this channel but if you leave links I'll find it here in the history

And I would be interested, so please do so

user21820

Sure just ping me here any time in the future when you like. I'm here a lot.

See you for now!

H Walters

np

LastIronStar

1:23 PM

@user21820 Hi

user21820

Hello!

LastIronStar

Do you want to continue?

user21820

Sure. Have you gotten the proof of the undecidability theorem?

LastIronStar

I'm sure if we are careful, our discussion should be readable by @Secret once he's in the room. What say ye?

No. I have postponed reading it so that I can read Martin Davis' book. I will start on the book once we are done for today :)

I hate jumping around when learning a concept - Admittedly that's very greek of me but I find the babylonian style suitable depending on the subject.

And Logic seems to not be one of those cases :D

user21820

Ah okay. No problem; you can come back to it next time.

Okay so there are two approaches I thought of for proving the semantic-completeness theorem for propositional logic.

LastIronStar

1:28 PM

I'm all ears.

user21820

Both depend on structural induction, you remember what it is right? Namely if we can assign natural sizes to every member of S and we want to prove that they all satisfy P, then it suffices to show that ( for every x in S, if every smaller y in S satisfies P then x also satisfies P ).

LastIronStar

No, I don't think we discussed structural induction.

user21820

Okay, but do you understand it?

LastIronStar

I don't get the bit on natural sizes otherwise it looks to be some strong subset form of MI

user21820

"assign natural sizes" just means "assign a size that is a natural number".

"smaller" here thus means "has a smaller size (natural number) assigned to it".

It is important that the sizes are natural numbers, otherwise it does not work.

LastIronStar

1:33 PM

wait so y needn't even share elements with x?

it is purely based on size?

user21820

Yes. For example if we want to prove something about all connected graphs by structural induction, we might define their size to be number of edges or something like that.

And so all we need to prove is that ( for every connected graph G with k edges, if every connected graph of fewer than k edges satisfies P then G also satisfies P ), and we would then be able to conclude by structural induction that every connected graph satisfies P.

LastIronStar

are these elements in S sets themselves?

Sorry, I'm having a lot of questions

user21820

@LastIronStar Does it matter whether a graph is a set? All that matters is whether you can prove the claim I stated in brackets.

S is not necessarily even a set.

LastIronStar

ok cool

user21820

Do you get the idea, and roughly why structural induction works?

LastIronStar

1:39 PM

ofc, we need to establish base case as well if i'm not wrong.

user21820

No we do not. As I stated it, it requires you to essentially prove directly that size 0 members of S satisfy P, since there are no smaller members.

So the base case is already inherent in the statement.

LastIronStar

some vacuously holds business?

user21820

Well you can say so. As long as you understand why, it doesn't matter whether you call it vacuous.

LastIronStar

ok go on

user21820

Okay so in our case we have propositions, which are formed from atoms and boolean operations. We shall assign them each a size, which is simply the number of boolean operations in it.

LastIronStar

1:43 PM

ok

user21820

Okay so I shall first present the approach I originally had in mind, namely:

The splitting-cases approach.

We saw that by inserting the proofs of LEM for each atom, we could then split cases completely.

Remember?

We now need to show how to prove the desired theorem in every of those cases.

LastIronStar

@user21820 yes I member.

user21820

For reference, that earlier discussion was somewhere here.

The claim was that if a propositional sentence was a tautology, then it is a theorem. We will now show that it is provable in each of the cases we have split into. Then we would be able to use Or-Elim to obtain it as a theorem.

The example I gave was the tautology Q = A or ( A implies B ) and the proof we will construct will look like:

2 days ago, by user21820

A or not A.
B or not B.
If A:
	If B:
		Q.
	If not B:
		Q.
	Q.
If not A:
	If B:
		...
		Q.
	If not B:
		...
		Q.
	Q.
Q.

LastIronStar

ok, plan is now understood

got it

user21820

So in each case we essentially have the truth values of all the atoms in the tautology.

LastIronStar

1:53 PM

basically each variable has two cases and they are nested successively - so it is like verifying the truth table in some sense.

user21820

Yeap.

We need to show that the tautology can be proven. This is where we invoke structural induction. Let P be the property on propositions that if it is true in that case then it is provable in that case.

Structural induction says we just need to establish this for a proposition X given that it holds for every proposition smaller than X.

LastIronStar

OK, let me process this a bit

Transcript for

♦ $Mathematics$ Logic

Transcript for

♦ Logic

♦ $Mathematics$ Logic