Logic - 2019-02-20

user400188

01:38

Are not the two c's in the second and third subproofs different? They have the same label in what you have written, however I think at least one should be labeled differently.

Please correct me if I'm mistaken.

In the third subproof, I think c needs to be a fresh constant, since it came from an existential quantifier.

user21820

02:59

@user525966 Sorry I was real busy these last few days. I'll check your attempt and show you my own proof. You are right in observing that sometimes you cannot just directly show existence via exists-intro. This is the nature of classical logic. Sometimes you can only show existence by contradiction. Is this surprising?

Give me a moment.

user525966

Also trying the equality one: (jumping ahead a bit / just posting it here in case I forget later)

Given a ∈ S:
    Given b ∈ S:
        Given c ∈ S:
            If a = b ∧ b = c:
                a = b   [∧ elim]
                b = b   [= intro]
                b = a   [= elim]
                b = c   [∧ elim]
                a = c   [= elim]
            a = b ∧ b = c → a = c       [→ intro]
        ∀z ∈ S (a = b ∧ b = z → a = z)  [∀ intro]
    ∀y, z ∈ S (a = y ∧ y = z → a = z)   [∀ intro]
∀x, y, z ∈ S (x = y ∧ y = z → x = z)    [∀ intro]

user21820

@user400188 I'm not sure what "what [I] have written" is referring to. You are right that the variable used to witness an existential has to be fresh (the ∃elim rule has the condition that y must be a fresh variable). So you have to use different variables because if you use c for the first one then it is no longer fresh when you want to witness the second one. (I'll fix it for you then you'll see.)

Ah I see your problem. I just read to the point where you want to use or-elim, so you want to use the same constant. But that's not possible. The solution is to 'forget' the constant by using exists-intro inside each case.

@user525966 Give me a while to type out the fixed version based on your attempt, which is more or less one way to prove it.

user525966

If ∃x ∈ S (x ∈ S):
    ∀y ∈ S P(y) ∨ ￢∀y ∈ S P(y)

    If ∀y ∈ S P(y):
        Let c be a constant such that P(c)
        P(c)
        P(c) → ∀y ∈ S P(y)
        ∃x ∈ S (P(x) → ∀y ∈ S P(y))

    If ￢∀y ∈ S P(y):
        ∃y ∈ S ￢P(y)
        Let d be a constant such that ￢P(d)
        ￢P(d)
        If P(d):
            ⊥
            ∀y ∈ S P(y)
        P(d) → ∀y ∈ S P(y)
        ∃x ∈ S (P(x) → ∀y ∈ S P(y))

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

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

^something like this?

user21820

If ∃x∈S ( x∈S ):
	Let c∈S such that c∈S.
	∀y∈S ( P(y) ) ∨ ¬∀y∈S ( P(y) ).  [by LEM, previously proven]
	If ∀y∈S ( P(y) ):
		If P(c):
			∀y∈S ( P(y) ).
		P(c) ⇒ ∀y∈S ( P(y) ).
		∃x∈S ( P(x) ⇒ ∀y∈S ( P(y) ) ).
	If ¬∀y∈S ( P(y) ):
		∃y∈S ( ¬P(y) ).  [by previously proven theorem]
		Let d∈S such that ¬P(d).
		If P(d):
			¬P(d).
			Contradiction.
			∀y∈S ( P(y) ).  [by explosion, previously proven]
		P(d) ⇒ ∀y∈S ( P(y) ).
		∃x∈S ( P(x) ⇒ ∀y∈S ( P(y) ) ).
	∃x∈S ( P(x) ⇒ ∀y∈S ( P(y) ) ).

@user525966 Yes but I'm not sure why you modified the first case. The original was correct except you had a superfluous "P(c)".

user525966

03:15

was trying to be more explicit i suppose

user21820

No in your last attempt it the first case became incorrect.

user525966

Why incorrect?

user21820

Because "P(c) → ∀y ∈ S P(y)" isn't justified.

user525966

