Basic Mathematics - 2021-11-26

Prithu biswas

08:53

@user21820 I think I will study about this later , because it seems like it is currently beyond my level.

@user21820 How do you define a function like f(x) = x^n in FOL, where x is a real number and n is a natural number ?

user21820

09:06

@Prithubiswas Very good question. It cannot be done without induction/recursion. The ideal approach is to first prove a recursion theorem and then apply it.

Oh, I wonder whether you're asking because we briefly mentioned this issue in this room:

Aug 15 at 17:38, by user21820

@F.Zer Indeed. Defining x^k for arbitrary k∈ℕ would require you to actually define the exponentiation function. Which we haven't come to yet. You should read (1) in the post I linked to before, because it's relevant:

5

A: When is a proof or definition formal?

There is one aspect of "definitions" that is not exactly asked in your question, but is relevant to mathematics. There are actually two kinds of completely formal definitions, arising from two separate mechanisms: $ \def\nn{\mathbb{N}} $ Definition by existential instantiation: When we have an ...

Aug 15 at 18:03, by user21820

There is actually an alternative to the approach in the linked post, which you might prefer. I'll do it now for the desired pow : ℝ×ℕ→ℝ. Let pow = { t : t∈(ℝ×ℕ)×ℝ ∧ ∃x∈ℝ ∃k∈ℕ ∃c∈ℕ ∃f∈FN(ℕ[≤c],ℝ) ( f(0)=1 ∧ ∀i∈ℕ[<c] ( f(i+1) = f(i)·x ) ∧ ⟨⟨x,k⟩,f(k)⟩ = t ) }. I claim that pow∈FN(ℝ×ℕ,ℝ). This is the non-trivial part, but if you manage to read and understand what this set means, you will see that it is just the set of all mappings in some function that obeys the recursion up to a finite point.

MaxH

09:48

@user21820 So I thought about the problems you gave me, but I think I need to understand the notation of your post in order to write them down the way you did correctly. Could you please explain the notation of your post?

user21820

@MaxH Firstly, do you (think you) understand exactly how each line in my above example is permitted by the rules?

Don't care too much about notation. All that matters is whether you can produce a perfect formal proof or not.

MaxH

I understand them but rather on an intuitive level than exactly applying the rules you give because I can't read the rules due to the notation I am not familiar with.

Meaning, I could write down proofs probably, but rather with the knowledge I had before and using what is intuitive to me

user21820

@MaxH It's strange if you can produce perfect PL proofs that obey the rules but cannot actually understand the rules. What is your native language?

MaxH

Well, I don't know if they are perfect.

I can provide you an example

Just a minute.

user21820

Haha please do. =)

MaxH

09:57

A or B and C iff (A or B) and (A or C)
	If A or B and C
		A or B
		C
		If A
			(A or B) and (A and C)
			(A or B) and (A or C)
		If B
			(A or B) and (B and C)
			(A or B) and (A or C)
		(A or B) and (C or A)

The indenting is probably wrong and I couldnt provide the arguments, because I can't read the rules, but I think the arguments should be correct with justification (at least I hope so).

This is only one direction by the way.

For example purposes

user21820

Ok firstly you're reading the exercise wrong. I'm using the standard precedence rules, namely that the operations are evaluated in order of ¬,∧,∨,{⇒,⇔} if brackets do not disambiguate, but brackets must be used for operations at the same level. "⇒" and "⇔" are at the same level.

So the exercise asks to prove ( A or ( B and C ) ) iff ( (A or B) and (A or C) ).

MaxH

Ok, that was not known to me.

user21820

Good, now you know. That's why I said this kind of thing must be learnt by doing.

MaxH

Not explicitly at least.

But perhaps you can see the problem I have. I think I can conclude the steps I did correctly and with justification, but not with the rules you provided - because I can't read the notation at all. I have never used or seen such a system before.

user21820

Secondly, none of the rules allow you to get "(A or B) and (A or C)".

MaxH

10:03

If I have A and C I also have that A or C is true, right?

