Logic - 2018-10-22

2:06 AM

@user525966 The difference is that you need to read the fine-print. The rules for the boolean operations start by saying "Take any statements A,B,C (in the current context)." and so we can apply them to statements only. The rules for quantifiers say "Now take any type S and a property P and an unused variable x that does not appear in S or P." and so we can only create a new subcontext "Given x in S:" if x is an unused variable.

user21820

2:19 AM

@user525966 You are right that it is very close. But it is incorrect because the Forall-Restate rule does not permit pulling "exists x in S ( P(x) )" in under "Given x in S", because "x" appears in "exists x in S ( P(x) )". And this restriction is necessary, otherwise it is ambiguous what "x" refers to, since now it is under both "exists x in S" and "Given x in S:".

@user525966 So the corrected proof is:

If not exists x in S ( P(x) ):
    not exists y in S ( P(y) ).
    Given x in S:
        If P(x):
            exists y in S ( P(y) ).
            Contradiction.
        not P(x).
    forall x in S ( not P(x) ).
not exists x in S ( P(x) ) implies forall x in S ( not P(x) ).

@user525966 Same here. It's practically correct but we need to avoid the variable ambiguity.

user21820

2:56 AM

Anyway aside from that minor issue, you have gotten the core idea for (Q1) and (Q2), so well done!

@user525966 For (Q3) you're right to question line 2, because the rules don't permit that. This should make sense because at that point "x" is undefined so it won't be meaningful to say "x in S". What you want to do is Exists-Elim to obtain a witness to "exists x in S ( x in S )".

user21820

3:10 AM

@PrashinJeevaganth: If you haven't tried the exercises, you can start reading from here. Here is a concrete example of why variable ambiguity (called variable shadowing in programming) should be avoided:

If forall x in S ( exists y in S ( not x=y ) ):  [If-Sub]
	Given y in S:  [Forall-Sub]
		forall x in S ( exists y in S ( not x=y ) ).  [Invalid use of Forall-Restate]
		exists y in S ( not y=y ).  [Forall-Elim]
		Let c in S such that not c=c.  [Exists-Elim]
		c=c.  [Equality-Intro]
		Contradiction.  [Not-Elim]
		[And now we can get all sorts of nonsense.]

The Forall-Restate rule says that "y" must not appear in the statement you pull into "Given y in S:", and for good reason, otherwise Forall-Elim would give nonsense. Some other deductive systems do permit variable ambiguity but then their Forall-Elim rule would need some complicated restrictions. I choose to forbid variable ambiguity because it's simpler.

Note that line 1 essentially says "If for every member in S there is an other member in S:", which can be true, for example if S has 2 members. So we should not be able to deduce arbitrary things about every y in S.

user21820

3:31 AM

For a similar example in the language of PA:

Given k in N:
	0<1.  [axiom 14]
	0+k<1+k.  [axiom 11,forall-elim,implies-elim]
	k+0=k.  [axiom 6,forall-elim]
	k+0=0+k.  [axiom 2,forall-elim]
	0+k=k.  [equality-elim]
	k<1+k.  [equality-elim]
	1+k in N.  [unstated axiom]
	exists m in N ( k<m ).  [exists-intro]
forall k in N ( exist m in N ( k<m ) ).  [forall-intro]
Given m in N:  [forall-sub]
	forall k in N ( exist m in N ( k<m ) ).  [invalid forall-restate]
	exists m in N ( m<m ).  [forall-elim]
	Let c in N such that c<c.  [exists-elim]
	not c<c.  [axiom 9]

user525966

3:47 AM

@user21820 I did consider exists-elim to get a witness but to my eye it looks like I would have to use a variable other than x for that?

user21820

Yup.

If you want to think of it in programming terms, "exists x in S ( P(x) )" is like a black-box procedure B that you can call and which returns some x in S that satisfies P. Then Exists-Elim is simply declaring a fresh variable and assigning it to the output of B. Like this in Java: S c=B();

user525966

but then I don't know how to correctly tie things back to finish the proof in terms of x

user21820

Exists-Intro allows you to use any unused variable, and "x" is not used.

user525966

How would my Q3 proof need to change?

user21820

4:05 AM

Oh I didn't read the rest of you attempt. You made another mistake, and this one is critical. Let's see what you have if you use Exists-Elim correctly:

If exists x in S ( x in S ):
    Let c in S such that c in S.
    If P(c):
        exists x in S ( P(x) ).
        Given y in S:
            ... [Exists-Elim requires a fresh variable. "y" is not fresh.]