If ∃x ∈ S (x = x):
    ∀y ∈ S P(y) ∨ ￢∀y ∈ S P(y)

    If ∀y ∈ S P(y):
        Let c ∈ S such that c = c
        If P(c):
            ∀y ∈ S P(y)
        P(c) → ∀y ∈ S P(y)
        ∃x ∈ S (P(x) → ∀y ∈ S P(y))

    If ￢∀y ∈ S P(y):
        ∃y ∈ S ￢P(y)
        Let d be a constant such that ￢P(d)
        ￢P(d)
        If P(d):
            ⊥
            ∀y ∈ S P(y)
        P(d) → ∀y ∈ S P(y)
        ∃x ∈ S (P(x) → ∀y ∈ S P(y))

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

user21820

@user525966 Yes now it's almost correct. The only thing you missed is that you didn't apply the exists-elim rule correctly (compare with mine), and hence also there was an error with the exists-intro rule.

The distinction is important, and note that the rules ensure that you cannot prove quantified statements over objects of the wrong type.

user525966

03:21

I don't follow, where didn't I apply exist-elim correctly?

user21820

@user525966 Don't you see a difference between yours and mine?

user525966

Just that I declared c inside the first subproof thing whereas you put it outside

user21820

Wait a minute; you edited your message.

user525966

maybe I had still been editing at the time

user21820

Earlier it merely said "Let c be a constant such that c∈S." and why did you change to "∃x ∈ S (x = x)"?

user525966

03:24

pretend the last line uses x=x instead, just switched it up for fun

user21820

Lol.

Anyway it's still incorrect; the second exists-elim is still wrong.

user525966

Let d ∈ S such that ￢P(d)

^instead?

user21820

Right!

Very important!

If you don't have "d∈S" you can't use exists-intro later to get "∃x∈S ( ... )".

Makes sense?

If you want to claim the existence of some member of S satisfying some property, you must of course start with a member of S.

user525966

I suppose the idea being that we have to match exactly the thing we're "sampling" from

to keep the domains straight and all that

ok final attempt:

If ∃x ∈ S (x = x):
    ∀y ∈ S P(y) ∨ ￢∀y ∈ S P(y)

    If ∀y ∈ S P(y):
        Let c ∈ S such that c = c
        If P(c):
            ∀y ∈ S P(y)
        P(c) → ∀y ∈ S P(y)
        ∃x ∈ S (P(x) → ∀y ∈ S P(y))

    If ￢∀y ∈ S P(y):
        ∃y ∈ S ￢P(y)
        Let d ∈ S such that ￢P(d)
        ￢P(d)
        If P(d):
            ⊥
            ∀y ∈ S P(y)
        P(d) → ∀y ∈ S P(y)
        ∃x ∈ S (P(x) → ∀y ∈ S P(y))

    ∃x ∈ S (P(x) → ∀y ∈ S P(y))
∃x ∈ S (x = x) → ∃x ∈ S (P(x) → ∀y ∈ S P(y))

user21820

@user525966 Yes, and it's just like programming in a strictly typed language like Java where your function declaration must have the correct type signature that matches the objects you want to pass in.

user525966

03:29

makes sense

user21820

@user525966 Correct. Now my turn. I'll give you a proof that doesn't rely on any previously proven theorem. Yours relies on three, but it's fine because in mathematics it's of course natural to rely on existing results. Just make sure you don't go in a circle. =)

user525966

Which three?

I know mine relies on ￢∀y ∈ S P(y) being equivalent to ∃y ∈ S ￢P(y)