user21820

Yes, but that is not permitted by the rules! So, even ignoring the issue with precedence rules, you are not able to produce perfect PL proofs.

MaxH

Again, I did this intuitively, I can't read the rules.

user21820

I know you can't read the rules. I am just saying that I was right that you can't actually produce formal proofs.

MaxH

Well yes, if it allows me to only involves the rules you listed in your post, then it appears I can't

user21820

I suspect that you did not really read through every single line of my example and look at the corresponding rule. Is that correct?

I purposely gave that example to show you how to use the rules involving ⇒,∧,∨.

MaxH

10:05

I read through at least half of it but not entirely through, yes. I thought I could adapt out of context.

user21820

No, please go back and make sure you read every single line. I don't waste time typing things that I don't think you should read.

If you knew programming, I could make the rules more precise, but you don't know programming...

MaxH

What does this mean and why is this written where it is? "B∨C. [restate]" (pretty far down).

You already know B or C, why mention it again?

Is it just a sort of summary?

You prove something if B is true and something if C is true, thus, in summary, if B or C is true this is also because of the implications?

user21820

@MaxH Exactly why I included it. See? I told you that you need to go through the whole thing. The ∨elim rule requires the preceding 3 lines to match exactly those 3 before you can write the line labelled ∨elim.

MaxH

If that is the casethen I would have thought it is redundant if I would not have seen you writing it down.

user21820

That's why you need the restate rule in order to get those lines there.

MaxH

10:16

Ok, so it appears to be rather technical? Did I overread something where you mentioned this? And with match you mean the indentation, right?

user21820

@MaxH It's right there in the description of the notation itself. By "match" it literally means exact match. Not just the indentation but the exact format.

Just look at the ∨elim rule; it requires the previous 3 lines to look exactly like shown in the rule.

> if the last lines you have written match "X" then you can write "Y" immediately after that at the same level of indentation

It's not really possible to get any clearer than this in English.

MaxH

Yes I think I get that now.

user21820

Good!

So now can you see how the restate rule is a precise formalization of what it means to "already know a previous line" and hence "be able to use it again"?

MaxH

Elim is supposed to mean elimination I suppose? So this rule is supposed to be read: If I have A or B and I have A implies C and B implies C, then I can conclude A or B implies C, right?

user21820

Sorry I see that I didn't actually say what "intro" and "elim" meant in that post haha!

MaxH

10:21

@user21820 Im not sure I fully understand that yet, but I hope I know how it works now.

user21820

@MaxH It's almost correct; I won't say "I can conclude A or B implies C". Rather, you literally can conclude "C", because you already have A∨B, and the implications A⇒C and B⇒C.

MaxH

@user21820 Well, that is pretty obvious, though. However, I would still say that the reason I can do what I can do is rather intuition and experience than the rules.

@user21820 Yes, I see.

(A or (B and C)) iff (A or B) and (A or C)
	If A or (B and C)
		A or (B and C)
		If A
			(A or B)
			(A or C)
		(A or B) and (A or C)
		If B and C
			(A or B) and C
			(A or B) and (C or A)
			(A or B) and (A or C)
		A or (B and C)
		A implies (A or B) and (A or C)
		(B and C) implies (A or B) and (A or C)
		(A or B) and (A or C)
	A or (B and C) implies (A or B) and (C or A)

Would this be better?

user21820

@MaxH First error is at "(A or B) and (A or C)". Not at the same level of indentation.

Second error is "(A or B) and (C or A)". This one you used intuition, but the rule never allowed you to only work on a part of the line. As I said, match exactly.

The first error is easily fixed. For the second error you'll have to figure out how to do something first so that you can apply a rule that lets you get from "C" to "C or A".

MaxH

Maybe I can make clearer what I don't understand about the rules with the following. Consdier the not(elim) rule. You wrote A and not A leads to the conclusion "contradiction". I have no idea what this means or in what way this makes sense. Again, I don't think I understand what it means if something is written above the bar.