This is important; if you think about the black-box analogy, you don't get to choose what witness you get. So you cannot use "y" under "Given y in S:" because it had already been given.

(Q3) is an interesting question. Why don't you think about what it means, and whether you are convinced that it is true, and why, and then attempt to translate your reasoning into a proof?

user21820

1:45 PM

@PrashinJeevaganth @user525966 @LeakyNun: I have updated my post with a full foundational system comprising PA plus a Set Theory. So now everything is contained in that one post. It also has nice LaTeX now, though sadly it's slow to render.

user525966

@user21820 TBH I'm not even entirely sure

It seems sort of self-evident in certain spots

user21820

@user525966 Try using LEM to split cases.

user525966

like there exists an x in S such that x is in S, isn't this always going to be the case?

user21820

@user525966 Not if S is empty.

user525966

what I mean is, isn't the second one redundant?

if S is empty then "exists x in S" is already a problem, but if S is not empty, then "exists x is S" is fine, but then adding "such that x is in S" seems superfluous

user21820

1:50 PM

@user525966 Right, the inside part is redundant. I just put it there because I need to put something.

Got to go. Back later.

Prashin Jeevaganth

2:07 PM

@user21820 Hmm, does that mean we only need to refer to the post and do not need a wiki anymore?

user21820

2:27 PM

@PrashinJeevaganth Yup everything is there now. Even later after you finish learning PA, if you want to do higher mathematics the next step is to learn the set theory there, which is basically what mathematicians need in practice. =)

Search for "Peano Arithmetic" in that post and you will see all the axioms there. (I modified them slightly to make them even easier to use, but they are equivalent.)

Prashin Jeevaganth

2:48 PM

@user21820 thanks for your efforts. Are you by any chance a teacher by profession? You definitely seem better than my tutor or professor.

user21820

3:44 PM

@PrashinJeevaganth I've taught undergraduate mathematics courses before, but I'm not a teacher by profession. It's true that for a mathematics teacher to be good he/she has to know how to formalize his/her arguments in first-order logic, because then he/she can justify everything rigorously and leave nothing to guesswork or hand-waving. That's why I always emphasize learning logic first.

user525966

3:57 PM

@user21820 What is the correct way to interpret multiple variables being used at the same time?

is it just doing "given x, y in S" sort of thing? or the same as "given x in S, and given y in S", or same as having two nested given contexts?

would this count as both an object expression for x as well as one for y, even though it involves more than one variable, or is it strictly "an object expression for x and y" and not x or y individually?

user21820

@user525966 In my post I did not permit creating a subcontext with multiple variables at the same time. You can create nested subcontexts, each declaring one variable. And then inside the innermost one both variables would be defined. Like this:

Given x in S:
  x in S.
  Given y in T:
    [here you can use both "x" and "y" as object expressions.]
    x in S.
    y in T.

user525966

(I refer to things like your Q4 where you have "forall x,y in S ( P(x) and P(y) implies x=y")

and how a forall x, y statement might be created/permitted by the rules

user21820

Oh that one I did define in my post under "Short-forms". It's just to save unnecessary typing.

user525966

a minor point but I think there's a missing \ on the forall in the post, but I see it now, thanks

user21820

@user525966 Yes I noticed that, and intend to fix all the minor errors that I see in the next few hours or so, at one go.

You can indeed think of it as quantifying both at the same time, but I did not want to make more rules, so I just rely on the existing rules by treating it as merely a syntactic short-form.

So although intuitively "forall x,y in S ( ... )" is obviously the same as "forall y,x in S ( ... )", syntactically the system treats them to mean different order. Of course, you can check that the system also easily allows you to get one from the other, so it's not a big deal.

user525966

4:11 PM

Why is forall-sub called so?

I still don't see why it isn't just a "restate" rule

or is it referring to both lines together?

e.g. is an if-statement in itself technically if-sub even if we aren't also restating the condition?

for instance, is it:

If P(x): [if-sub]
    Given x in S: [forall-sub]
        x in S. [restate]

user21820

@user525966 The last line would be by "forall-sub" according to the rules. I chose to name the rules that way only to distinguish between statements previously deduced and statements that arise from the subcontext.

I don't really care whether you want to ignore the rules' names. Their main use is so that we can know what rule each other is referring to. After you can follow the rules you will be able to invent your own system to suit yourself. =)

@user525966 If you notice both Implies-Sub and Forall-Sub in that post allow stating what is in the subcontext header inside the subcontext. The only difference is that one declares a variable and the other just declares a true condition.