unless you also mean LEM? (if we're counting that as something we're proving via given DNE as opposed to also given like proofmood's system)

user21820

@user525966 Sure, if you use ProofMood then LEM and explosion don't count, so you're right you only rely on one.

user525966

ah okay you're counting ex falso as well

in your system do you generally only assume DNE given?

(with LEM + ex falso derived?) can't recall

user400188

I was referring to @user525966 first proof.
Also, long time no see @user21820.

user21820

03:36

@user525966 Yes I thought you were using my system, because ProofMood doesn't have restricted quantifiers. I have no problem with you using LEM and EX as primitives. As long as you know you're using it, no problem!

If ∃x∈S ( x∈S ):
	If ¬∃x∈S ( P(x) ⇒ ∀y∈S ( P(y) ) ):
		If ∃x∈S ( ¬P(x) ):
			Let c∈S such that ¬P(c).
			If P(c):
				If ¬∀y∈S ( P(y) ):
					¬P(c).
					Contradiction.
				∀y∈S ( P(y) ).
			P(c) ⇒ ∀y∈S ( P(y) ).
			∃x∈S ( P(x) ⇒ ∀y∈S ( P(y) ) ).
			Contradiction.
		¬∃x∈S ( ¬P(x) ).
		Given y∈S:
			If ¬P(y):
				∃x∈S ( ¬P(x) ).
				Contradiction.
			P(y).
		∀y∈S ( P(y) ).
		Let d∈S such that d∈S.
		If P(d):
			∀y∈S ( P(y) ).
		P(d) ⇒ ∀y∈S ( P(y) ).
		∃x∈S ( P(x) ⇒ ∀y∈S ( P(y) ) ).
		Contradiction.

@user400188 Same to you!

user525966

I guess I don't quite get how like... if this were a program and I use c in the first subproof, I used d in the second one just to be safe but why couldn't I in theory use c since it isn't "conflicting" with the first one? (or is it, technically?)

user21820

@user525966 It's all a matter of design decisions. Programming languages face exactly the same decision, namely whether or not to allow you to use the same variable and overwrite the previous declaration. C/Java do not allow this. Javascript does.

user525966

But in Java I am able to do;

        public static void main (String[] args) throws java.lang.Exception
	{
		if (1 == 1) {  // arbitrary if statement
			int c = 4;
			System.out.println(c);
		}
		if (2 == 2) { // arbitrary if statement
			int c = 5;
			System.out.println(c);
		}
	}

user21820

Yes, programming languages allow you to re-assign variables, while the system I gave does not, but remember that exists-elim may give you an object of arbitrary type, so you can't use the same variable in general anyway even in programming.

If you attempt to remove this restriction, then you will have much more complicated other rules, such as the restate-rule. You can no longer just repeat a statement you deduced earlier!

Because now the symbols may have different meaning.

In my opinion, it's best to adopt the "fresh variable" approach, so that once a variable is declared it never changes meaning.

Until you 'exit' the context where it is declared.

user525966

Is there an easy example showing how this is a problem if we're allowed to re-use the same constant label even if totally different (i.e. not nested) subproofs?

user400188

03:41

Wait, I think you should still use fresh variables once you leave the context where it was first declared.

user525966

In my above proof I don't understand why I wouldn't be able to use c again in the second if statement, for instance

like the java code above

ahh nice proof for drinker's paradox, full-on contradiction proof

user21820

@user525966 Oh my initial objection was to your initial attempt where I thought you instantiated c before the first case. Sorry about that.

@user525966 That's a very good question, and I was just about to answer it, except that you got to the asking first haha.. Basically, once you leave the context where a variable was declared as witness, you can use it again. The rules I gave for my system are stricter, because it's harder to state the looser version.

user525966

oh if i had declared it outside then i would absolutely agree

java would throw a fit if i did that as well:

user21820

@user400188 This is exactly what my rules say. Note that if we want to loosen it, we can allow using variables that have been instantiated, but not variables that we have used with quantifiers in previous statements.

user400188

I'm missing the definition of a term here. What is meant by witness?

user525966

03:44

	public static void main (String[] args) throws java.lang.Exception
	{
		int c = 4;

                if (1 == 1) {
			System.out.println(c);
		}

		if (2 == 2) {
			int c = 5;
			System.out.println(c);
		}
	}

Main.java:19: error: variable c is already defined in method main(String[])

user21820

@user400188 Exists-elim allows you to say "Let c∈S such that ..." which gives you a witness c that satisfies ...

Also called instantiation of the exists-statement.

@user525966 Yup, so I guess you understand my comment about C/Java not allowing that thing, while Javascript doesn't care.

user525966

right

Python:

c = 4
if 1 == 1:
    print(c)  # 4

if 2 == 2:
    c = 5
    print(c)  # 5

print(c)  # 5

user400188

Just to clarify, when we write $\exists x\in X~P(x)$ or $\forall x\in X~P(x)$ are we using this as shorthand for $\exists x~(x\in X)\land(P(x))$ and $\forall x~(x\in X)\rightarrow(P(x))$ respectively?

user21820

Here's an example where using a previously quantified variable causes problems:

If ∃x∈S ∃y∈S ( x≠y ):
	Let y∈S such that ∃y∈S ( y≠y ).
	Let z∈S such that z≠z.
	z=z.
	Contradiction.

@user400188 No, in my system the restricted quantifies are not short-hand because there may not be a "∈" predicate-symbol. See the section "Peano Arithmetic" in my post, for example.

user525966

∃x∈S P(x) shorthand for ∃x(x∈S ^ P(x))
∀x∈S P(x) shorthand for ∀x(x∈S → P(x))

user21820

03:51

@user525966 I just said it's not.

Other people might go down that path, but it's not the right way of thinking anyway.

user400188

So when you write $\forall x\in X$, are you changing the domain of discourse?

user21820

@user400188 No, there is no 'domain of discourse' in the traditional sense. I suggest you read my post thoroughly. It is similar to what is called multi-sorted first-order logic, except that it's even better.

Types in my post correspond roughly to sorts in multi-sorted FOL.

user525966

How does this one look?

Given a ∈ S:
    Given b ∈ S:
        Given c ∈ S:
            If a = b ∧ b = c:
                a = b   [∧ elim]
                b = b   [= intro]
                b = a   [= elim]
                b = c   [∧ elim]
                a = c   [= elim]
            a = b ∧ b = c → a = c       [→ intro]
        ∀z ∈ S (a = b ∧ b = z → a = z)  [∀ intro]
    ∀y, z ∈ S (a = y ∧ y = z → a = z)   [∀ intro]
∀x, y, z ∈ S (x = y ∧ y = z → x = z)    [∀ intro]

user400188

Normally, I read statements like $\forall x\in X$ as having a domain of discourse (or universe), and a domain (which is a set).

By the way, if my memory serves me correct, you have several posts on Peano arithmetic. Which one can I find your definitions in?

user21820

@user400188 The one I just linked above (I edited the message to add the link).

user400188

03:56

Ah, thank you

user21820

In standard multi-sorted FOL, the sorts are fixed, and an interpretation must specify a domain for each sort. In my system, the types are not necessarily fixed. For example see the section "Set Theory" in that same post where I give rules that permit creating new types from sets.

In one-sorted FOL, you only have one domain, and so there is no need for restricted quantifiers. But then you can't have both PA and other stuff together...

@user525966 If you strictly follow the rules, the first =elim is incorrect. Check the rule carefully. =)

