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

LastIronStar

11:00

I see you and secret are having a similar discussion like the one we've had.

Good stuff, lot more people onboarding onto Logic Studies = more fun discussing!

user21820

Yea it's good.

Have you figured it out for yourself yet?

Secret

@user21820 you mean the program proof? For that one I am ok with it now after your explanation

LastIronStar

Nah man, I've been busy the past 24 hours - had to make a topic presentation to my advisor. But looking at transcript now to recollect and convince myself :)

user21820

@Secret If so, then just understand all English proofs in terms of their program representations.

And use the above translation I gave you to understand conventional form of arguments.

For example the last one you quoted translates to:

If ( Joe is now 19 years old ) and ( Joe is now 87 years old ):
  Bob is now 20 years old.

But it is impossible to justify that inner statement in its context, so the argument is invalid.

LastIronStar

@user21820 wait are you saying that this example is not a VALID argument? Its premises can't all be true at any point in time!

user21820

11:12

Oh sorry. You are right; I didn't read the premises carefully.

It is valid, because you can justify that that context is impossible and hence it is safe to assert anything you like in it.

Really sorry; I saw "Joe ... Joe" and "Bob" and thought "Premises irrelevant." lol...

LastIronStar

basically my understanding regarding Programmatically stylised arguments that we've been discussing is this:

Secret

what do you mean by inner statement? The stuff in brackets?

LastIronStar

A PSA is valid iff in the program's context, all assertions are true.

user21820

@Secret There is one context governed by "If ( Joe is now 19 years old ) and ( Joe is now 87 years old ):" and one sentence "Bob is now 20 years old." within that context. Please see my later remark retracting my original claim.

LastIronStar

PSA = Programmatically Stylised Argument(s)

since i'm not sure what they are actually called or even they have a name

user21820

11:15

I don't know whether they have a name, but it's something I came up with to explain logic to CS students.

LastIronStar

ok, I vote to call it PSA

rather ASP

user21820

@LastIronStar It's slightly stronger than that. a PSA is valid iff all the assertions that it executes are guaranteed to pass.

LastIronStar

cos the former is ambigous

@user21820 perfect, i was also searching for how to include the "execute" bit

sorry about the confusion, let's call it ASP instead.

user21820

ASP is ambiguous too; there's a language called ASP and an animal called an asp.

LastIronStar

oh ok, let's just stick to PSA then

my question now is forallx's notion of VALiD and this notion of VALID - are they equivalent?

It seems to me that PSA notion of VALID is slightly more water tight in resolving questions about hypothetical behaviour of VALID arguments

user21820

11:20

forallx's is actually slightly wrong in its explanation.

Sigh.

Consider the following 'argument' S (for silly):

Premise: Cows are animals.
Conclusion: Goats are animals.

According to the literal definition given in forallx, this is a valid argument simply because the conclusion is always true (in our world).

But according to my definition, you won't be able to justify validity of the corresponding PSA, and hence the validity of the original argument.

And for good reason. After all you won't consider it logical... Wrong method and right answer does not make a valid solution.

My example is a clearer instance of the problematic issue than the one given in forallx about Paris and France, since goats will forever be animals.

Secret

I still don't quite get the relationship between all these conventions that are floating around here. Using my understanding, asserts Premise: "Cows are animals." is true then the conclusion: "Goats are animals." can be true or false without triggering a contradiction

Using your program interpretation of the above statement, "Cows are animals" is true said nothing about "Goats are animals."

Using forallx interpretation: both "Cows are animals" and "Goats are animals." are true in the real world

user21820

@Secret So use my definition of validity and forget the rest.

LastIronStar

Here's the PSA explicitly:

@user21820 How are you writing multiline programs on chat here?

Secret

shift enter

user21820

Heheh.

LastIronStar

11:31

tks

If (Cows are animals):
    Goats are animals

user21820

Alternatively you can type it somewhere else then paste. But remember to click "fixed font" so that it doesn't eat up your spaces.

@LastIronStar Right.

