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

David Reed

05:00

@user21820 its effectively a 20x20 truth table

user21820

Anyway I just proved that the puzzle is false. I ask "Will you say no to the question I am asking now?" and none of the gods can answer truly or falsely.

David Reed

@user21820 negative. Random god can answer

user21820

Cannot.

See the Wikipedia definition of Random.

He flips a coin, then answers truly or falsely accordingly.

So he too cannot answer.

David Reed

i stand corrected

you're right

although i don't know that that makes the puzzle false

user21820

As for the da/ja complication, there is a way to reduce to yes/no, so we can assume it's yes/no with our standard meanings.

David Reed

05:04

as you've obstructed yourself from achieving the desired outcome

you've now asked a question and are not any closer to knowing which god is which

user21820

@DavidReed It makes it false in the sense that the puzzle claims these gods exist, but they can't because there is question that none of them can answer according to the puzzle's claims.

From this I can deduce a contradiction, and hence that I can solve the puzzle without asking any question. =D

Leaky Nun

@DavidReed the part where it disappeared

@user21820 oh god

user21820

@LeakyNun Har har. Pun intended?

Leaky Nun

@user21820 not intended

user21820

Lol.

David Reed

05:05

@user21820 I reject that reasoning

Leaky Nun

@DavidReed why?

you follow minimal logic then

David Reed

I don't know what minimal logic is.

user21820

In classical logic, we have the principle of explosion.

David Reed

I reject it because it simply doesn't make sense to me

user21820

false |− P.

I'm using that.

Leaky Nun

05:07

> I reject it because it simply doesn't make sense to me

David Reed

using what?

Leaky Nun

be logical

4

@DavidReed exfalso sequitur quodlibet

aha

user21820

@DavidReed: You want a formal proof? Okay give me a minute.

David Reed

I'm aware of a contradiction proves everything

Leaky Nun

@user21820 there is no proof of axioms

you're just using other axioms

David Reed

05:09

although implicit in that assumption is that the material conditional is an accurate portrayal of the actual conditional

Leaky Nun

disjunction elimination?

David Reed

but also I just don't see a contradiction

Leaky Nun

@DavidReed he just derived a contradiction

user21820

@LeakyNun Of course. I'm not proving that rule, but the claim I just made that David rejects.

David Reed

Give me the True and give me the false

doesn't have to be formal

user21820

05:11

In the world which the puzzle describes, the gods will answer any question either truly or falsely. Instantiate that for the question I wrote above. Then contradiction.

Leaky Nun

twin prime conjecture: ∀x∃y[y>x∧(∀a∀b(ab=y−1⟹a=1∨b=1))∧(∀a∀b(ab=y+1⟹a=1∨b=1))]

what is the classification? @user21820

user21820

@LeakyNun The one you wrote is Π3, however remember that we only count unbounded quantifiers, and here we can bound the quantified a,b.

David Reed

where in the statement does he guaraentee that you will get a response to a question

theres ambiguity in the phrase "always speaks truly/falsely"

Leaky Nun

@user21820 hmm, what is the Π2 version?

David Reed

One could rationally interpret that to mean : If he speaks, he will speak only the truth/not truth"

user21820

05:14

@DavidReed If you interpret that as saying that the gods may not answer at all, then by unsolvability of the halting problem relative to the gods you will find that you cannot solve the puzzle at all either!!!

Because all three could agree to keep silent to keep you in the dark forever.

David Reed

could $\neq$ will

user21820

@LeakyNun Just bound the a,b; you know the factors of a number are no greater than the number itself.

@DavidReed But the point is that you cannot prove any solution correct.

Because I can prove that you cannot.

By constructing a model of the puzzle as described above (all 3 silent), I can show you that any purported solution fails.

David Reed

what happens in the instance that all three are not silent>

what if you get a response to each question you ask

user21820

Then my earlier proof of contradiction applies, since your objection to my interpretation of "always speaks" does not apply.

I'm not sure why you don't understand my reasoning. It's water-tight. It's the puzzle that's flawed.

Leaky Nun

oh

David Reed

05:17

I understand your reasoning

user21820

Perhaps the only way to save the puzzle is to try finding a middle ground.

Leaky Nun

somehow I read unbounded as unbound and got confused haha

user21820

But I don't see a way.

David Reed