The purpose of that exercise was to see how the rules strictly work, but in practice you just do that theorem in one primitive step.

user525966

I didn't quite understand how the post defined it but I had used = elim in that way on proofs.openlogicproject.org which may define it differently

user21820

@user525966 In the post you must have "E=F" and "P(E)" before you can get "P(F)". You cannot use it if you have "F=E" and "P(E)".

user400188

Ok, I'll give your post another read afterward, but unfortunately I have to go now.

By the way, I'm still working on a back of the napkin problem I asked you about 2 to 3 months ago. I got to about 30 line in the proofmod site, then decided to start doing it by hand because it wont lag.

I'll finish it someday!

user21820

@user400188 Sure see you again. =)

user525966

04:06

what problem? @user400188

user400188

@user525966 I could list it here in the "export" format that proofmod creates. Although I haven't even written out all the axioms yet (just a few of them were sufficient to get to 30 lines and determine the truth value of half of the variables it uses.)

user525966

Oh I see, then I guess more like:

b = c (^ elim)
b = b (= intro)
c = b (= elim)
a = b (^ elim)
a = c (= elim)

or something?

user21820

@user525966 First 4 lines work. Last line doesn't. Wait you edited... Still doesn't.

But you're getting the idea. Namely you're first proving that = is symmetric. =)

user525966

a = b (^ elim)
a = a (= intro)
b = a (= elim on a = b and a = a)
b = c (^ elim)
a = c (= elim on b = a and b = c)

like this?

user21820

@user525966 Perfect!

Of course from now on, you can use equality as, you know, equality. =)

user525966

04:19

I just don't understand why it isn't sort of tossed in there as a given axiom or rule

reminds me of that hilbert thing where you have to derive p -> p in quite a roundabout way while some systems just give it to you as an extra axiom for convenience

i guess it's just to fit the notion of intro and elim

i admit I still don't understand the = elim rule lol

i just assumed it was
P(x) = P(y)
P(x) = P(x)
then
P(y) = P(x) by sort of taking the first part and using that to substitute in P(y) in the second part