LastIronStar

now the program always executes

and the assertion is always true

so PSA also says this is a VALID argument!

user21820

I may have been slightly ambiguous in one of the many explanations I gave earlier, but I always intended to emphasize that it is only valid if you can guarantee it without executing it.

LastIronStar

17 mins ago, by user21820

@LastIronStar It's slightly stronger than that. a PSA is valid iff all the assertions that it executes are guaranteed to pass.

Secret

My understand of PSA is like so:

Define program P as:
If (A)
B

A is safe (either True or False).
P is valid iff B is True?

LastIronStar

11:35

I think you can be a bit more clearer - please define VALID for PSAs once and for all. Take your time to do it precisely - i feel it is important that we fix this for eternity @user21820

user21820

The problem is that you need to encode "cows" and "animals" and "goats" and "are" somehow into program form. After you do that, you find that you can no longer guarantee that its assertions pass.

Secret

Yeah, I felt like I need semantics free sentences like A, B in order to fully understand what is the criteria of validity

Everytime there are possible semantics, my mind go tree diagrams and then I got confused

user21820

@LastIronStar The easiest way is to simply say that I only accept those that correspond to a valid Fitch-style proof as given in Chapters 6−7.

But I didn't want to do that because I want to motivate the rules in those chapters.

That's why the best I can do is to emphasize that you must be able to justify that every assertion (in true program form; not with random English bits) passes.

Let me show you what that example becomes:

If ∀x∈Cows ( x∈Animals ):
  ∀x∈Goats ( x∈Animals ).

If you want pure first-order logic:

If ∀x ( Cow(x) ⇒ Animal(x) ):
  ∀x ( Goat(x) ⇒ Animal(x) ).

Unfortunately, real-world programs cannot handle quantifiers, so you have to just imagine an oracle giving you the answer for now.

@LastIronStar @Secret: That is why all I actually wanted is for you to understand the correspondence between my example Fitch-style proof and the program fragment, and the reasoning for why the last line in both is valid. That kind of reasoning is all you need to understand all the rules in Fitch-style natural deduction (given in Chapters 6−7).

Remember the goal I stated for logic?

Secret

But I still don't get the criteria for valid here. I am guessing the program will terminate with an error if "Goat(x) ⇒ Animal(x)" is false?

user21820

Just forget it. I think the conventional notions of arguments are not suitable for either of you two.

It's better if you just look at the mechanical rules.

The goal is to convince yourself that those rules will ensure what I said was the goal in logic:

> That every sentence written is true in its context.

Why is that important? It means that any sentence that we can write without any context is then unconditionally true, and we call such sentences that we can write as a theorem.

Secret

11:46

Context(Cow(x))=real world
Context(Animal(x))=real world
?

user21820

No just forget about that example.

Let's just focus on the goal I stated.

LastIronStar

@user21820 by packaging the conditioning into the sentence, we can make an argument a theorem right?

user21820

@LastIronStar Yes if it is a valid argument (my validity).

LastIronStar

ok, consider this example:

Secret

1. Socrates is a man.
2. All men are carrots.
So: Therefore, Socrates is a carrot.

Context(Socrates is a man.)=Socrates the philosopher?
Context(carrots) = carrots as a vegetable in real life?

Context(So: Therefore, Socrates is a carrot.)=the truth value of that sentence in real life???

user21820

11:51

That example is a valid argument. But seriously I think there's little point in talking about English examples now. Both of you are (understandably) getting confused by the interpretation of them in the real world.

LastIronStar

If A and NOT(B):
    B.

user21820

Invalid.

Any more you want to ask?

LastIronStar

ok

yes

Secret

english words has too much context. Lastironstar did better than me, but for me since I take no assumptions, I permutate all possibel contexts I can think of, thus the truth value will have many possibilities. This is why I get really confused because I am seeing mental tree diagrams and not a clear path

user21820

After you both finish asking, let me start from scratch in explaining logic. I will at some later point invoke your understanding of the programs I gave earlier. But I will not use anything from forallx.