@user21820 Ok, the indentation will be a problem for a bit more time, since I feel like I did not yet fully get it. Let me see...

user21820

@MaxH Oh don't look at negation yet. Make sure you understand the rest first.

MaxH

10:28

Ah okay, so I would have to indent taht one a bit more and write A implies (A or B) and (A or C) after that with the same indentation as "If A", right?

user21820

Correct!

MaxH

If so, then I have to admit I only know this because I looked at your example

user21820

@MaxH That's what the example is for! =)

MaxH

It is not yet transparent to me what logic underlies this notation, I guess.

Yes, but it would feel more satisfying and probably avoid mistakes, if I did notonly know how to use it but rather why. BUt perhaps that is too advanced.

user21820

@MaxH No it's not advanced at all; it's the core of 100% logical reasoning. The ultimate goal of Fitch-style is that every sentence you write down is true in its context.

> The context of each statement is specified by all the headers that are in effect.

So under the "If A:" you could deduce "A or B" and "A or C" and hence also "(A or B) and (A or C)". You can't necessarily do that outside. But you can just outside the "If A:" deduce "A implies (A or B) and (A or C)".

MaxH

10:32

If B and C
			(A or B) and C
				(A or B)
				C
				C or A
				(A or B) and (C or A)

Is this a fix for the second error?

user21820

I don't know where you got "(A or B) and C" from. Sorry this was error 1.5 and I missed it because I was focusing on the more obvious error.

But it's correct that you have to apply ∧elim to break up B∧C to get C and then apply ∨intro to get C∨A.

But why you want that, I don't know, since you can get A∨C instead.

MaxH

Oh I think this is a new error.

One that I only included in the "fix"

Nevermind.

user21820

It was there in the original because you forgot to change after realizing "A or B and C" is not "(A or B) and C".

MaxH

Yes.

I saw it now too.

user21820

But of course I'm sure you know how to fix it.

MaxH

10:35

Oops.

(A or (B and C)) iff (A or B) and (A or C)
	If A or (B and C)
		A or (B and C)
		If A
			(A or B)
			(A or C)
		(A or B) and (A or C)
		If B and C
		B
		C
		B or A
		A or B
		C or A
		A or C
		(A or B) and (A or C)
	A implies (A or B) and (A or C)
	B and C implies (A or B) and (A or C)
	A or (B and C) implies (A or B) and (A or C)

I hope this is better now

Im not sure if I have to write "A" after "if A" or if it is rather redundant.

Prithu biswas

12:02

@user21820 I asked the question because:
I know that x^2 means x.x , x^3 means x.x.x.
But x^n could mean x.x.x....x [n times]
But Isn't the "..." non-rigorous?
That is why I asked the question.
[Note : I wasn't aware that you and F.Zer had a discussion about this earlier =)]

user21820

@MaxH Still didn't fix your first error. Also, how can you write "B"? Where did it come from? The line before that did not say "B and C"!

At your stage, please follow the punctuation strictly as well; put the ":" at the end of a header, and a "." at the end of a statement.

@Prithubiswas You're absolutely correct; the "..." requires induction/recursion, hence what I said just now.

If you only want a specific natural power, like ( ℝ x ↦ x·x·x ), you can clearly do that as I just did.

But clearly you're asking about having the natural power as an input, in which case there is no choice but to use induction/recursion. Note that recursion requires a tiny bit of set theory; this is unavoidable in any foundational system based on set theory.

@Prithubiswas: Do you want to see the approach using recursion?

MaxH

12:22

@user21820 Oh okay, does this fix the first error, or am I still getting something wrong?

A or (B and C)) iff (A or B) and (A or C)
	If A or (B and C)
		A or (B and C)
		If A
			(A or B)
			(A or C)
			(A or B) and (A or C)
		A implies (A or B) and (A or C)

@user21820 So is this an indentation error? Because if I have B and C, I surely have B (I guess I need to indent B).

user21820

@MaxH Yes no error now. But as I said, stick to the full punctuation. It's not an idle syntax; it allows line-breaking with no ambiguity.