I don't understand what "E = F, P(E), therefore P(F)" means

in particular because my final result is more of a P(E, F) type of thing

although I guess it is a P(F) just doesn't have any kind of restrictions unlike the P(E) requirement

user21820

@user525966 E,F are objects. P is a property, so P(E) is a statement about E. Search for "property" in my post to see its definition. If E=F and E satisfies some property, namely P(E) is true, then of course F also, namely P(F) is true.

user525966

Yeah / I get that P(E) is a property of E I just don't really get the difference

like what does E look like? What does P(E) look like?

user21820

P(E) is not a property of E.

P(E) is a statement.

user525966

because in both cases everything looks like (variable) = (some other variable) anyway

user21820

In your case, the first time you used P(x) ≡ (a=x).

user525966

04:26

property "function" perhaps

I think of it like, for instance is_blue(x)

user21820

You had a=b and P(a).

@user525966 That's a statement, not a property.

user525966

what's the property here?

is_blue?

(without any input header thing)

user21820

@user525966 Yes! Once you put an object 'into' a property, you get a statement.

That's why we talk about whether this or that object satisfies a property P. It is the same property, but P(E) may be true while P(F) is false.

user525966

is "is_blue" the property or is "blue" technically the property

I'm not quite sure what the difference is here

like talking about a quality something "has" vs. the function checking if it has that quality vs. the result of that function given some input

user21820

@user525966 That's up to you to define. I don't really want to talk about the English language. In logic you just define your properties or whatever the way you wish. Some people like calling the property of being blue "isblue". Personally I'll just use the adjective "blue" itself.

Those people think that "x is blue" translates to "isblue(x)".

That's a fair enough interpretation of the English statement. But English "is" has a much broader complicated function.

user525966

04:44

I think I am still missing something

Is there a less-trivial example of = elim being used?

user21820

@user525966 It's just used for substitution of an object for another that you've deduced to be equal. I'm not sure how non-trivial that can be.

But you can try the other exercise I gave you before regarding uniqueness. That's the canonical example of how equality works in logic.

Got to go now. See you later!

user525966

06:20

@user21820 Yeah I can't figure out Q6 at all lol

Unlike propositional logic it seems like working backwards often just doesn't work

Also not even sure I am reading it right, ∃x,y ∈ S (￢(x=y)) → ∀x ∈ S (∃y ∈ S (￢(x=y))) ?

Q5 being ∀x ∈ S (∀y ∈ S (Q(x,y) → P(x))) ↔ ∀x ∈ S ((∃y ∈ S Q(x,y)) → P(x)) ?

can't get that one either

(also, unrelated but I think Q4 may be typoed)

user21820

@user525966 Yea there are some typos. Let me repost a fixed version of those exercises.

Well that's the only typo in that list, but I guess I'll just post it again.

In these exercises, S is a type, and P is a property, and Q is a 2-parameter property (i.e. "Q(x,y)" is a statement about "x" and "y").
(Q1) not forall x in S ( P(x) ) implies exists x in S ( not P(x) ).
(Q2) not exists x in S ( P(x) ) implies forall x in S ( not P(x) ).
(Q3) exists x in S ( x in S ) implies exists x in S ( P(x) implies forall y in S ( P(y) ) ).
(Q4) forall x,y,z in S ( x=z and y=z implies x=z ).
(Q5) forall x in S ( forall y in S ( Q(x,y) implies P(x) ) ) iff forall x in S ( exists y in S ( Q(x,y) ) implies P(x) ).

Notes:
(Q3) is also called the drinker's paradox.
(Q5) states the equivalence between two ways of saying "everyone who mixes with bad company is unreliable".
(Q7) states the equivalence between two different ways of expressing that there is a unique x in S satisfying P.

@user525966 (Q5) is easier than (Q6).

@user525966 Right that's what it means.

@user525966 Yes.

user525966

07:08

@user21820 Is this even close so far?

If ∀x ∈ S (∀y ∈ S (Q(x,y) → P(x))):

    If ￢∀x ∈ S ((∃y ∈ S Q(x,y)) → P(x)):
        ...

        Given d ∈ S:
            ...
            (∃y ∈ S Q(d,y)) → P(d)

        ∀x ∈ S ((∃y ∈ S Q(x,y)) → P(x))
        ⊥

    ∀x ∈ S ((∃y ∈ S Q(x,y)) → P(x))