but i don't see how in the instance you get an answer from all three i have to change my interpretation of always speaks

user21820

Haha.. bind > bound > bounded. Double past tense.

Leaky Nun

05:19

∀x∃y[y>x∧(∀a∀b(a<y→b<y→ab=y−1→a=1∨b=1))∧(∀a∀b(a<y→b<y→ab=y+1⟹a=1∨b=1))]

English

David Reed

Your objective is to have all three answer your questions. Why would you intentionally ask a question they would not answer>

user21820

@DavidReed The point is that the puzzle is flawed. Give me a precise version of the puzzle and I'll think about it.

Leaky Nun

what's the complexity now?

user21820

@LeakyNun Π2, but seems wrong. Your second part bounds a,b by y−1, but it needs to be y+1...

David Reed

@user21820 something tells me there is going to be inherent imprecision in anything that is ever presented to you :)

Leaky Nun

05:21

alright

user21820

@DavidReed Nah it's just that I dislike puzzles that are presented by people as "world's hardest" or something pompous but are actually so flawed.

If a friend came up with it on his/her own, it would be totally different.

David Reed

I understand

You actually express that sentiment a lot..... a strong dislike of narcissism

user21820

@LeakyNun Normally you rewrite in Skolem normal form before counting, but it's kind of obvious here.

Yup. Well put.

Leaky Nun

well

user21820

Oh and adjacent quantifiers of the same kind are always counted as one partly because Cantor pairing allows us to.

Where can I move this conversation to? Logic (intertwining with the other thread)?

Leaky Nun

05:25

do you use "if" or "iff" for definitions? @user21820

user21820

iff.

David Reed

oh yeah leaky what part of 17.2 were you not following?

Leaky Nun

21 mins ago, by Leaky Nun

@DavidReed the part where it disappeared

David Reed

lol

sry

so I skipped a little because I had sent you 17.1 yesterday

but I will resend it

Leaky Nun

do keep in mind that I'm an idiot

in fact I'm the world's most idiotic person in existence

user21820

05:27

@LeakyNun What's that supposed to mean.

David Reed

user21820

@LeakyNun: If you cannot justify your self-vilification, I'm going to trash it. =)

Leaky Nun

@user21820 well interpretation depends on the domain and the constants and the relations and the functions

@user21820 it's not self-vilification

so your statement is flawed from the antecedent to the consequent

user21820

← 18 messages moved from CRUDE

David Reed

it is self-vilificationn

Leaky Nun

05:29

it isn't

David Reed

some would tell you that repeating that to yourself will reinforce that viewpoint in you

user21820

Hmm it seems we have a disagreement here.

Heh.

David Reed

and you will eventually begin to believe it

user21820

I'm sure LeakyNun is kidding though.

Leaky Nun

it was obviously a parody of this statement:

user21820

05:30

Or using some idiosyncratic notion of "idiot".

Leaky Nun

9 mins ago, by user21820

@DavidReed Nah it's just that I dislike puzzles that are presented by people as "world's hardest" or something pompous but are actually so flawed.

David Reed

idiots don't make it this far on the incompleteness theorem

Leaky Nun

@DavidReed I still don't follow 17.2

David Reed

Maybe its because I'm a zombie right now

user21820

@LeakyNun Actually I don't quite see the link.

David Reed

05:31

but i have no idea what that means

ok let me pull it up for myself and we'll go through it

Leaky Nun

@user21820 well you said you dislike things tagged with "world's ..."

user21820

@LeakyNun You made an invalid deduction! I said "world's hardest" or something pompous.

Leaky Nun

lol

David Reed

Ok

user21820

"world's most idiotic person" does not fit that.

=D

Phew. For a moment I thought there was a loop-hole in my statement allowing people to justify self-vilification...

David Reed

05:33

So Q is the closure of those axioms from the pg that says 16.2 minimal arithmetic

Q is the set of all sentences provable from those axioms

Leaky Nun

@DavidReed why don't you just send me the page instead

David Reed

i did

Leaky Nun

you didn't

David Reed

hrm. well i screenshotted. there were a lot of pages. my bad

here it is

Leaky Nun

you only sent me the first few lines of 17.2

David Reed

05:34

user21820

You two like to argue back and forth like little kids. It is. It isn't. I did. You didn't...

David Reed

user21820

Just kidding.

David Reed