Secret

11:52

ok

LastIronStar

sounds good

Secret

(please don't make my poor brain to generate tree diagrams...)

LastIronStar

Suppose the following is a valid argument:

If A:
    B.

What can we say about the following one:

If A and NOT(B):
    B.

user21820

Valid as well.

Not so easy to explain that now.

LastIronStar

@user21820 this is what I've been trying to say the whole week approximately!!!

user21820

11:55

Yes, but previously you kept saying that the latter doesn't seem valid.

Secret

My question is more subtle:
P is the following program:
If A:
B.

what is the criteria for P to be valid in terms of A, B. Or rather, what exactly do we mean by context of A, B?

LastIronStar

what latter?

user21820

@LastIronStar If you read your initial question to me, you disagreed with me that even if the following is valid:

If A and B and C:
  D.

The following seemed invalid (to you):

If A and B and C and not D:
  D.

LastIronStar

wow, i can see how my understanding has shifted now! Pretty cool. Thanks for all the persistence @user21820! I have no more questions for now :)

user21820

Oh that's great.

So let me start on the actual logic.

LastIronStar

12:01

shouldn't we wait for @Secret to confirm as well?

user21820

Sure.

LastIronStar

@Secret there?

user21820

@LastIronStar That's always the problem with online chat. There is no social convention to help us determine whether the other party is actually there right now or has been interrupted by something else. And similarly whether a message has been read. Lol. I guess @Secret is away from his computer.

=P

LastIronStar

@user21820 Yes a new twist to the old Byzantine Generals' Problem

I guess we can start, @Secret will surely catch up i feel.

user21820

Alright we shall build a Fitch-style system that satisfies the following goal:

21 mins ago, by user21820

> That every sentence written is true in its context.

Rules shall govern what we can write.

Every rule is of the form:

| ...
|-----
| ...

Which means that if in any context you can write what is above, then you can write what is below within the same context.

Okay?

We shall only write what the rules allow.

At first we start with no rules, so we cannot write anything.

Check that our goal is trivially satisfied.

We shall add rules one by one, each time ensuring that our goal is still achieved.

LastIronStar

12:11

is the rule = argument?

user21820

No.

Let me introduce the first rule, called Repeat:

| A
|---
| A

LastIronStar

what is the context here?

user21820

We haven't specified any rules for creating contexts, so currently we can only write in the outermost context.

Secret

@LastIronStar just back from bath, and I don't think I can said anything about what I think of the above program now, cause my mind is still tree diagraming into confusion. Hopefully after user21820 went through the logic 101 (as he is doing now), I will have a better understanding and my brain no longer generate tree diagrams

LastIronStar

"Which means that if in any context you can write what is above, then you can write what is below within the same context" - here you use context to define rules, doesn't requiring rules to define/create contexts later on then become circular? @user21820

Leaky Nun

12:15

you can indent whenever you want

you don't need rules to create contexts

user21820

@LeakyNun Actually, you do, but most people don't say so explicitly.

I was going to make it explicit.

Secret

@user21820 I am not sure if I understood this line correctly: So you mean something is a rule when given ... in context A, the ... after the --- is written in context A?

user21820

Here is that rule, which we can call if-sub (for conditional-subcontext):

@Secret Yes.

Just a moment once we have the second rule then we can see actual examples.

LastIronStar

@LeakyNun Hi!

Leaky Nun

hi

Secret

12:18

I am fine with abstract examples for now, cause they are semantics free enough to prevent my brain from tree diagraming into BSOD

user21820

@LastIronStar You are half-right. It sounds circular, but contexts are defined according to the indentation, but I haven't permitted you to write the context headers so you cannot even create them yet.

Here is that subcontext-creation rule, which we can call if-sub (for conditional-subcontext):

|
|-------
|If A:
|  A.

LastIronStar

@user21820 I don't understand this, maybe it's a first pass issue, so i will wait for now giving the benefit of the doubt.

user21820

It says that you do not have to have written anything but you can write a context header and then inside that subcontext you can restate that thing in the header.

