Logic - 2018-12-24

10:53 AM

@user525966: So now that you roughly get the idea of variables, are you going to try the logic exercises you haven't done, or do you want simple exercises in PA instead?

user525966

3:58 PM

I mean I still don't get it at all in terms of when we can't use certain variable labels

user21820

4:19 PM

@user525966 What exactly do you not get? I don't see what's unclear about "fresh variable", and as I showed you earlier the used variables are just exactly those declared by a containing ∀-subcontext or in a previous ∃-elim step. If you're unclear about something, you should provide an example.

user525966

Nov 5 at 18:56, by user21820

If ￢∀x∈S (P(x)):
    If ￢∃x∈S (￢P(x)):
        Given y∈S:
            If ￢P(y):
                ∃x∈S (￢P(x)). // Exists-Intro since x is unused.
                ￢∃x∈S (￢P(x)). // Restate since y does not occur in it.
            P(y).
        ∀y∈S (P(y)).
        ∀x∈S (P(x)). // Rename
        ￢∀x∈S (P(x)). // Restate
        Contradiction.
    ∃x∈S (￢P(x)).
￢∀x∈S (P(x)) → ∃x∈S (￢P(x)).

Like we're using x, then we switch to y, then for some reason back to x again, I can't follow it

user21820

4:58 PM

@user525966 If you use "Given x∈S:", then you are not allowed to pull in "￢∃x∈S (￢P(x))" from outside, because the variables would conflict.

You can see the ∀-restate rule gives that very condition. Any system will necessarily have a similar kind of restriction (including in Hilbert-style).

@user525966: So that's why we use a different variable "y". Later, the ∀-intro rule only gets us "∀y∈S (P(y)).", which we then use the variable renaming rule to change the variable name back.

user525966

hmm

user21820

Here's an alternative:

If ￢∀x∈S (P(x)):
    If ￢∃x∈S (￢P(x)):
        ￢∃y∈S (￢P(y)). // Rename
        Given x∈S:
            If ￢P(x):
                ∃y∈S (￢P(y)). // Exists-Intro since x is unused.
                ￢∃y∈S (￢P(y)). // Restate since y does not occur in it.
            P(y).
        ∀x∈S (P(x)).
        ￢∀x∈S (P(x)). // Restate
        Contradiction.
    ∃x∈S (￢P(x)).
￢∀x∈S (P(x)) → ∃x∈S (￢P(x)).

@KarlKronenfeld: Hello and welcome! Interested in logic?

user525966

5:24 PM

yeah this is too abstract for me

I can't see the intuition or relationships between any of these rules here

it all feels arbitrary and hard to get a wrap on

propositional logic is a lot easier to see what's going on but I feel like here there are all sorts of little conditions and rules spanning across all these different things and I can't make heads or tails of it

user21820

@user525966 First-order logic is of course harder than propositional logic. The only way to learn how to use it is to use it.

user525966

Already tried using it

Stuff was still wrong so that brings one back to trying to understand the rules again

vicious circle

user21820

@user525966 When I said "use it" I meant to try. Only if you make mistakes is it possible for me to identify what you don't understand.

It's just like programming. You cannot learn it by reading the C++ standard.

user525966

that example up above

I don't understand when we need a new variable vs. when we're using what vs. when we're suddenly switching back

seems super random to me

user21820

5:40 PM

The first thing is to understand this:

41 mins ago, by user21820

@user525966 If you use "Given x∈S:", then you are not allowed to pull in "￢∃x∈S (￢P(x))" from outside, because the variables would conflict.

It's simply forbidden by the rules. So to get what you want you have no choice but to use a different variable.

You must separately grasp the rules and the reasons for them.

user525966

I don't understand that second part

Why that specific thing?

What aren't we allowed to pull in from the outside / why?

Why would we even be allowed to re-use a label twice? A lot of programming languages wouldn't even permit that

If I make a new x that's already used it's going to either override it like Python and do funny shit, or yell at me like C++ and go hey, dude you've already got an x, rename it

user21820

@user525966 They do permit that! Python has lambda expressions. C/Java allows you to reuse variables that go out of scope.

Sorry I see an accidental mistake in the above alternative. It should be:

If ￢∀x∈S (P(x)):
    If ￢∃x∈S (￢P(x)):
        ￢∃y∈S (￢P(y)). // Rename
        Given x∈S:
            If ￢P(x):
                ∃y∈S (￢P(y)). // Exists-Intro since x is unused.
                ￢∃y∈S (￢P(y)). // Restate since y does not occur in it.
            P(x).
        ∀x∈S (P(x)).
        ￢∀x∈S (P(x)). // Restate
        Contradiction.
    ∃x∈S (￢P(x)).