Don't wry about the E rudimentary part

just think of Q as the set of all sentences provable from those axioms

user21820

It's ∃-rudimentary?

And it just means Σ1-sentence, in modern terms.

Leaky Nun

05:36

@DavidReed I just need 17.2

you keep sending me pages

none of those contain the second part of 17.2

David Reed

ok

Leaky Nun

@user21820 we don't

David Reed

Leaky Nun

oh, finally you got that page across, lol

David Reed

maybe the connection doesn't like sending a lot of pages at once. Because on my end I scroll up and see that I've sent you like 15 pgs a few min ago

user21820

05:40

@DavidReed: By the way, are you in your 3rd or 4th year or something?

David Reed

I'm 30

Leaky Nun

so it's "something"

David Reed

why?

Leaky Nun

nvm

@user21820 so somehow soundness is assumed

user21820

@DavidReed Ah okay. You mentioned being a student last time so I thought you might still be. Are you working or doing research?

David Reed

05:41

Ah.

2006-2010 B.S. math at baylor

2010-2015ish drugs/depression

2015-present prereqs for med school

user21820

@LeakyNun It must be assumed somewhere, but I don't know what that 17.2 is doing.

@DavidReed Ah I see. All the best.

David Reed

Thanks man

user21820

Curious that you're so into logic though, since you're now going into med school. Though we need more doctors who are logical...

Leaky Nun

@user21820 17.2 is deriving a contradiction from the fact that there is a formula that determines provability

user21820

But that's way stronger than Godel used.

David Reed

05:44

I maintained a recreational mathematics curriculum over the last few yrs

Ok

Leaky Nun

@user21820 hmm

David Reed

so earlier the book proves that the relation : there exists a proof of formula A, is semirecursive

user21820

@LeakyNun In particular, yes that assumption is where soundness is.

You can significantly strengthen the argument simply by not assuming that and proceeding.

Leaky Nun

@user21820 could you explain to me where exactly Con(PA) and Con(PA+Con(PA)) differ?

they are both sentences over the same language

@user21820 to where?

user21820

The second implies the first but not the other way around?

Wait one question at a time.

Leaky Nun

05:47

ok

David Reed

To clarify, that's not the part of the incomplentess theorem that I sent you, although its in here as well

user21820

You now know how to construct the sentence ⬜P for any sentence P. Moreover you know how to diagonalize to get the fixed-point lemma.

So construct sentence G such that S |− G⇔¬⬜G.

If S |− G, then S |− ⬜G because S can { reason about programs / prove any Σ1-sentence }, but also S |− ¬⬜G by the property of G.

