Basic Mathematics - 2021-07-19

Prithu biswas

10:03

@user21820 I am having some confusion understanding the inference rules for quantifiers from this post of yours:

https://math.stackexchange.com/questions/1681857/predicate-logic-how-do-you-self-check-the-logical-structure-of-your-own-argumen/1684204#1684204

Can I ask them to you?

user21820

@Prithubiswas Which rule?

Prithu biswas

∃elim.

user21820

@Prithubiswas What's the issue?

Did you understand the "Example"?

Prithu biswas

In the rules you said:

"Let y∈S such that P(y). [∃elim]"

But in the example you said:

"Let a∈S such that ∀y∈T (P(a,y)). [∃elim]"

First you used y as a free variable , then you used "a" which I think is not a variable , but an object expression. That is my confusion.

user21820

@Prithubiswas I did not use the term "free variable". Please use the same terms otherwise you are either confusing yourself or confusing me.

Prithu biswas

10:12

In the list of inference rules of that post , For the ∃elim rule you said "y is a fresh variable". Sorry I mistakenly wrote "free".

user21820

@Prithubiswas Yes, so what is wrong with my use in the Example? "a" is a fresh variable at that point by the definition of "fresh".

Prithu biswas

@user21820 Then why use the letter "a" for denoting a variable?

user21820

@Prithubiswas Your question doesn't make sense. Why do programming languages allow you to use "a" as a variable name??

Or why do mathematicians use "a" as a variable in their proofs?

The rule says you must use a fresh variable. It never said you must use "y".

Prithu biswas

@user21820 I mean commonly we use x,y,z for variables and a,b,c as constant. So when I saw "a" , I thought it was an object expression. It is new to me that a,b,c are also used as variables.

user21820

@Prithubiswas Your first sentence is simply false.

Prithu biswas

10:20

Oh so people do use a,b,c for variable names. That is new to me.

user21820

Sets are typically called S,T,U. Matrices, A,B,C. Functions, f,g,h. Degree/diameter/depth d. Fields, F,K,L. But that's irrelevant to the point that you can use anything you want. Even what you think of as "constants" are almost never true constants.

They are just quantified variables like any other.

In number theory, usually only 0,1 (and other numeric constants) are the true constants.

"f is a linear (real-valued) function on ℝ" ≡ "∃c∈ℝ ∀x∈ℝ ( f(x) = c·x )". Both c,x are variables of exactly the same kind.

Prithu biswas

Another confusion.For the definition of Unused variable you said:=

"Unused variable: A variable that is not declared in the header of any containing ∀-subcontext or in any previous ∃-elimination ("let") step in the current context or any containing contexts."

I didn't really understood this line. Maybe because the sentence is a bit too long for me.

Maybe examples might help.

user21820

@Prithubiswas Unused variable: A variable that is not declared ( in the header of any containing ∀-subcontext ) or ( in any previous ∃-elimination ("let") step in ( the current context or any containing contexts ) ).

Prithu biswas

What does it mean by " in the header of any containing ∀-subcontext"?

user21820

@Prithubiswas Uh, that's the basic notion of "Contexts", isn't it? I wrote:

> Every line is either a header or a statement. Only headers can have lines subsumed under it, as in a multi-level list. The context of each statement is specified by all the headers that are in effect.

So you just look at all the headers of surrounding contexts, as well as those ∃elim statements that came before it in one of those contexts, to figure out which variables are already used (in the current context you are interested in).

Prithu biswas

10:34

what is ∀-subcontext?

user21820

Of the form "Given x∈S:".

Prithu biswas

by all the headers you mean "Given" and "Let" headers , right?

user21820

"Let ..." is not a header, which is why the definition of "unused" also has to mention them.

Prithu biswas

Oh , thats why in your post , lines are not sublimed under "let" becuase it is not a header...

user21820

Yes. There are two main variants of deductive systems for FOL. One is mine, and the other has a different kind of ∃elim. I do not like the other kind because it creates many unnecessary subcontexts.

Can you imagine if you do ∃elim 3 times in a row by applying previous lemmas and thus get yourself nested 3 times deeper?

Not "sublimed", by the way, but "subsumed". =)

Prithu biswas

10:45

Oh ok it is subsumed.

Also by "surrounding context" you mean the current context and the parent context of the current context. right?