∀x ∈ S (∀y ∈ S (Q(x,y) → P(x))) ↔ ∀x ∈ S ((∃y ∈ S Q(x,y)) → P(x))

I have no idea how you're supposed to go about solving most of these

does working backwards just not work as well for FOL proofs?

user21820

@user525966 There was no need to do the first "contradiction". If I'm not wrong, the shortest proof of "∀x∈S ( P(x) )" in any context will always be by ∀-intro, and the shortest proof of "A ⇒ B" will always be by ⇒-intro. Same for "A ∧ B". Other than those three, you cannot work backwards systematically.

And for general first-order systems, this lack of an algorithm for proving can in fact be proven! But just to get an idea of how difficult it is, note that Goldbach's conjecture and the twin-prime conjecture can be stated as purely arithmetic sentences. If there was an algorithm that could easily find a proof or disproof of arithmetical sentences, they would not remain open for so long.

user525966

So something more like

If ∀x ∈ S (∀y ∈ S (Q(x,y) → P(x))):

    Given c ∈ S:
        ...
        (∃y ∈ S Q(c,y)) → P(c)
    ∀x ∈ S ((∃y ∈ S Q(x,y)) → P(x))

∀x ∈ S (∀y ∈ S (Q(x,y) → P(x))) ↔ ∀x ∈ S ((∃y ∈ S Q(x,y)) → P(x))

user21820

Yup but that only gives you "⇒", not "⇔".

user525966

yeah just doing one direction at the moment

user21820

Yea just commenting on your last line which has "⇔".

user525966

07:23

if i get one i (would hope) the other side will be easier to get

"And for general first-order systems, this lack of an algorithm for proving can in fact be proven!" is this the incompleteness thing?

If ∀x ∈ S (∀y ∈ S (Q(x,y) → P(x))):

    Given c ∈ S:
        ∀y ∈ S (Q(c,y) → P(c))
        Q(c,d) → P(c)

        If ∃y ∈ S Q(c,y):
            ...somehow → elim the Q(c,d) from above...
            P(c)

        (∃y ∈ S Q(c,y)) → P(c)

    ∀x ∈ S ((∃y ∈ S Q(x,y)) → P(x))

∀x ∈ S (∀y ∈ S (Q(x,y) → P(x))) ↔ ∀x ∈ S ((∃y ∈ S Q(x,y)) → P(x))

@user21820

any closer?

drat I can't edit it but maybe this:

If ∀x ∈ S (∀y ∈ S (Q(x,y) → P(x))):

    Given c ∈ S:
        ∀y ∈ S (Q(c,y) → P(c))

        If ∃y ∈ S Q(c,y):
            Let d ∈ S such that Q(c,d)
            Q(c,d) → P(c)
            P(c)

        (∃y ∈ S Q(c,y)) → P(c)

    ∀x ∈ S ((∃y ∈ S Q(x,y)) → P(x))

∀x ∈ S (∀y ∈ S (Q(x,y) → P(x))) ↔ ∀x ∈ S ((∃y ∈ S Q(x,y)) → P(x))

user21820

@user525966 Yes. Currently experts believe that both open problems I mentioned can either be proven or disproven by ZFC (which is also a first-order system). And if so, there is a trivial algorithm to find a proof, namely enumerate for k from 1 to ∞ all possible proofs of length k and wait until one of them proves or disproves the desired question. Clearly, nobody is going to do this because the program would take longer than any mathematician...

@user525966 That's right. You got the first part, though you could have just used "x" instead of "c".

On to the reverse implication!

user525966

why am I allowed to use x?

I thought in general I had to invoke a constant for ∀-intro, taking an arbitrary object from the domain S

user21820

07:38

@user525966 The rule says you can use any unused variable. At that point where you want to create the subcontext, there are no used variables (as defined in my post). x,y are not fresh, but they are not used.

user525966

I think I will never understand that lol

user21820

Just think about the programming equivalent, if you know first-class functions in say Python or new Java.

user525966

This whole used/fresh/unused/free thing makes zero sense to me even with the programming comparison

user21820

Then you probably don't understand lambda abstraction in programming!

user525966