If S |− ¬G, then S |− ⬜G by property of G, but then clearly S is not sound for { program halting / Σ1-sentences } because S cannot prove G (we're assuming S is consistent).

Done.

Leaky Nun

mmhmm

user21820

@LeakyNun Let PA* = PA+Con(PA). Then PA* does not prove Con(PA*). Hence PA* cannot prove ( Con(PA) ⇒ Con(PA+Con(PA)) ).

Leaky Nun

But I'm asking what is the difference between the two sentences

user21820

05:52

Well of course they would be different sentences when you plug them into the machinery, whether using TC or PA−.

I thought you were asking about the qualitative difference.

Leaky Nun

I'm asking about the "of course" part

user21820

The "of course" is because PA and PA+Con(PA) have different proof verifiers, so the sentence generated will of course be different.

I'm of course using the obvious proof verifiers. It is conceivable that they have the same proof verifier, but the above shows that it is impossible.

Leaky Nun

please expand on the obvious proof verifier

where is the difference?

user21820

You can write a proof verifier for PA, right?

Now Con(PA) is some sentence. The proof verifier for PA+Con(PA) simply checks whether each step uses a valid deductive rule or an axiom of PA or Con(PA).

Difference is clearly there.

Leaky Nun

thanks, you could have gone there from the beginning

user21820

05:56

I didn't know it wasn't obvious...

Leaky Nun

I did say I'm asking about the of course part

user21820

I assumed you knew how to write proof verifiers, and it's obvious by definition of PA+Con(PA).

In general for any first-order theory S and sentence P over S, we have S+P denoting the system generated by axioms of S plus P.

Leaky Nun

is Con(PA) unique?

user21820

06:13

Well it clearly depends on your chosen proof verifier.

Which depends on your proof style.

And also depends on the specific phrasing of axioms, in the case of a first-order theory.

Leaky Nun

@user21820 so let's say I wrote two different sentences for the consistency of PA

Con1(PA) and Con2(PA)

I think you can guess my question :P

user21820

Yes I can.

Answer is no.

Wait...

I think it depends.

Leaky Nun

hmm

on what?

user21820

I'm not sure.

Leaky Nun

@user21820 but it also depends on whether I phrase it positively or negatively though

wait, in English no is always negative

user21820

06:17

To make clear, you want to ask whether PA proves ( Con1(PA) ⇒ Con2(PA) ).

Leaky Nun

in Chinese no always negates the question

user21820

Actually, yes it does.

Leaky Nun

wait what

user21820

Interesting, my intuition was wrong.

I think.

Leaky Nun

how did you know that your intuition was wrong

you must have used intuition

but if your intuition is wrong

then you shouldn't trust your intuition

which makes your judgment non-trustworthy

which makes it trustworthy

assuming the soundness of intuition

ok seriously @user21820 what is the answer

user21820

06:20

Working in PA, if ¬Con2(PA), then there exists a proof over PA2 (some specific representation of PA) of "false2" (in that representation), and now PA (using induction) can follow that proof (of arbitrary length) and construct a proof over PA1 of "false1", and hence ¬Con1(PA).

I think induction is necessary because it needs to be able to follow any proof of arbitrary length.

Leaky Nun

PA cannot use induction, what if?

user21820

So for example I think it is not always the case that TC proves ( Con1(TC) ⇒ Con2(TC) ).

Leaky Nun

hmm

that's... absurd

user21820

06:34

@LeakyNun If you really want to know, I could ask this on Main.

Leaky Nun

@user21820 thanks

David Reed

1

A: The infamous sub(s,c,d)

Note: Most of these are from Boolos' "Computability and Logic". It is going to be strongly assumed here that one is familiar with properties of recursive functions and relations. I will define these functions and leave it to the reader to verify they are recursive: $ \\ $ quo(x,y) to be the quo...

@user21820 are this persons comments what you would consider "cranky"

user21820

@DavidReed No? reuns seems to prefer my kind of computability approach, as you yourself noted. So how is it cranky?

David Reed

snotty

"excuse me, but why do you care about these details? I would simply show that.."

user21820

06:49

By "cranky" I didn't mean anything except "by a (mathematical) crank".

David Reed

"pompous"

user21820

But you're reading too much into the first comment; it seems neutral to me, an honest comment from someone like myself who does not see why it is of much interest to do it all out.

I may not use the same words though.

I'll just not read and not comment.

David Reed

this is how I would say it....

"Nice post. You know there's an alternative way of developing this that I personally find to be easier...."

Stipulating that I have not seen the "programming language" approach, I will say that the less precise you are in terms of defining your system/computer/program syntantically and semantically the less confident I would expect you to be with your end result/theorem

Anyways I have to get some sleep. Have a good night.

user21820

07:06

@DavidReed Good night!

@DavidReed That's true, LeakyNun and I faced a similar issue when attempting to literally produce a sentence over TC/PA− by the computability method. We found that there was no going around building essentially a compiler inside the system, so the best might be a minimalist compiler that still supports high-level looping.

@LeakyNun: I hope I'm not missing some obvious trick...

0

Q: Equivalence of different consistency sentences

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

@LeakyNun But if my guess is correct, I don't find it absurd because TC is really too weak to do inductive reasoning; it can only check specific finite sequences, not reason about all finite sequences.

We'll see. I tend to get very little attention for my posts, compared to rubbish like "Is this batman equation real?"

@DavidReed @DavidReed: By the way, I think there is a way to fix the logic puzzle. The fixed version stipulates that the gods will always answer if the question can be justified to be a true/false question about reality. The question I gave is indeed not justifiable (by any reasonable means) to be of that kind, as explained in my post about the paradoxes. This fix is imprecise, but the easiest way to make it precise is to stipulate exactly what sentences are allowed, which kind of spoils the fun.

For instance we would have to say that we can form atomic sentences of the form "A/B/C is True/False/Random" and "da/ja means yes/no" and that we know who A/B/C refer to, and so on. This would really spoil the fun.

user21820

08:07

This fixed version prevents not only my proof that the puzzle is flawed, but also the 'alternative' solutions given in the Wikipedia article, which are of the same kind of question as mine. For this fixed version, I deduced the same solution as Boolos, which is permitted by the above restrictions. Here is the full explanation:

If every question we ask could be answered by Random, then we are doomed because we get zero information.
Therefore we must figure out how to ask questions to True or False.
First note that we can assume we know which of ja/na is yes/no, because we can append "xor ( ja means no )" and treat "ja" to mean "yes", since the appended proposition is false iff "ja" means "yes".
Next note that we can assume True and False answer truly by appending "xor ( you are False )", since the appended proposition will negate the answer iff you are asking False.

No need for messy truth tables at all!

Leaky Nun

11:42

Let G be a formula such that for all P and X, ⊢[G(P,X,0)⟺Q(X,0)], where P="Q".
Now, let D(P,n) := ¬G(P,P,n).
Assume ⊢D("D",0). Then, ⊢¬G("D","D",0) by def D. Then, ⊢¬D("D",0) by prop G.
Assume ⊢¬D("D",0). Then, ⊢G("D","D",0) by def D. Then, ⊢D("D",0) by prop G.
Therefore no such formula G exists.
---
Let G be a formula such that [⊢G(P,X,0)⟺Bew(P++"(X,0)")] and [⊢G(P,X,1)⟺Bew("¬"++P++"(X,0)")].
Then, for any P and X: let "Q"=P.
Assume ⊢Q(X,0). Then, ⊢Bew("Q(X,0)"). Therefore, ⊢G(P,X,0).
Assume ⊢¬Q(X,0). Then, ⊢Bew("¬Q(X,0)"). Therefore, ⊢G(P,X,1).

@user21820

user21820

12:18

What is this?

You should have split into two.

@LeakyNun The first section is wrong in the last line. Just because there is a sentence that cannot be proven or disproven does not imply a contradiction.

Leaky Nun

@user21820 oh right

user21820

@LeakyNun The second section seems wrong in the first line, but it's syntactically malformed so I don't know what it's supposed to mean.

Leaky Nun

what's wrong with the first line?

user21820

You didn't prove that such a G exists.

Leaky Nun

I'm trying to translate your stronger proof into PA

I don't even know what "halt" means

I assume it has something to do with a finite number

user21820

12:23

Hmm, don't you know what "program P halts on input X" means?

"exists finite sequence of states such that..."

Leaky Nun

@user21820 yes, but I don't know how to translate it to PA

user21820

Just use Godel coding and the section in my post about how to code a finite sequence of strings as a single string? Finite string can be coded as a natural, no problem.

But if you want in terms of provability...

That's why I said it feels like the stronger version is not similar to Rosser's trick.

Leaky Nun

hmm

user21820

You want C to diagonalize against the zero-guessing decider... So C(x) should be equal to 1 iff x(x) = 0 but equal to 0 otherwise. In terms of a 'fixed-point' style, you want C to be represented somehow by a sentence.

Leaky Nun

I'm not even sure what the zero-guessing means

user21820

12:35

Wait did you read the section using the zero-guessing problem?

Leaky Nun

@user21820 yes

what I mean is

as I've said above

sigh

I'm not sure how to translate zero-guessing to PA

user21820

You need a 2-parameter sentence for the function C.

Because you need to represent the function's output.

Leaky Nun

55 mins ago, by Leaky Nun

Let G be a formula such that for all P and X, ⊢[G(P,X,0)⟺Q(X,0)], where P="Q".
Now, let D(P,n) := ¬G(P,P,n).
Assume ⊢D("D",0). Then, ⊢¬G("D","D",0) by def D. Then, ⊢¬D("D",0) by prop G.
Assume ⊢¬D("D",0). Then, ⊢G("D","D",0) by def D. Then, ⊢D("D",0) by prop G.
Therefore no such formula G exists.
---
Let G be a formula such that [⊢G(P,X,0)⟺Bew(P++"(X,0)")] and [⊢G(P,X,1)⟺Bew("¬"++P++"(X,0)")].
Then, for any P and X: let "Q"=P.
Assume ⊢Q(X,0). Then, ⊢Bew("Q(X,0)"). Therefore, ⊢G(P,X,0).
Assume ⊢¬Q(X,0). Then, ⊢Bew("¬Q(X,0)"). Therefore, ⊢G(P,X,1).

are you talking about my G?

user21820

The problem is that it's not clear that it exists by the fixed-point lemma.

Leaky Nun

I mean, is my G above the correct way to phrase the "zero-guessing decider"

user21820

12:41

As I said I can't tell because you didn't explain what "++" means, but the idea looks correct, though as I said you didn't prove that such a G exists.

It's not just concatenate...

Leaky Nun

not just?

user21820

And I don't know why you didn't phrase it the same way as the earlier one.

Leaky Nun

oh

well

I should have

user21820

It's not, because you can't just concatenate the code with "(X,0)".

Leaky Nun

oh, I'm supposed to substitute

user21820

12:42

That's why "syntactically malformed".

Leaky Nun

good point

but I'm asking whether it's your intended translation of your proof into PA-

user21820

The first section also is wrong because you didn't use soundness.

@LeakyNun The second section first line is still wrong because you didn't diagonalize.

Leaky Nun

@user21820 your proof didn't diagonalize in the second section

user21820

It did. C did the diagonalization.

Leaky Nun

@user21820 you said you don't need soundness

user21820

12:46

@LeakyNun Your first section needs.

Leaky Nun

C isn't even in your proof

user21820

Mine doesn't.

Leaky Nun

@user21820 which is why I'm asking you for a better translation...

user21820

Sorry D.

> Let D be the program constructed in the proof that G does not solve the zero-guessing problem.

Leaky Nun

not this section

the section above

user21820

12:48

@LeakyNun I'm saying you didn't even translate the first section (which mirrors Godel's proof) right.

Leaky Nun

1 min ago, by Leaky Nun

@user21820 which is why I'm asking you for a better translation...

now we're going in circles

by "first section" I mean "Zero-guessing problem"

user21820

Wait look at my first two messages responding to yours. I was splitting your message into "first section" and "second section".

Next time don't put unrelated things in the same message.

Leaky Nun

unrelated?

user21820

@LeakyNun <− I'm going to repeat myself; your first section is wrong even if you remove the last line.

Leaky Nun

the first section in my message is "Zero-guessing problem" and the section is "Rosser's incompleteness theorem via the zero-guessing problem"

@user21820 could you just translate the whole thing into PA instead of having me embarrass myself and not getting what you/I want?

user21820

12:52

Oh sorry I'm the one making the embarrassing mistake.

It's not wrong, but not the argument you want.

> Assume ⊢D("D",0). Then, ⊢¬G("D","D",0) by def D. Then, ⊢¬D("D",0) by prop G.
> Assume ⊢¬D("D",0). Then, ⊢G("D","D",0) by def D. Then, ⊢D("D",0) by prop G.

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

user21820

You do not want to work in the meta-level.

Do that two lines inside the system.

Leaky Nun

it's inside the system

user21820

If D("D",0) then ... hence contradiction. If not D("D",0) then ... contradiction.

No you did it outside by saying If |− D("D",0) then ...

Which is why I glanced at it and said there's no contradiction.

But actually if you do it inside you get a contradiction.

Leaky Nun

well I'm doing it inside, I just prefixed everything with ⊢

user21820

12:56

No that's incorrect.

You are stating something of the form ( If ( S |− P ) then ( S |− Q ) ).

Leaky Nun

that's just a misunderstanding

user21820

What you want is the stronger ( S |− P ⇒ Q ).

Your notation means the former.

Leaky Nun

well

if you insist

oh, I see it

user21820

Sorry it's just like that. You'll find it that way in standard books.

It's important to know the distinction.

Because it's strictly stronger if you can prove the implication inside.

Leaky Nun

D("D",0) [assumption]
¬G("D","D",0) [def D]
¬D("D",0) [prop G]
⊢D("D",0)→¬D("D",0)

better?

user21820

12:58

Yes.

Leaky Nun

move on

user21820

And similarly for the next one. So that you get |− false.

Leaky Nun

agreed

user21820

For the next part you wrote:

> Let G be a formula such that [⊢G(P,X,0)⟺Bew(P++"(X,0)")] and [⊢G(P,X,1)⟺Bew("¬"++P++"(X,0)")].

Transcript for

♦ $Mathematics$ Logic

Transcript for

♦ Logic

♦ $Mathematics$ Logic