Leaky Nun

@user21820 (unrelated) can you prove the infinitude of primes within first-order PA?

user21820

@LeakyNun Yes.

Leaky Nun

12:20

how?

user21820

Wait.

Leaky Nun

ok

user21820

Here is an example proof that we now can write.

If A:
  A.
  If B:
    B.
    B.
  A.
  A.
  A.

Not very interesting, is it?

Leaky Nun

I hope the proof doesn't involve encoding lists of primes within an integer

user21820

@LeakyNun No it doesn't.

LastIronStar

12:22

@user21820 :@

why are same assertions being repeated!?

Secret

The context header is the ---, and the
|If A:
| A.

creates the subcontext known as A?

Leaky Nun

@LastIronStar because there's no other possibilities

we only have the repeat rule for now

user21820

@Secret No. the context header is "If A:".

LastIronStar

can you write it in rule format?

Secret

|
|-------
|If A:
| A.

every line is within the same context, and then the line | A. is part of the subcontext |If A: ?

user21820

12:24

No the "|−" shape is just to separate the above from below.

The line on the left is just part of that shape. No other significance.

If you want in plain English:

> Repeat: If you have written "A" in any context, you can write "A" again in that context.

> If-sub: In any context, you can write "If A:" and it creates a subcontext within which you can write "A.".

@Secret @LastIronStar: Do you get what these two rules so far have allowed us to do? The example should make it clear:

6 mins ago, by user21820

If A:
  A.
  If B:
    B.
    B.
  A.
  A.
  A.

LastIronStar

what is the outermost context?

also what does leaving the space above ---- in a rule mean?

Secret

So, line by line (stuff to the right of |)
1st line: Any context
2nd line: (separator)
3rd line: Any context
4th line: Subcontext created by 3rd line?

LastIronStar

wait so 1st line is a context or an assertion true in some context(defined before it)?

user21820

No the 3rd line literally says you can write the string "If A:".

22 mins ago, by user21820

Which means that if in any context you can write what is above, then you can write what is below within the same context.

LastIronStar

ok, so these are assertions

Secret

12:32

@user21820 No I mean I am trying to understand where each line is within which context in the if-sub example

user21820

@LeakyNun: Do you have another way of explaining this? I don't know why they don't get it.

LastIronStar

@user21820 ROFL

Leaky Nun

@user21820 eh

user21820

Basically, a proof is a specific format. Just like a program, which you both know.

The compiler requires that you write in a certain format, otherwise it will spit it out and throw compile-error.

That kind of format is precisely what we are going to define.

LastIronStar

I get that, my question is more conceptual than syntactical

user21820

12:33

In a program, you can create if-structures, right?

LastIronStar

yes

user21820

You can also write statements.

It's exactly the same thing here.

LastIronStar

so suppose I write:
| A
|-----
|B

user21820

You can't write that.

LastIronStar

oh

user21820

12:35

I'm using a diagram to represent a rule. The diagram is not what you can write in a proof.

The diagram merely attempts to convey the rule.

Leaky Nun

@user21820 meanwhile I'm doing proofs in real proof-languages

user21820

Lol.

Leaky Nun

by proof-language I mean a programming language that is designed for writing proofs

and you're still explaining how proofs require a certain format

while I'm worrying about the fact that I used dne twice

user21820

Very funny.

Leaky Nun

so, no I don't know how to explain it

Secret

12:36

@All I don't know what my questions belong, it seems I am reading all of these very differently from what you, Leaky and Lastironstar did. Basically, you give me the notion of any rule:

| ...
|-----
| ...

where | is part of the shape, and --- is a separator. Here if we have any context U, then the 1st and 3rd line are within U.

Now I want to understand:

|
|-------
|If A:
| A.

Is the 1st line within U, 3rd line within U, 4th line within the subcontext A?

user21820

Yes.

And the second rule says that within U you can literally write "If A:".

Secret

ok

user21820

If you don't have this rule, then you can't even create subcontexts.

