Basic Mathematics - 2023-09-20

Nav Bhatthal

05:37

@user21820

user21820

06:34

@NavBhatthal: It's not your fault, but it really is frustrating that you're asking questions that would make no sense once you even learn PL..

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

↑ This is a valid proof in PL. It is also sufficient to illustrate all that happens when you use ⇒elim.

@NavBhatthal So superficially it seems that I should just say "yes" to this question, but I'm not sure whether you actually get it!

Actually, maybe I should say "no", because we don't need to "open a new context in which A is given".

You may do so, as illustrated by the above proof.

In general, you can always open a new subcontext anywhere, and so you can always do what you describe when you have deduced "A ⇒ B". But in some cases it may not lead anywhere; you may not be able to gain anything by doing so.

soupless

09:48

12

Q: Is it OK if a proposition contains $\frac{1}{0}$?

I think the following statement is accepted as a proposition. $$\forall x\in \mathbb{Q}\left(x\neq 0\Rightarrow \frac{1}{x}\in\mathbb{Q}\right).$$ This means $$\bigwedge_{x\in \mathbb{Q}}\left(x\neq 0\Rightarrow \frac{1}{x}\in\mathbb{Q}\right).$$ The conjunction includes $$0\neq 0\Rightarrow \fra...

In essence, OP is asking if 0 ≠ 0 ⇒ 1/0 ∈ ℚ, given that ∀x∈ℚ (x ≠ 0 ⇒ (1/x)∈ℚ) and 0∈ℚ.

This is the part where the type signature for operators really matter, as I see it.

user21820

14:10

1

A: Showing permutation does not change output of commutative operation (recursion theorem)

First of all, I don't believe you have sufficient foundation in basic logic to tackle such problems. This is not your fault, naturally, because it is hard to find good teachers. For you to truly grasp how everything in mathematics is built, you would need to learn basic FOL (first-order logic) in...

↑ @PrithuBiswas @soupless: You may be interested in this post regarding the recursion theorem, which we have discussed before! =)

soupless

@user21820 I am interested, but I still don't get this since I haven't encountered this yet.

user21820

I know you haven't gotten to learning this yet, but you may or may not want to look and see how much you can understand. =P

soupless

I do want to learn this, since I am really interested. I want to know how to formalize these notions, since most functions that work with some sort of index are recursive, I think. If I can write it in Haskell, I seem to understand how it is really defined, but not how it is formalized

user21820

Programming languages have inbuilt recursion. Unfortunately, current conventional foundations for mathematics don't.

That's why the recursion theorem is needed.

Incidentally, my personal foundational system has a true fixed-point theorem, which allows proving a recursion theorem that is much cleaner (and more like programming) than the usual recursion theorem that you see in mathematics textbooks (of which I gave one in my post).

For example, to define Fib (fibonacci), one would intuitively like to say.. Let Fib = ( ℕ k ↦ k ≤ 1 ? k : Fib(k−1)+Fib(k−2) ).. and then prove by induction that Fib ∈ ℕ→ℕ.. Too bad that's not allowed by current conventional systems. It's possible in my system. XD

soupless

14:31

Wait, can you explain this part, please? ℕ k ↦ k ≤ 1 ?

Oh, it's a lambda expression.

user21820

My convention is that "↦" has lowest precedence. So the inside part is "k ≤ 1 ? k : Fib(k−1)+Fib(k−2)".

Which is a C/Java-style conditional.

Yea I see you figured it out.

soupless

Maybe it's supposed to be k >= 1?

user21820

No, we want Fib(0) = 0 and Fib(1) =1.

soupless

Sorry, I didn't parse it well. I'm rechecking.

I don't understand the question mark. Maybe it's a syntax thing in C/Java. Ternary operator?

user21820

Yup.

soupless

14:38

Got it. The syntax S x in S x ↦ E(x) feels weird to look at, to be honest. Maybe I'm just not used to it.

user21820

14:58

@soupless Lambda syntax would be ( λx:S. E(x) ). It's weirder, and one could argue has a meaningless lambda.

An alternative would be ( x:S ↦ E(x) ), but I didn't want to use the ":" for yet another thing.

Nav Bhatthal

So 'given' means that a statement holds in a context

If means that in everything following the indent a statement holds

One last thing that confuses me is what's the difference between "If A then B" and "B given A"

@user21820 Thanks so much for putting up with me.

user21820

@NavBhatthal In my system, "Given" is only for ∀subcontexts.

In English, "given" may be used for given conditions/assumptions.

Nav Bhatthal

I see. So it's wrong to say "Given x=1"?

In the technical sense (not natural language)

user21820

You need to decide whether you want to work formally or informally.

If you look at my system, you find that only the ∀sub rule allows you to write "Given ...".

It would be possible for both ∀sub and ⇒sub to use the same word "given", but it would be downright confusing for students.

So if you want to learn to do formal reasoning within my system, you need to stick to it even if English permits "given" to be used in a broader sense.

Anyway, I need to go soon.

soupless

15:14

@NavBhatthal If you want some technical sense, the production rule of a ∀sub header is "Given " <variable> ("," <variable>)* "∈" <type>, for instance, Given x,y,z∈ℝ. In user21820's system, this is the only production rule that uses the word "Given" even though it still makes sense in a much more general setting, like the example you said.

Nav Bhatthal

In natural language I might say

Given x=1 then y=2