user21820

Yes, and all the ancestors.

Prithu biswas

The word "ancestor" is the same as "parent"?

user21820

@Prithubiswas No? "Parent" is only one level up.

Prithu biswas

So , Lets say I pick a line in the proof , and pick a variable from that line. Then we check the headers of the current context the line is in and the headers of all the ancestor contexts of the current context. If the variable is not declared in any of those headers , then that variable is an unused variable. right?

Oh we also have to check ∃elim.

user21820

@Prithubiswas Exactly. Now you know why the definition is not so simple.

Prithu biswas

10:57

Oh ok.

I am asking these questions so that I am sure about the syntax of FOL. Hope you didn't mind.

user21820

11:14

@Prithubiswas Of course I don't mind.

By the way, I don't expect you to get the deductive rules right on the first try (in the exercises), so it's okay if you make mistakes there and we correct the mistakes along the way.

Ok I got to go. Bye!

Prithu biswas

16:35

@user21820 I have another confusion.In the post of the fitch-style system,

Object expression: An expression that refers to an object.
In classical first-order logic,
the object expressions are simply the well-formed terms
(whose free variables are each declared in the header of some containing ∀-subcontext).
In the following rules E,F (if involved) can be any object expressions.

But I am still not sure what object expressions actually are.

Prithu biswas

17:03

Are the object expressions are simply the well-formed terms
(whose free variables are each declared in the header of some containing ∀-subcontext).?

In you deductive system?

user21820

@Prithubiswas Well I sort of assumed that the reader did know the basic syntax of FOL formulae, and was just providing a deductive system. So yes I presume you already do know that an object expression is either a variable or a function-symbol applied to some object expressions.

Maybe the point you miss is that all these different deductive systems all prove the same FOL (first-order logic) tautologies, and the same theorems from any given FOL axiom set. The proofs may look completely different, but the theorems are the same.

(Of course ignoring the fact that my system is for many-sorted FOL whereas common texts only target the typical one-sorted FOL.)

Anyway as far as (Q1) to (Q5) are concerned, you never have to use any object expressions beyond variables, since those exercises do not involve any function-symbols.

Prithu biswas

In your deductive system , do object expressions have follow the rule that:

"(whose free variables are each declared in the header of some containing ∀-subcontext)." ?

user21820

@Prithubiswas Yes, that is a must.

Prithu biswas

And the ∃intro rule:

| E∈S.
| ...
| P(E)
| ...
|-------------------------
| ∃x∈S

right?

where E is an object expression.

Here is the example given in your post.

If ∃x∈S (∀y∈T (P(x,y))):   [⇒sub]
   ∃x∈S (∀y∈T (P(x,y))).   [⇒sub]
   Let a∈S such that ∀y∈T (P(a,y)).   [∃elim]
   a∈S.   [∃elim]
   ∀y∈T (P(a,y)).   [∃elim]
   ∀z∈T (P(a,z)).   [∀rename]
   Given y∈T:   [∀sub]
      y∈T.   [∀sub]
      ∀z∈T (P(a,z)).   [∀restate]
      y∈T.   [restate]
      P(a,y).   [∀elim]
      a∈S.   [∀restate]
      ∃x∈S (P(x,y)).   [∃intro]
   ∀y∈T (∃x∈S (P(x,y))).   [∀intro]
∃x∈S (∀y∈T (P(x,y)))⇒∀y∈T (∃x∈S (P(x,y))).   [⇒intro]

user21820

Ah I see what you mean. Yes there is an error there.

The variables declared by the active ∃elim can also be used to form object expressions, as you might expect.

Lol. The example is correct. Just my remark in brackets is incomplete.

Good spotting!

Prithu biswas

17:17

So in the statement:
"(whose free variables are each declared in the header of some containing ∀-subcontext)."
Should be changed to:

"(whose free variables are each declared in the header of some containing ∀-subcontext) or in some previous ∃-elimination ("let") step in the current context or any containing contexts"

correct?

@user21820 [Correction to my previous comment]

So the statement:

"Whose free variables are each declared in the header of some containing ∀-subcontext."

Should be changed to:

"Whose free variables are each declared in the header of some containing ∀-subcontext or in some previous ∃-elimination ("let") step in the current context or some containing contexts."