Does it make sense now?

Secret

so far ok

LastIronStar

what does a blank in the rule mean?

user21820

12:38

It means "nothing required to have been written before".

LastIronStar

Are all rules in some context?

Secret

Currently reading this, and I need to be afk for roughyl 10 mins after this message, will catch up afterwards:

If A:
A.
If B:
B.
B.
A.
A.
A.

user21820

@LastIronStar All rules will apply in any context.

That is why in my silly example you could repeat the "B" inside.

Got it so far?

LastIronStar

basically rule is a way to reason about sentences without worrying about the context. Is that characterisation correct?

user21820

Yes it will indeed be the case for all the rules I will introduce.

Leaky Nun

12:45

@user21820 I think we should have separate words for things assumed a priori and sentences in a theory

LastIronStar

what does a null sentence (ie., a blank) in a rule mean now?

for example:
|
|----
| A

user21820

@LastIronStar The rule means that if you have written what's on top then you can write what's below. Your rule will not be good because it basically says you can write anything you like.

LastIronStar

I see blank doesn't mean null sentence, it means for any sentence, is that correct?

user21820

(If the top is blank it means that you don't have to have written anything.)

Leaky Nun

oh btw @user21820 I'm proving that the class of all singletons exists (in nbg)

the consturction is firstly the class of (a,(b,c)) such that a in c and b in c

user21820

12:49

@LeakyNun That's trivial, isn't it.

Leaky Nun

that is by intersecting [(a,(b,c)) where a in c] and [(a,(b,c)) where b in c]

the former is created by converse comprehension which makes it the same as the latter

the latter is U cross mem

then I construct the class of (a,(b,c)) where a is not equal to b

user21820

Let Singletons = { x : set(x) ∧ ∃y∈x ∀z∈x ( y=z ) }. What's wrong with my construction?

Leaky Nun

@user21820 nbg

with the finitely many comprehension axioms

not the schema

user21820

That's not practical. Why do that?

Leaky Nun

because it's finite :P

and because it's fun

user21820

12:51

@DavidReed will like you.

Leaky Nun

I was on a plane for 12 hours

I planned it beforehand

user21820

I see.

@LastIronStar @Secret: Shall I continue?

Here is another rule:

Secret

(I am still afking. Dealign with some old photos from mum in the bg)

LastIronStar

6 mins ago, by LastIronStar

I see blank doesn't mean null sentence, it means for any sentence, is that correct?

user21820

7 mins ago, by user21820

(If the top is blank it means that you don't have to have written anything.)

Okay let's be extremely precise.

LastIronStar

12:55

yes, that should help

user21820

The rule means that, if you have written every single line above the --- in that order in the current context, then you can write any line below the --- in the current context. In particular, if there is no line above the ---, then you vacuously can write any line below the --- in the current context.

Better now?

LastIronStar

yes!

user21820

Okay here is the next rule, which I call If-Repeat.

|A.
|If B:
|-------
|  A.

It's ambiguous, but it's supposed to mean that you are allowed to repeat the "A" inside the "If B:" subcontext if you have already written it outside.

LastIronStar

| A.
|-------
| If B:
|    A.

Shouldn't it be this then?

user21820

You can think of it that way too, but the problem is that it is not clear whether you are forcing the user of that rule to write "If B:".

Whereas in my version I require the user to already have written "If B:", allowed by the earlier rule.

It doesn't matter how you think of it.

Just make sure you understand what the rule means when actually writing a proof obeying it.

Example:

If A:
	A.
	If B:
		B.
		A.
		B.
	If not B:
		not B.
	If not A:
		not A.
		A.

LastIronStar

13:06

I think what you are saying is that since our rule has the convention that means: if all sentences in the top are true, then each sentence in the bottom is true, they way you wrote it is right

user21820

That is more or less the idea, which is called soundness of the rule.

(true in its context).

LastIronStar

you still haven't defined what a context is btw

user21820

Each context-header, currently including those of the form "If A:", creates a subcontext within the one it is in.

LastIronStar

@user21820 this seems to me to be valid argument/proof

user21820

Good.

Leaky Nun

13:09

Emperor Palpatine "Good" Compliation

►

LastIronStar

given an outer context, you are able to create an inner context - but you have conveniently not told what is an(the?) outermost context!

user21820

@LastIronStar I was going to get to soundness later, but since you already got there, great! Basically, to ensure that we achieve our ultimate goal, it suffices to ensure that every rule we have is sound, namely if every sentence we wrote so far is true in its context then every sentence that the rule permits us to write is true in its context.

LastIronStar

@LeakyNun haha

user21820

@LastIronStar The entire proof is in the outermost context, which you can imagine has no assumptions whatsoever, but really it does not matter.

See, the proof is going to obey our goal even if the outermost context is the sun's interior, or the moon's surface.

@LeakyNun If you keep distracting apprentices and swaying them away from the logic side then I may have to exile you (until you turn back to logic).

Leaky Nun

@user21820 :o

user21820

13:12

Just kidding.

Leaky Nun

:D

user21820

@LastIronStar: So, convinced that our 3 rules so far are sound?

LastIronStar

@user21820 if it has no assumptions, how do i decide upon if a rule is useful at all?!

basically, is it AN outermost context or THE outermost context?

user21820

Um does not matter? Like you noticed previously, the rules are there to allow us to reason within any context without caring about the context.

Leaky Nun

@user21820 sometimes I do things related to ordinals, the theory tells me that my task will be done in finitely many steps, but also my heart is telling me "you're relying on the consistency of ZFC" (in particular the axiom of foundation being true)

if that axiom were somehow false, I would not be able to finish my task

user21820

13:15

@LeakyNun That is why I don't play with over-large ordinals at work.

Leaky Nun

@user21820 but it works out every time :P

so ZFC is still consistent

LastIronStar

@user21820 yes but what's the point of it all if not even one rule's upper statement is true!

user21820

@LastIronStar I'm not sure I understand the question here. It's because we haven't added more rules to allow us to deduce theorems.

LastIronStar

@user21820 Ok let me put it this way: If there is more than one outermost context, how do I know which one to use?

user21820

@LastIronStar The point is that you can see that the rules are sound (regardless of the context you use them in). Hence the proofs will be valid (satisfy the goal) regardless of the context you write them in!

LastIronStar

13:19

at the end of the day, your outermost context would behave like axioms of a system and you want to be able to establish them as equivalent to, say, an alternative axiomatic system

Leaky Nun

@user21820 and then my mind is telling me to trust the force (the logic)

user21820

@LastIronStar Wait don't jump before you can stand. We are not going to talk about axioms or alternative systems yet!

LastIronStar

@user21820 ok fair point but i think this question remains: how to determine if a rule is sound?

user21820

Which of the rules so far do you doubt its soundness?

10 mins ago, by user21820

@LastIronStar I was going to get to soundness later, but since you already got there, great! Basically, to ensure that we achieve our ultimate goal, it suffices to ensure that every rule we have is sound, namely if every sentence we wrote so far is true in its context then every sentence that the rule permits us to write is true in its context.

I hope you can see that Repeat is obviously sound.

LastIronStar

oh wow, this is more constructivist than i would have imagined. nice..

user21820

13:22

The two Restate rules are also sound by the intended meaning of contexts, exactly like in the program interpretation.

So on to the next rule:

|If A:
|  B.
|-------
|A⇒B.

Finally, we have a way of 'escaping' subcontexts. But it's actually not much. What is the meaning of "A⇒B"? Well, it means that "if A is true then B is true".

Can you see why this rule is sound?

I got to go for quite a while. Back later.

LastIronStar

ok

let me think a bit on this

just ping me whenever you're free again

what i'm afraid of is that there is no clear way for users to agree on what the outermost context is! This may lead to a lot of confusion na

Transcript for

♦ $Mathematics$ Logic

Transcript for

♦ Logic

♦ $Mathematics$ Logic