I'd interpret this to mean that we have deduced that x=1 implies y=2 and we are now in the context where ,x=1 is given and hence y=2 is true

user21820

@NavBhatthal This is actually incorrect in English..

One might say "Given x = 1, we have y = 2, and hence ...".

It's wrong English to say "Given ... then ...".

Nav Bhatthal

Why the hence

If there is nothing more

user21820

If there's nothing more, it's usually pointless to say anything at all.

Anyway, that's not the point.

soupless

No, that's not how "Given" is used in user21820's system. In natural language, that still somehow makes sense (some handwaving here because we just understand it without it being grammatically complete), at least for me. But it would be confusing once you start to encounter variables since you have to reuse "Given"

(a reply, I typed too slow here)

Nav Bhatthal

15:18

If I have a definition of y in terms of x. Why can I not say, Given x =..., y=... ?

user21820

You can, and there's no "then".

Nav Bhatthal

Then is what I used instead of "we know that..." or "we have"

I spoke it out loud and it sounded silly

I promise I can speak English 🤣

user21820

...

Funny...

Anyway the point really is to stop focusing on how other people use English in a variety of ways (some of which are dubious or wrong).

Just get the logic right..

Later figure out how to say it in English to people who refuse to learn logic.

Ok see you all next time!

Nav Bhatthal

It's hard to use a formal system for my school exams when my teachers don't know such system

So I don't see the point in learning it right now

soupless

Ok, see you soon!

My teachers also don't such a formal system, since it looks too formal

But I learned it, and somehow, some things became clearer

Nav Bhatthal

15:23

@soupless

If we see talking about natural language only and not formal. Would you say 'A given B' and 'A if B' convey the same information.

I would say yeah.

soupless

For me, I see it as a yes. But it was really confusing at first.

Nav Bhatthal

15:40

What was confusing at first?

Prithu Biswas

@user21820 Does the author really want the reader to first construct the summation function using recursion and then prove the theorem suing induction? O_O

If it is, then it seems too demanding to me for an analysis 1 book.

soupless

@NavBhatthal Sorry for the late reply. I still don't understand the concept of necessity and sufficiency because the "Given" keyword there or the "A if B" format bugs me out

Nav Bhatthal

A if B means $B \implies A$.

I am merely saying that I think this conveys the same information in natural language as does the "incorrect" statement '$A$ given $B$'

Prithu Biswas

@user21820 Regardless, I upvoted it. It is an awesome answer.

soupless

I reconstruct it first, so it's "A, if B." which makes me get it, but it's confusing at first. I don't know how else I can express it.

@NavBhatthal I'm not sure, but it is still probably valid in natural language.

But even if it does convey the same information, doesn't mean we should allow using it. I mean, we could, but we need to provide additional context once we start writing proofs involving universal quantifiers.

Nav Bhatthal

15:49

Yes

soupless

If P:
    Given x∈S:
        P.

Nav Bhatthal

Can you then conclude that $\forall x \in S (P)$?

soupless

If we allow using "Given" to have an "if" function, then what is "Given" doing here? Is it referring to P holding for all x∈S, or is it that x∈S implies P?

Nav Bhatthal

I'm not sure

soupless

@NavBhatthal Yes, that's true in user21820's system. From this point, I'll just refer to user21820's system as "the system"

Nav Bhatthal

15:52

Did he make this system or something?

soupless

@user108262: You're welcome and I hope it helps you as much as it has helped me! When I devised these rules I was strongly influenced by programming where the context of every statement is explicit. That really is the key, because it is then simple to construct the inference rules based on intuition. Like in programming, there can be multiple statements within the same context, and this minimizes the amount of writing needed, in stark contrast to Hilbert-style systems. I presented it here in Fitch-style but we can just as well use braces or indentation like in C or Python. — user21820 Mar 10, 2016 at 0:57

So it seems like user21820 did.

@NavBhatthal That's why in the system, we only use "If" to refer to (Boolean) assumptions, while "Given" refers to objects and how they are being 'described'

I keep quoting 'described' because in the sample proof I sent, P doesn't really describe x.

I hope I got it right.

EE18

16:47

@user21820 I am looking forward to reading your full answer more closely this evening, but in the meantime may I ask -- do you have a favorite reference for mathematical logic as discussed in your answer? I have heard of only Ebbinghaus

Prithu Biswas

17:15

21

A: What are the prerequisites for studying mathematical logic?

If you have mathematical background, I recommend Hannes Leitgeb's Mathematical Logic lecture notes, which introduces modern first-order logic up to Godel's first incompleteness theorem, with a conventional kind of deductive system, and has exercises and solutions. Another good reference is Steph...

@EE18 These are user21820's recommendation for Studying logic.

EE18

Thanks Prithu!

Oh ya, reading that first set of notes it looks like they follow Ebbinghaus. Very cool!

Prithu Biswas

Also, if you wish to first learn logic.

40

A: Predicate logic: How do you self-check the logical structure of your own arguments?

Truth tables are not enough to capture first-order logic (with quantifiers), so we use inference rules instead. Each inference rule is chosen to be sound, meaning that if you start with true statements and use the rule you will deduce only true statements. We say that these rules are truth-preser...

EE18

17:34

Got it, thanks again for all the help Prithu

Transcript for

♦ $Mathematics$ Basic Mathematics

Transcript for

♦ Basic Mathematics

♦ $Mathematics$ Basic Mathematics