Is this correct?

user21820

@Prithubiswas Yea, or you can just cheat and say, whose free variables are all used variables (opposite of unused variables). Hehe.

Prithu biswas

Oh ok because the description is quite similar to the description of unused variable.

just opposite

user21820

17:39

@Prithubiswas Yea. Basically the whole idea is simply that at any point some variables are used (to refer to some objects), and you can use unused variables for new ∀subcontexts (in which that declared variable would of course become used).

And whatever variables are used can of course be combined syntactically with function-symbols to refer to more objects.

F. Zer

17:53

@user21820 Hello, how are you ? I hope you are well ! Since you are teaching again PL, I took the chance to give a fresh look after finishing your whole set and evaluate my current mindset. Could you tell me what do you think of my P6 proof ?

(P6)
  If ¬(( A ⇒ B ) ⋁ ( B ⇒ A ) ):
    If A:
      If B:
        A
      B ⇒ A
      ( A ⇒ B ) ⋁ ( B ⇒ A )
      ⊥
    ¬A
    If A:
      ⊥
      B
    A ⇒ B
    ( A ⇒ B ) ⋁ ( B ⇒ A )
    ⊥
  ( A ⇒ B ) ⋁ ( B ⇒ A )

user21820

@F.Zer That's correct!

F. Zer

Thank you !

@user21820, I am looking at Velleman's book...A=B is equivalent to ∀ x ( x ∈ A ⇔ x ∈ B); could you tell me how do you write it in your system since you use restricted quantifiers ?

user21820

18:23

@F.Zer That's for sets A,B. In my system, you need to explicitly state the type of every object, including sets.

And what you stated is the extensionality axiom given in my post.

Note that my axiomatization of set theory is slightly different from the usual ZFC, but has the same strength.

F. Zer

@user21820 Thank you. I should get a book on set theory; could you recommend one, please ?

user21820

@F.Zer Oh, you're really interested in set theory?

I don't recommend studying ZFC specifically partly because it is completely irrelevant to almost all mathematics.

So unless you have a specific motivated interest in ZFC, in my opinion it's not a good way to spend time.

F. Zer

@user21820 Thanks for your opinion ! Sorry for the really naive question, I would like (have to) do proofs involving sets. Is set theory really necessary ?

That's my specific interest.

user21820

@F.Zer No, that's precisely the point. Books that are sold on set theory are really books about ZFC, not about using set theory for ordinary mathematics.

F. Zer

@user21820 Good. Exactly. I specifically want to use set theory for ordinary mathematics.

user21820

18:38

What you should do is simply to translate what you learn from normal mathematics books such as Spivak's Calculus and Velleman's How To Prove It into the system we've been using, and I'll help you if you get stuck on the set-theoretic axioms.

F. Zer

@user21820 Thank you so much. I appreciate it. Could you give me the skeleton of the proof A = B, please ?

user21820

That's also why my version is different from the usual ZFC, because I made it as user-friendly as possible while retaining the full strength of ZFC.

@F.Zer Well the extensionality axiom is what you'd want to use, so just apply it to the sets you want and you'd have an equivalence.

Technically, FOL already proves ∀S,T∈set ( S=T ⇒ ∀x∈obj ( x∈S ⇔ x∈T ) ). This is an easy tautology that you can prove. So the real impact of extensionality is in the other direction: ∀S,T∈set ( ∀x∈obj ( x∈S ⇔ x∈T ) ⇒ S=T ).

Which is clearly what you need to prove two sets equal.

Note that ∀x∈obj ( x∈S ⇔ x∈T ) ≡ ∀x∈S ( x∈T ) ∧ ∀x∈T ( x∈S ), which is why textbooks will generally tell you to prove S⊆T and T⊆S in order to prove S=T.

F. Zer

Thank you. I'll digest this a little bit.

(P7)
  If A ⇒ B ⋁ C:
    If ¬ ( ( A ⇒ B ) ⋁ ( A ⇒ C ) ):
      If ¬A:
        If A:
          ⊥
          B
        ( A ⇒ B ) ⋁ ( A ⇒ C )
        ⊥
      A
      B ⋁ C
      If B:
        If A:
          B
        A ⇒ B
        ( A ⇒ B ) ⋁ ( A ⇒ C )
        ⊥
      If C:
        If A:
          C
        A ⇒ C
        ( A ⇒ B ) ⋁ ( A ⇒ C )
        ⊥
      ⊥
    ⊥
    ( A ⇒ B ) ⋁ ( A ⇒ C )