￢∀x∈S (P(x)) → ∃x∈S (￢P(x)).

You're going to have to stick with it and work through it until you understand. Please read the ∀-restate rule to see why the following is not permitted:

If ￢∀x∈S (P(x)):
    If ￢∃x∈S (￢P(x)):
        Given x∈S:
            If ￢P(x):
                ∃x∈S (￢P(x)).
                ￢∃x∈S (￢P(x)). // This is invalid.
            P(x).
        ∀x∈S (P(x)).
        ￢∀x∈S (P(x)).
        Contradiction.
    ∃x∈S (￢P(x)).
￢∀x∈S (P(x)) → ∃x∈S (￢P(x)).

user525966

I don't see why not

We have "∃x∈S (￢P(x))" as one of our assumptions

and one of the propositional logic rules was that any assumption we make can be restated (as long as we're still in that context)

user21820

@user525966 Think carefully. x is already declared in "Given x∈S:", so it is not clear what the "x" in "P(x)" is supposed to refer to!

It could be the "x" in "∃x∈S"...

user525966

But we're allowed to say "￢P(x)" and "∃x∈S (￢P(x))"?

Why are the x's here somehow not ambiguous but it is in "￢∃x∈S (￢P(x))"?

user21820

5:50 PM

@user525966 The "￢P(x)" is okay, but the "∃x∈S (￢P(x))." is also invalid.

I wasn't focusing on that one so I missed it.

user525966

Maybe it's easier if we go through it stepwise so I can see your reasoning at each step

We wish to prove:

￢∀x∈S (P(x)) → ∃x∈S (￢P(x))

So this implies a proof of the form:

If ￢∀x∈S (P(x)):
    ...
    ∃x∈S (￢P(x)).

￢∀x∈S (P(x)) → ∃x∈S (￢P(x))

Correct so far?

user21820

You missed an ∃, but it's correct.

And the problem is that you cannot prove the existential directly because you simply have no object at hand. So you have to use a "contradiction" proof.

user525966

copy/paste error, should be fixed

if I look at exists-intro it says I need E in S, and then some P(E), from which I can declare that there exists an x in S such that P(x)

user21820

@user525966 Yes so (you can guess that) you can't use exists-intro to get the goal directly.

user525966

Why can't I use that to mean "declare some x in S, and then deduce not P(x)"?

user21820

6:00 PM

@user525966 How can you declare an object that you don't even know exists??

And even if you know S is not empty, the object you randomly pick may satisfy P.

user525966

Is "￢∀x∈S (P(x))" not in some way giving me some variable to work with?

this line in some way is introducing x, S, and P(x), what am I allowed/not allowed to do with them?

user21820

@user525966 No, as we discussed earlier:

yesterday, by user21820

Inside the first If-subcontext, x,y are already not fresh, but still unused.

That was for a different example, but it's the same thing.

user525966

I guess I don't see why they're "unused"

Like to me even if I declare int a = 5 to me that's still "using" it

maybe the word is not applying here the same way

user21820

It's because you keep confusing quantified variables and declared variables...

Even in natural language...

> For every student S there is a person T who taught S.

> For every student x there is a person y who taught x.

They mean exactly the same.

So "If ∀x∈S ( ... )" does not make "x" have any particular meaning outside that quantified statement.

Because "If ∀x∈S ( P(x) ):" and "If ∀y∈S ( P(y) ):" would both create the same subcontext, in which "every member of S satisfies P".

And we even discussed this before. See how it can be somewhat captured in programming:

Oct 21 at 3:51, by user21820

def Q():
    for x in S:
        if not x<4: return false;
    return true;
if Q():
    for y in S:
        assert y<4;

user525966

so if-statements, for-all statements, exist statements, etc, are not actually using the variables in any way

just using the "label" to establish the relationship

user21820

6:10 PM

Yes, that's why some people also call them dummy variables.

user525966

and then that label becomes off-limits for when we want to actually declare a variable?

user21820

Yes. When you declare a variable, from that point onwards it has a fixed meaning and you can't use it as a dummy variable anymore.

user525966

Like I would never in Python do something like:

for x in S:
    x = 5 # why even bother iterating S?

user21820

Yes.

user525966

k = 100

for k in range(10):
    print(k)  # 0 thru 9

print(k) # 9

user21820

6:13 PM

That too. Though the C++ version more clearly matches the intent behind my rules:

int k = 100;
for(int k=0;k<10;k++) print(k); // invalid

And:

for(int k=0;k<10;k++) print(k);
print(k); // invalid

(Assuming you have a print function.)

I got to go now; please leave your questions here.

user525966

9:29 PM

Okay I am going to try the proof from scratch using that idea in mind

We begin at:

If ￢∀x∈S (P(x)):
    ...
    ∃x∈S (￢P(x)).

￢∀x∈S (P(x)) → ∃x∈S (￢P(x))

As you mentioned earlier we don't have a variable yet so we should try a proof by contradiction:

If ￢∀x∈S (P(x)):
    if ￢∃x∈S (￢P(x)):
        ...
    ∃x∈S (￢P(x)).

￢∀x∈S (P(x)) → ∃x∈S (￢P(x))

To get a contradiction inside that context we'll need to contradict that first if-statement most likely

but I'm not sure what a negation of that looks like

Like what does it mean to contradict "￢∀x∈S (P(x))"

I can't tell if the not is applying to the whole statement or just the for-all or what

maybe this is where the long form helps?

￢∀x, x∈S implies P(x) maybe

maybe the negation is only applied within a quantifier?

￢∀x, x∈S and ￢P(x)

Or maybe it's applying to the whole thing and I'm overthinking it

i.e. if the first if statement is the same as ￢(∀x∈S (P(x)))

Then the thing we want to deduce is ∀x∈S (P(x)) to contradict it?

fuck it let's just try it

If ￢∀x∈S (P(x)):
    if ￢∃x∈S (￢P(x)):
        ....
        ∀x∈S (P(x))  // contradiction with first if-statement
    ∃x∈S (￢P(x)).

￢∀x∈S (P(x)) → ∃x∈S (￢P(x))

okay so to get a for-all intro I just have to show that something holds for an arbitrary value

But here is where I may not be able to say given x∈S because x is used?

so...

If ￢∀x∈S (P(x)):
    if ￢∃x∈S (￢P(x)):
        Given y∈S:
            ...
            P(y)
        ∀x∈S (P(x))  // contradiction with first if-statement
    ∃x∈S (￢P(x)).

￢∀x∈S (P(x)) → ∃x∈S (￢P(x))

I'm not sure if I can jump straight from the given-using-y context to the for-all-using-x statement though

can we do this?

If ￢∀x∈S (P(x)):
    if ￢∃x∈S (￢P(x)):
        Given y∈S:
            ...
            P(y)
        // ∀y∈S (P(y)) // ????
        ∀x∈S (P(x))  // contradiction with first if-statement
    ∃x∈S (￢P(x)).

￢∀x∈S (P(x)) → ∃x∈S (￢P(x))

whatever moving on

To get P(y) out there by itself I don't have a good way to disconnect it from any previous statement using intro-elim so I'll try a proof by contradiction again

If ￢∀x∈S (P(x)):
    if ￢∃x∈S (￢P(x)):
        Given y∈S:
            If ￢P(y):
                ...
            P(y)
        // ∀y∈S (P(y)) // ????
        ∀x∈S (P(x))  // contradiction with first if-statement
    ∃x∈S (￢P(x)).

￢∀x∈S (P(x)) → ∃x∈S (￢P(x))

hmm

well I can't contradict by pulling in a P(y) or something, that's the very thing I'm trying to show eventually, so I'll need to find some other contradiction to make from assuming ￢P(y)

I guess I could say:

If ￢∀x∈S (P(x)):
    if ￢∃x∈S (￢P(x)):
        Given y∈S:
            If ￢P(y):
                ∃y∈S (￢P(y))
                ...
            P(y)
        // ∀y∈S (P(y)) // ????
        ∀x∈S (P(x))  // contradiction with first if-statement
    ∃x∈S (￢P(x)).

￢∀x∈S (P(x)) → ∃x∈S (￢P(x))

Just by combining the given-y and the if-not py thing

maybe I can get my contradiction between that and the second if-statement?

If ￢∀x∈S (P(x)):
    if ￢∃x∈S (￢P(x)):
        Given y∈S:
            If ￢P(y):
                ∃y∈S (￢P(y)) // contradiction with second if-statement???
            P(y)
        // ∀y∈S (P(y)) // ????
        ∀x∈S (P(x))  // contradiction with first if-statement
    ∃x∈S (￢P(x)).

￢∀x∈S (P(x)) → ∃x∈S (￢P(x))

not sure if that works

Transcript for

♦ $Mathematics$ Logic

Transcript for

♦ Logic

♦ $Mathematics$ Logic