MaxH

@user21820 Yes, I read that too late, I will try to include it.

@user21820 Why is there no dot after B (in the If B: case)?

user21820

@MaxH Yes, again, the ∧elim rule lets you get "B" from "B and C" only at the same indentation level.

@MaxH Because I made an error. And also later on the "C".

MaxH

(A or (B and C)) iff (A or B) and (A or C)
	If A or (B and C):
		A or (B and C).
		If A:
			(A or B).
			(A or C).
			(A or B) and (A or C).
		A implies (A or B) and (A or C).
		If B and C:
			B.
			C.
			B or A.
			A or B.
			C or A.
			A or C.
			(A or B) and (A or C).
		B and C implies (A or B) and (A or C).
	A or (B and C).
	A implies (A or B) and (A or C).
	B and C implies (A or B) and (A or C).
	A or (B and C) implies (A or B) and (A or C).

I hope this is correct hen

Sorry for the tons of mistakes.

user21820

The punctuation is also to remind you that headers are headers and statements are statements. Obviously, once you can use the system, you can do it mentally and in your mind you can of course discard all this syntax. But for the purpose of understand how the system works without any human intuition, it's best to follow the rules precisely.

@MaxH It's almost correct; your only error is the indentation of "A or (B and C)." and two lines after that. And so you're also missing a line after those two.

MaxH

12:31

Ah, yes I see.

Prithu biswas

@user21820 Sure I want to see the approach using recursion.

user21820

@MaxH There's no problem with making errors; it's the same as how people learn programming; they run the compiler and it says "syntax error". =)

MaxH

Sorry, that was not careful enough.

@user21820 Yes, as far as I see it, the mistakes I make are rather specific to the notation/system, not the understanding/logic, which is hopefully not too bad.

Thank you for understanding and being patient.

user21820

Exactly. Learning a deductive system is much simpler than learning programming because you only have to get syntax right. Programming requires you to actually write a program that does what you want. But formal proof only requires that you follow the syntax/deductive rules.

MaxH

Technically, though, we are using quantification and variables even right now, aren't we?

A, B and C are placeholders for statements and we do it for arbitrary statements.

user21820

12:35

@Prithubiswas: Sure, give me a moment.

@MaxH Actually, no. the propositional atoms in PL can be considered as 0-input predicate-symbols. There is no need for variables, nor quantifiers.

MaxH

@user21820 I fear I don't really know what that means.

user21820

@MaxH For now, just do not think of those A,B,C as variables, because they are not. They are arbitrary statements given right at the beginning.

MaxH

Ok.

Thats the way I have been thinking about them, I just don't see why they are something other than variables, but I will stick with it then.

user21820

@MaxH Your intuition is half-correct. A PL proof is useless in a vacuum. When you use a PL proof in the real world, you interpret each atom to be some specific statement about reality. But that interpretation is not and cannot be mathematics.

Also, in FOL one is not allowed to quantify over statements, so we really cannot treat PL atoms as being quantified over. Later you'll see what I said about 0-input predicate-symbols when we get to FOL.

MaxH

12:55

(A or B) and (B or C) and (C or A) implies (A and B) or (B and C) or (C and A)
	If (A or B) and (B or C) and (C or A):
		A or B.
		B or C.
		C or A.
		If A:
			If B:
				A and B.
				(A and B) or (B and C).
				(A and B) or (B and C) or (C and A).
			B implies (A and B) or (B and C) or (C and A).
			If C:
				A and C.
				(A and C) or (B and C) or (A and B)
			C implies (A and C) or (B and C) or (A and B).
		A implies (A and B) or (B and C) or (C and A).
		If B:
			If C:
				B and C.
				(B and C) or (A and C).

This is (P2). I have some question regarding it, though, but I need to think about how to formulate it.

I think its better if you check for errors first, maybe I made an error that is connected to the question I have.

Thank you in advance.

user21820