@user21820, this is the last exercise of PL set. Not sure if this is a clean proof of P7. What do you think ?

user21820

@F.Zer It's clean. What did you doubt?

There may be a shorter but asymmetrical proof; I can't recall now.

F. Zer

18:55

@user21820 Good. Thank you. I thought perhaps doing the proof without deriving "A" first. But I can't remember.

user21820

@F.Zer Don't bother. This one is nice enough haha..

F. Zer

Good :-)

F. Zer

19:12

@user21820 Here is my attempt:

Prove ∀ S, T ∈ set ( S = T ⇒ ∀ x ∈ obj ( x ∈ S ⇔ x ∈ T ) )
  Given S, T ∈ set:
    If S = T:
      If x ∈ obj:
        If x ∈ S:
          ...
          x ∈ T
        If x ∈ T:
          ...
          x ∈ S
        x ∈ S ⇔ x ∈ T
      ∀ x ∈ obj ( x ∈ S ⇔ x ∈ T )
    S = T ⇒ ∀ x ∈ obj ( x ∈ S ⇔ x ∈ T )
  ∀ S, T ∈ set ( S = T ⇒ ∀ x ∈ obj ( x ∈ S ⇔ x ∈ T ) )

user21820

@F.Zer "If x∈obj:" is incorrect. You mean "Given". Then it's correct, but why did you leave the "..."?

F. Zer

@user21820 Yes, sorry. I will fix in my notes. I don't know how to fill the "...". I do know S = T. How can I formally justify ?

S = T means ∀ x ( x ∈ S ⇔ x ∈ T ). However, you already noted that wasn't allowed in your system.

user21820

@F.Zer It's just =elim! No need for any other steps!

F. Zer

@user21820 Ohhhh ! That's fantastic !!

I never thought about using =elim with sets !

Of course, I can replace any occurrence of S by T (and viceversa).

Prove ∀S,T∈set ( ∀x∈obj ( x∈S ⇔ x∈T ) ⇒ S=T )
  Given S, T ∈ set:
    If ∀ x ∈ obj ( x ∈ S ⇔ x ∈ T ):
      ...
      S = T
    ∀ x ∈ obj ( x ∈ S ⇔ x ∈ T ) ⇒ S = T
  ∀S,T ∈ set ( ∀x∈obj ( x∈S ⇔ x∈T ) ⇒ S=T )

user21820

@F.Zer Why are you trying to prove this when I said it's the extensionality axiom?

F. Zer

19:24

@user21820 Oh, you said the first one was an easy FOL tautology to prove. You didn't say anything about the second one. Sorry.

user21820

I did.

1 hour ago, by user21820

And what you stated is the extensionality axiom given in my post.

43 mins ago, by user21820

Technically, FOL already proves ∀S,T∈set ( S=T ⇒ ∀x∈obj ( x∈S ⇔ x∈T ) ). This is an easy tautology that you can prove. So the real impact of extensionality is in the other direction: ∀S,T∈set ( ∀x∈obj ( x∈S ⇔ x∈T ) ⇒ S=T ).

Impact meaning significant consequence.

F. Zer

@user21820 Yes, I just meant you didn't say I should prove the second one.

user21820

Ah, yes.

F. Zer

@user21820 So, the first one is an easy derivation within FOL. The really important bit is the other direction.

user21820

Yes.

F. Zer

19:35

Theorem. Suppose A ⋂ C ⊆ B and a ∈ C. Then a ∉ A \ B.
  If A ⋂ C  ⊆ B ∧ a ∈ C:
    If a ∈ A \ B:
      A ⋂ C  ⊆ B
      ∀ x ∈ A ⋂ C ( x ∈ B )
      ...
      ⊥
    a ∉ A \ B

@user21820, this is my first concrete example with sets. Could you tell me if the proof skeleton is correct ? I want to prove it within your system. I leave it here.

Transcript for

♦ $Mathematics$ Basic Mathematics

Transcript for

♦ Basic Mathematics

♦ $Mathematics$ Basic Mathematics