user525966

4:55 PM

@user21820 So if we have

If ∃ x ∈ S ( x ∈ S )

What can we even do with this?

I don't know what it looks like to correctly eliminate the exists/use a witness here

for instance could I do:

If ∃ x ∈ S ( x ∈ S ):
    Let y ∈ S such that (y ∈ S)
    y ∈ S

In particular I can't use x here? Or can I?

user21820

@user525966 Yes this is all you can do. And yes you can't use x because it's not defined.

Basically, all you can get from "∃ x ∈ S ( x ∈ S )" (which is equivalent to just saying "S is non-empty") is some random witness y that you know nothing about except that "y ∈ S".

user525966

5:13 PM

@user21820 I still can't determine from these rules how one is supposed to do Q3 -- what's the intended solution, to get a better sense for all this context/variable naming stuff?

user21820

@user525966 It's impossible to prove directly. That's why I hinted that you need LEM.

user525966

I mean it seems like we have to do something weird, because directly we'd need:

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

and I don't think we can pull x ∈ S directly

user21820

@user525966 Not quite; if you literally work backwards based on the rules, you would need:

user525966

isn't that the rule for exists-intro?

user21820

If ∃ x ∈ S ( x ∈ S ):
    ...
    E ∈ S.
    P(E) → ∀ y ∈ S ( P(y) ).
    ∃ x ∈ S ( P(x) → ∀ y ∈ S ( P(y) ) ).

For some E to be determined.

user525966

5:21 PM

what must be in E? what permits us to use x there?

user21820

@user525966 Use x where?

user525966

on that last line

user21820

Exists-Intro.

I'm not saying that's the correct solution sketch, because it's not, but at least that's what you would get if you literally tried to work backwards from the desired statement by 'reversing' Exists-Intro.

Like with (Q1) and (Q2), when the direct approach does not seem to work, you should try DNE (or LEM).

user525966

sure, but I'm still unclear on these rules to begin with which makes them hard to use

I know that's exists-intro but so is the thing I wrote above is it not?

What's the difference?

Is E not allowed to be a statement about x?

or are you just being rigorous in terms of what we could put there if we were truly working backwards

For example we could possibly do,

If ∃ x ∈ S ( x ∈ S ):
    ...
    c ∈ S.
    P(c) → ∀ y ∈ S ( P(y) ).
    ∃ x ∈ S ( P(x) → ∀ y ∈ S ( P(y) ) ).

user525966

5:48 PM

Also when Googling the drinker's paradox I see it stated a little differently,
∃ x ∈ S (P(x) → ∀ y ∈ S (P(y)))

user21820

@user525966 Yes I am just being rigorous in terms of not confining it to a variable. In general it may be a compound expression and not just a variable. That's all.

user525966

if we treat S like "the bar" and "x" as a person and "P(x)" as "person x is drinking", saying "there exists a man in the bar such that if he's drinking, everyone in the bar is drinking"

user21820

@user525966 This version as stated is incorrect. A counter-example is when S is empty.

user525966

It does say the set must be nonempty

Drinker paradox

The drinker paradox (also known as the drinker's theorem, the drinker's principle, or the drinking principle) is a theorem of classical predicate logic which can be stated as "There is someone in the pub such that, if he is drinking, then everyone in the pub is drinking." It was popularised by the mathematical logician Raymond Smullyan, who called it the "drinking principle" in his 1978 book What Is the Name of this Book?The apparently paradoxical nature of the statement comes from the way it is usually stated in natural language. It seems counterintuitive both that there could be a person who...

user21820

That's why my version has that extra condition.

In a formal system, we cannot say S must be non-empty outside of the system.

So we have to say it inside.

Hope that makes sense. Got to go now! =)

user525966

5:56 PM

There's no way to say something like
∃ x ∈ S → ∃ x ∈ S ( P(x) → ∀ y ∈ S ( P(y) ) )
?

(trying to avoid the redundant statement)

user21820

@user525966 We can of course make a system where that is permitted, but the one in my post does not. Another alternative is "exists x in S ( x=x )". I know it's odd, but there's always a trade-off between simplicity and ability. The more ability, the less simplicity (the more rules).

user21820

6:23 PM

@user525966 @PrashinJeevaganth Let's delay the original (Q4) and insert 3 simpler exercises:

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

Okay I'm off! =)

Transcript for

♦ $Mathematics$ Logic

Transcript for

♦ Logic

♦ $Mathematics$ Logic