@MaxH Well, I forgot to mention that the precedence rules also allow dropping brackets for a chain of "∧" or a chain "∨". Of course, you know this intuitively. But formally you must realize that it is entirely because you can get ( A∧(B∧C) ⊢ (A∧B)∧C ) and the other way around, and similarly for ∨.

MaxH

I dont know what "⊢" stands for.

user21820

"X ⊢ Y" is the 1-line version of the rule syntax with "⊢" in the middle and X on top and Y below.

MaxH

Ok, but essentially you never explained what that means either. I assume that it means something like "If X holds, Y can be concluded".

But again, I treated this with intuition, rather than certainty.

user21820

The rule only says what it allows you to write. In itself it is meaningless. It just happens that we believe that they are meaningful because of:

3 hours ago, by user21820

@MaxH No it's not advanced at all; it's the core of 100% logical reasoning. The ultimate goal of Fitch-style is that every sentence you write down is true in its context.

MaxH

13:04

Ok, I think (and hope) I get it.

user21820

So this is why there are many variant Fitch-style systems. The only thing in common is this ultimate goal.

This bolded goal is called soundness (with respect to the PL semantics).

PL semantics are how we evaluate the truth-value of a statement given truth-values of all the atoms.

You can check the rules one by one and see that each rule is sound, meaning that if all previously written statements are true in their context, then the statement that the rule permits you to write is also true in its context.

This rule-by-rule soundness guarantees global soundness, which is the ultimate goal.

Take the ⇒sub rule, for example. It says that if the previous line is "If A:" then I can write "A" indented just underneath that. Why? Clearly, "A" is true in the subcontext where "A" is true...

MaxH

Ok, I have the feeling this makes me understand all the rules of your post except for the "not" rules. However, I had the feeling I understood them intuitively before.

user21820

Good! We come to the ¬rules later. Firstly we have to fix your attempt of one direction of (P2), and you still have to do the other direction for (P1).

MaxH

Sure.

user21820

@MaxH Where does "A implies (A and B) or (B and C) or (C and A)." come from?

MaxH

13:10

Yes I do, however I wanted to try something else. I will do the other direction for sure, just wanted to see.

@user21820 I have to write A and (B or C) implies ..., right?

user21820

No? Follow the ⇒intro rule; it doesn't allow you to do anything close to that.

And in fact, at that point you violated the ultimate goal; that statement is not true in its context, which is "If (A or B) and (B or C) and (C or A):".

So if you want to use your intuition to help, you can check that you believe every statement is true in its context.

If you don't, then you must have broken some rule somewhere.

MaxH

So I have proven that If A and B hold, I get (A and B) or (B and C) or (C and A). As well as if A and C hold I also get (A and B) or (B and C) or (C and A). which matches intuition.

user21820

@MaxH Yes but the line after those come from nowhere.

MaxH

Yes, that was also the line I was concerned about, actually.

Or rather one of them

So is the correct thing: A implies (B implies (A and B) or (B and C) or (C and A) or C implies (A and B) or (B and C) or (C and A))?

If not then I might have some misunderstanding

user21820

Also, "A and C" ≠ "C and A". The system doesn't care about your belief of commutativity of "and".

MaxH

13:18

@user21820 So what does this mean as a consequence? Does the order of statements just not matter? Because if it does, then I think I need commutativity here, don't I?

user21820

I made a mistake earlier; your statement was actually true in its context; I'm not sure how I thought it wasn't, perhaps because of the syntax error.

But it remains the case that you didn't use the ⇒intro rule correctly.

@MaxH It just means that you cannot treat two lines the same unless they are literally identical.

MaxH

I might be confused now. Just to make sure, the intro rules, introduce a new symbol, meaning in this case, I can write "implies" if I can write what is above the bar in the rule, right?

user21820

@MaxH Yes, but you do not have what the rule requires!

You have "If A:".

MaxH

So "A implies (B implies (A and B) or (B and C) or (C and A) or C implies (A and B) or (B and C) or (C and A))" is not correct either?

user21820

At that point, no. Just tell me what the rule requires you to have written above in order to write "A implies (A and B) or (B and C) or (C and A).".

