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

« first day (479 days earlier) ← previous day next day → last day (2633 days later) »

user21820

13:00

Doesn't make sense why you have 3 zeros and 1 one.

That's why I was saying it must be wrong.

Leaky Nun

> Let G be the following program on input (P,X):
For each string s in length-lexicographic order:
If V( "The program P halts on input X and outputs 0." , s ) then output 0.
If V( "It is not true that the program P halts on input X and outputs 0." , s ) then output 1.

funny

user21820

Oh lol.

Leaky Nun

your write-up has exactly 3 zeros and 1 one

user21820

Argh my intuition is failing badly.

Leaky Nun

are you alright

sleep deprivation?

not awake?

user21820

13:01

I'm alright but a bit too lazy today.

Leaky Nun

move on

user21820

But we can't move on anyway; this is the crucial part; we don't have an obvious way to prove that G exists.

Leaky Nun

then how should I translate that part?

user21820

Well the way I would do it is to simply translate the entire program as one piece. Rather than to try following a Godel-proof-like approach.

Namely, you see the definition of G in my post, right?

It's a well-defined program.

Leaky Nun

which corresponds to a formula

user21820

13:05

Just dump it into the system as a formula, and then apply the unsolvability proof.

Yea.

Leaky Nun

but I want to write the formula

user21820

But I think you won't be too satisfied with that.

Leaky Nun

@user21820 you know me too well

user21820

Well it's not hard, is it? It's a program so there is a 2-parameter sentence that corresponds to it.

Leaky Nun

3-parameter, since I have two inputs

> it's not hard, is it?

we're doing this again

user21820

13:07

That's also fine; I had in mind combining (p,x).

Leaky Nun

13 mins ago, by Leaky Nun

I'm saying, instead of telling me repeatedly that I'm wrong, which I know I am, just translate it to PA correctly

I already did it once

you said it's wrong

and your comment now is "it's not hard, is it?"

no it isn't, but I don't know how to do it

user21820

But you do; γ(p,x,y) ≡ ( p(x)=0 ∧ y=0 ∨ p(x)≠0 ∧ y=1 ).

Pass it through the encoding.

And you'll get a γ that represents G.

Leaky Nun

γ(p,x,y) ≡ ( p(x,0) ∧ y=0 ∨ p(x,n) ∧ n≠0 ∧ y=1 )

user21820

With an existential.

Leaky Nun

in the front?

user21820

13:11

γ(p,x,y) ≡ ( p(x,0) ∧ y=0 ∨ ∃n ( p(x,n) ∧ n≠0 ) ∧ y=1 )

Leaky Nun

are they equivalent?

anyway

user21820

The two I wrote are equivalent at the high-level. After encoding, they remain equivalent because the system is assumed consistent and Σ1-complete.

It can prove every true Σ1-sentence, which is the same as saying can reason about programs.

Leaky Nun

wait, you dropped the Bew

user21820

Oh.

Forgot.

Leaky Nun

Could you write G though

G(P,x,n) := Bew("Q(x,0)") ∧ y=0 ∨ ∃m (m≠0 ∧ Bew("Q(x,m)")) ∧ y=1)

user21820

13:16

No that's not correct, because we must have the negation under the box.

γ(p,x,y) ≡ ( ⬜p(x,0) ∧ y=0 ∨ ⬜¬p(x,0) ∧ y=1 )

Leaky Nun

oh right

why do you keep using gamma?

G(P,x,n) := Bew("Q(x,0)") ∧ y=0 ∨ Bew("¬Q(x,0)") ∧ y=1)

user21820

To emphasize that it's not the same as the program G.

But never mind.

Leaky Nun

To prove: for all P and X, ⊢[G(P,X,0)⟺Q(X,0)], where P="Q".

Assume ⊢Q(X,0) outside the system

Then, ⊢Bew("Q(x,0)")

can't prove it inside the system...

user21820

Right. This must be meta.

Leaky Nun

then how do I prove that property?

user21820

13:19

Oh your zero-guessing problem was too strong.

> If P halts on X, then the answer is 0 if P(X) = 0 and is 1 otherwise. (If P does not halt on X, then any answer is fine.)

Leaky Nun

but then I would need soundness

user21820

No you don't, you can say "if P halts on X".

Leaky Nun

what does that mean in PA-?

user21820

Halting is just a Σ1-sentence.

Wait copy your attempt:

> Let G be a formula such that for all P and X, ⊢[G(P,X,0)⟺Q(X,0)], where P="Q".

Correct should be:

> Given G be a 3-parameter sentence over S such that for any program represented by a 2-parameter sentence P coded by p such that ( N |= P(x,k) for some natural k ), we have S |− G(p,x,0) ⇔ P(x,0), ...

I think.

That's why I hate doing it this way; so prone to error.

Leaky Nun

that's why I love doing it that way :P

user21820

13:34

Then your D looks wrong now too...

I'm getting a headache doing it this way.

Leaky Nun

lol

user21820

The reason is that instead of using programs you are trying to use formulae, but that's very troublesome because you can't just use any formulae but those that represent programs..

So it gets messy quick.

If you want to go the formula way, I think all you need is a stronger fixed-point theorem.

The usual one says that given any 1-propositional-parameter sentence F whose parameter is under the ⬜, you can construct a sentence P such that the system can prove P⇔F(P).

That's like recursion with 1 program.

You need recursion with 2 programs.

I think.

Leaky Nun

hmm

user21820

Namely given any 2-propositional-parameter sentences F,G whose parameters are under the ⬜, you can construct sentences P,Q such that the system can prove P⇔F(P,Q) and Q⇔G(Q,P).

Leaky Nun

what do I get if I use “not X” as my formula for my usual fixed point theorem?

user21820

13:42

You can't; the parameter must be under the ⬜.

If you look again at the proof of the fixed-point theorem you will see that you can only construct the sentence when only its code is used recursively, not its truth value.

So as long as it is under the box it is fine.

But let me do something else for today. Not really in the mood for playing with 2d-modal-fixed-point theorems.

Leaky Nun

3 hours later…

Leaky Nun

17:01

@KennyLau What would convince me is a proof that a proof for this question requires induction; just saying it's necessary will not. — Duncan Ramage 1 hour ago

@user21820 lol

6 hours later…

Leaky Nun

23:25

@user21820 how is this?