i use lambdas in python but i usually use different variable labels to prevent any funny business

user21820

07:40

That's what I mean by you don't really understand it.

( int x ↦ x+1 ) is the same object as ( int y ↦ y+1 ).

The variable name doesn't actually matter. We could equally express it using De Bruijn indexing, namely ( int ↦ \1+1 ) where "\1" means "first parameter".

So outside of that definition of the function the variable is not actually in use to refer to anything.

That's why it's unused. In programming, you can create different functions using the same dummy variables. In Javascript for example:

var f = function(x) { return x+1; };
var g = function(x) { return x+2; };

The reason I can safely use x when defining g is because x is not used in the current context (which is outside the definition of f).

Does this make sense?

user525966

If ∀x ∈ S ((∃y ∈ S Q(x,y)) → P(x)):

    Given c ∈ S:
        (∃y ∈ S Q(c,y)) → P(c)

        ...

        Given d ∈ S:
            ...
            Q(c,d) → P(c)

        ∀y ∈ S (Q(c,y) → P(c))

    ∀x ∈ S (∀y ∈ S (Q(x,y) → P(x)))

reading now

user21820

@user525966 Your third line has a mistake.

user525966

fixed hopefully

I understand how x is "unused" in those examples you posted, just less obvious to me when that sort of thing is taking place in a proof (when we can use x, when we need some kind of other letter, etc)

I think I can't use exists-elim directly on the implication without tearing it apart first by using another subcontext but then I'm not sure how to get back out of it correctly

user21820

@user525966 There is a systematic definition. Whenever you declare a variable in a ∀-subcontext "Given x∈S:" then "x" becomes used inside that subcontext. Whenever you declare a variable in any context using ∃-elim like "Let x∈S such that ...", then "x" becomes used from that point onwards until the end of that context. Other than that, no other variables are counted as used.

@user525966 It's not so complicated. To use "A ⇒ B" you typically have to deduce "A" (unless you simply deduce "¬( A ⇒ B )"...).

user525966

What is the difference between "Given x..." (which I think is most similar to doing int x = something) and forall-elim where I can suddenly invoke a new label for something? (what kind of variable is this?)

yeah that's what I mean though, there's nothing there to deduce A directly

probably another variable scoping issue i'm missing lol

brain is mush / about to fall asleep at my desk, calling it a night, thanks again @user21820

good night

user21820

07:58

@user525966 Just a quick answer to this before you sleep.

In ∀-elim, you go from "∀x∈S ( P(x) )" to "P(t)" where t is some object that you already have in the current context. At no point will you 'introduce' any new object or label or variable.

The only way you introduce new objects/variables is via ∀-subcontext and ∃-elim. Hence the above definition of "used".

Anyway, you're welcome and good night! =)

Leaky Nun

12:08

I think I'm confused again

because I've heard that every finite subset of the axioms of ZFC has a model

user525966

14:54

@user21820 From "∀x∈S ( P(x) )" to "P(t)" I think I get that t is already an object we have in current context, as in, we have all the objects in S and we're just taking one, but aren't we still coming up with the label "t" to describe this? Shouldn't this "t" not conflict with anything? Just because I have some_list = [4, 6, 9, 10] if I want to take one I still have to ensure that t = some_list[i] is not in conflict with another t

"The only way you introduce new objects/variables is via ∀-subcontext and ∃-elim. Hence the above definition of "used"."

I understand that these introduce new variables, what I don't understand is why I am allowed to do "Given x∈S" when we have x in a previous line.

I know you mention that "sometimes the x's are different / not the same" because they're sort of wrapped up in their own functions, but we can always restate things in-context and at this point I don't see how it differs from declaring a variable and then needing to avoid reusing/redeclaring it

If ∀x ∈ S (∀y ∈ S (Q(x,y) → P(x))):

    Given x ∈ S:
        ...

and then, what about:

If ∀x ∈ S (∀y ∈ S (Q(x,y) → P(x))):
    ∀x ∈ S (∀y ∈ S (Q(x,y) → P(x)))    [restate]

    Given x ∈ S:
        ...

Are these both equally valid? Does "restating" a header somehow make it a "real" instance I now have to avoid conflict with?

Transcript for

♦ $Mathematics$ Logic

Transcript for

♦ Logic

♦ $Mathematics$ Logic