MaxH

13:22

I need to have:

If A
	...
	(A and B) or (B and C) or (C and A).

user21820

Exactly.

But you don't.

MaxH

According to the rule, or am I getting something totally wrong?

OK.

Let me see..

user21820

So work backwards to see what you need to do in order to get what you need.

MaxH

Ok so I think I should get: A implies ((B or C) implies (A and B) or (B and C) or (C and A))?

user21820

@MaxH But that isn't what you want! You do want "A implies (A and B) or (B and C) or (C and A)." just outside the "If A:".

And you just told me exactly what you need in order to get that.

That's all correct. So you must figure out how to actually get it.

MaxH

13:28

Wait, I think I am confused. Give me a second.

Just for my understanding: I have something like:

If A
	If B
		P
	If C
		P
	B implies P and C implies P
A implies (B implies P and C implies P)

Right?

Just think of it out of the context of the exercise, for general understanding.

user21820

Yes that's right (if you fix the missing brackets). But that's not what you want.

MaxH

Yes, just for the purpose of understanding.

Ok, let me see.

user21820

"B implies P and C implies P" means "B implies ( P and C ) implies P" which I consider syntactically invalid because you can't have two "implies" in a row.

MaxH

@user21820 It comes from the case analysis: I know that B or C is true. Now if B is true I get the desired result and if C is true I also get the desired result. Hence with v elim I should get A implies the desired result in total.

@user21820 So my example is actually incorrect?

user21820

13:48

@MaxH Correct if you fix the brackets. My last messages tells you the meaning of what you wrote, which is not what you meant to say. I know what you meant to say, which is correct.

Anyway you want:

25 mins ago, by MaxH

If A
	...
	(A and B) or (B and C) or (C and A).

So just figure out how to get it. It is possible, and is part of the solution. And don't think too complicated. Look at all the rules available to you.

@Prithubiswas Here is the rigorous definition in full. To make our life easier, we shall first make some syntactic sugar. Let "( S x , T y ↦ E(x,y) )" be short-form for "( (S×T) p ↦ E(first(p),second(p)) )" for any 2-parameter expressions E, where first and second are the projection function-symbols I defined earlier.

The basic recursion theorem is:

> Recursion theorem: ∀S∈set ∀c∈S ∀f∈S→S ∃g∈ℕ→S ( g(0) = c ∧ ∀k∈ℕ ( g(k+1) = f(g(k)) ) ).

From this we can prove:

> Parametrized Recursion theorem: ∀A,S∈set ∀c∈A→S ∀f∈A×S→S ∃g∈A×ℕ→S ∀x∈A ( g(x,0) = c(x) ∧ ∀k∈ℕ ( g(x,k+1) = f(x,g(x,k)) ) ).

Proof:

Given A,S∈set and c∈A→S and f∈A×S→S:
	Let f' = ( (A→S) h ↦ ( A x ↦ f(x,h(x)) ) ).
	f' ∈ (A→S)→(A→S).
	Let g'∈ℕ→(A→S) such that g'(0) = c ∧ ∀k∈ℕ ( g'(k+1) = f'(g'(k)) ).  [recursion]
	Let g'' = ( A x , ℕ k ↦ g'(k)(x) ).
	g'' ∈ A×ℕ→S.
	Given x∈A:
		g''(x,0) = g'(0)(x) = c(x).
		Given k∈ℕ:
			g''(x,k+1) = g'(k+1)(x) = f'(g'(k))(x) = f(x,g'(k)(x)) = f'(x,g''(x,k)).
	∀x∈A ( g''(x,0) = c(x) ∧ ∀k∈ℕ ( g''(x,k+1) = f(x,g''(x,k)) ) ).
	∃g∈A×ℕ→S ∀x∈A ( g(x,0) = c(x) ∧ ∀k∈ℕ ( g(x,k+1) = f(x,g(x,k)) ) ).

And then to get natural exponentiation for reals:

Let c = ( ℝ x ↦ 1 ).
c ∈ ℝ→ℝ.
Let f = ( ℝ x , ℝ y ↦ x·y ).
f ∈ ℝ×ℝ→ℝ.
Let pow∈ℝ×ℕ→ℝ such that ∀x∈ℝ ( pow(x,0) = c(x) ∧ ∀k∈ℕ ( pow(x,k+1) = f(x,pow(x,k)) ) ).  [parametrized recursion]
Given x∈ℝ:
	pow(x,0) = 1.
	Given k∈ℕ:
		pow(x,k+1) = f(x,pow(x,k)) = x·pow(x,k).

@Prithubiswas: Let me know if any step is unclear.

Also, let me know if you wish to see a proof of the recursion theorem. It's the only part that 'truly' needs ST, since as you can see I did not use any ST in the rest except for function-notation.

MaxH

Im not sure but is this correct now:

oh it didnt fix font

Let me see.

(A or B) and (B or C) and (C or A) implies (A and B) or (B and C) or (C and A)
	If (A or B) and (B or C) and (C or A):
		A or B.
		B or C.
		C or A.
		If A:
			If B:
				A and B.
				(A and B) or (B and C).
				(A and B) or (B and C) or (C and A).
			B implies (A and B) or (B and C) or (C and A).
			If C:
				A and C.
				(A and C) or (B and C) or (A and B)
			C implies (A and C) or (B and C) or (A and B).
			B or C.
			(A and B) or (B and C) or (C and A).
		A implies (A and B) or (B and C) or (C and A).

Essentially I added the above.

user21820

@MaxH It's better (no more error involving ⇒intro), but as I said earlier "A and C" ≠ "C and A".

So you need to modify your steps slightly so that you get exactly what you want.

MaxH

14:04

@user21820 True, I need to reread that, because I feel like I didn't fully understand it.

But other than that, the crucial thing was the B or C that was missing, right?

user21820

@MaxH Right, you need to use the ⇒restate rule to 'pull it into the subcontext'.

MaxH

Ok. I hope Im getting there slowly.

user21820

Sure.

Ok I got to go. Bye for now!

MaxH

Bye and thanks for all the help!

MaxH

16:17

@user21820 I did two more.

(A implies notB) and B implies notA

If (A implies notB) and B:
	A implies notB.
	B.
	If not(notA):
		A.
		B.
		A implies notB.
		If A:
			notB.
		contradiction.
	notA.
(A implies notB) and B implies notA.

not(A and B) iff notA or notB

If not(A and B)
	not(A and B).
	If not(notA or notB).
		not(notA or notB).
		If A:
			If B:
				A and B.
				contradiction
			notB.
			not(A) or not(B).
			contradiction.
		notA.
		notA or notB
		contradiction.
	notA or notB.
not(A and B) implies notA or notB.

But since those are with negation, I am not sure. Hopefully not too many mistakes.

F. Zer

21:11

@user21820 Could you check if this proof is correct ?

Prove Strong induction from Well-ordering:
  If ∀k ∈ ℕ ( ∀i ∈ ℕ ( i < k ⇒ P(i) ) ⇒ P(k) ):
    If ¬∀k ∈ ℕ ( P(k) ):
      ∃k ∈ ℕ ( ¬P(k) )
      Let m ∈ ℕ such that ¬P(m) ∧ ∀k ∈ ℕ ( ¬P(k) ⇒ k ≥ m ) [well-ordering]
      ∀i ∈ ℕ ( i < m ⇒ P(i) ) ⇒ P(m)
      ¬∀i ∈ ℕ ( i < m ⇒ P(i) )
      ∃i ∈ ℕ ( i < m ∧ ¬P(i) )
      Let a ∈ ℕ such that a < m ∧ ¬P(a)
      ¬P(a) ⇒ a ≥ m
      a ≥ m
      ⊥
    ∀k ∈ ℕ ( P(k) )

Transcript for

♦ $Mathematics$ Basic Mathematics

Transcript for

♦ Basic Mathematics

♦ $Mathematics$ Basic Mathematics