Logic Theory Proof

[loud topaz]

Definitions:

A demonstration in logic theory is a sequence of propositions where each element B must satisfy one of these conditions:

It is an axiom, OR
It comes from two previous elements in the form of: "A => B" and "A"

A theorem is any proposition that can be written in a demonstration.

Given Axioms:

(A or A) => A
A => (A or B)
(A or B) => (B or A)
(A => B) => ((C or A) => (C or B))

Problem:
Prove that if A => B, then (B => C) => (A => C)
In other words, prove: [A => B] => [(B => C) => (A => C)]

Note
A => B
Is same as : not A or B

P.S.
A logic is where each term can either has to be True or False.

Thanks @cinder tangle For this question

[dreamy parrot]

wait why is there an arrow inside the first term in the fourth axiom
seems irrelevant

[distant hatch]

xd this is just brute force-able

just write a truth table, there's only 8 options

ig that's not using the axioms though

[cinder tangle]

It is meaning you have axioms that define truth tables ! The only thing we allow is : A => B is noA or B

[cinder tangle]

I mean everything in logic is "logic" and always true :p

[sleek patio]

wait we are given $(A \implies B) \implies (B \implies C \implies A \implies C)$. surely it comes from this plus some substitution with earlier axioms

[cinder tangle]

The better is to publish every logic theorem you find so that you store it for later ! You'll need some other in between theorems but there are multiple roads ! It is not expected to see the path right away.

[proven loom]

This would be a possible proof only using the 4 axioms, the additional note and the fact that not(not(B)) <=> B

So you don’t really need any in between theorems

[cinder tangle]

Well played ! You have the proof with every theorem needed to be proved in between, the actual formal proof is longer though ! Would you like to try to give it a formal approach ?

[cinder tangle]

Well you can't use anything else than the 4 axioms ! So if it's provable as the question says it is, then it is effectively proveable with the 4 axioms

[proven loom]

The note that was used in my solution is literally the definition of the „implies“ relation, so I assume you mean the proposition of not(not(B)) <=> B that is missing for the complete solution?

[cinder tangle]

But you didn't just use the 4 axioms. You assumed no(noB) <=> B that you did without proving it ! You also lack one thing, you proved (A = > B) => (B or no A ) => with a very long chain but we only want (A => B) => (B=>C) => ( A => C)

[cinder tangle]

Yes and the just other thing I said, which is normally the first step, and then there is the rigor !

But you figured it all out, well played !

[proven loom]

Are you saying that it is also not allowed to consider [(A=>B) and (B=>C)] => [A=>C]?

And I assume the first step you are referring to is the fact that I didn’t write a „to be proven“ statement? Or is there something else missing in the beginning?

[cinder tangle]

Well in fact that's you get if you assume A => B
B=> C

We only want something that is true for every A, B, C

So we wouldn't make a claim that can be false one time so in fact all the logic theorems don't give us hints of the truthfulness of A or A=> B

[cinder tangle]

This is the first step I was talking about !

The question is not hard, it is hard when you are rigorous to the end.

[cedar wyvern]

oh wait i just realized, we're only allowed to go through the given axioms and not through normal logic rules right

[cinder tangle]

Yes

That is why it is logic theory proof

The question starts on the definition of what is a demonstration and what is a theorem

In the end the definition of a demonstration and the 4 axioms prove all logic

[cinder tangle]

Yes it is ! I asked FC to add that in the question as not everyone knows the definition of imply

I didn't got the time to read :(

[cedar wyvern]

i didn't mean to send it yet lol

what can we use?

like is it a given that A v ~A is true?

it's not given as an axiom but it's how OR is defined

[cinder tangle]

No it is not given

[cedar wyvern]

[cinder tangle]

And or is just defined as it is true if one is true and falqe is both are false

Why should we assume A or no A true ?

[cedar wyvern]

can associativity/commutativity/de morgan be applied?

[cinder tangle]

Everything is given

So you can prove them

[cedar wyvern]

damn, ok

[proven loom]

Here is my proof for everything implies itself and then subsequently B => not(not(B))

The proof for chainability is still missing though

[cinder tangle]

😄

[cedar wyvern]

oh so like we can prove more stuff and then use that as part of the final proof?

im not familiar with formal proofs

[cinder tangle]

Yes

[cinder tangle]

Correct !

[proven loom]

For the chain proof, is it allowed to see the fact A and B <=> not(not(A) or not(B))
As a definition of the AND operator? Or are we not allowed to consider AND at all?

[cinder tangle]

You don't need to really use and as it is just a definition, but you have to prove the equivalence though. If you manage to prove the equivalence then you can use and as a simplification. You'll need to prove that A and B => A, A and B => B.

[proven loom]

How are we supposed to proof something like that if there is no axiom including AND?

[cinder tangle]

Because and doesnt really exist

And implies doesn't really exist

Implies is just : no or

And is just : no(no or no)

Only no and or exist

[proven loom]

I see, thanks

[cinder tangle]

Also the transitivity is done by the definition of a demonstration.

[proven loom]

So you mean we don’t need to proof transitivity at all? Then the proof for AND wouldn’t even be necessary

In the first place, the proof for De Morgan‘s law I could find needed transitivity as well, so I wasn’t really sure if it would be usable for proving transitivity

[cinder tangle]

Transitivity is a definition of a writing of a theorem. All you wrote is good but you don't separate the =>

The definition of a demonstration includes the modus ponens : A; A=>B; B

[proven loom]

So you mean I would theoretically only need to separate the statements, and I then I‘m done?

[cinder tangle]

Pretty much !

But be rigorous :p

[proven loom]

Then is it provable that A=>B=>C
is the same as A;A=>B;B=>C;C?
Or is that just an informal way of writing it?

[cinder tangle]

You need to write B between it

[cinder tangle]

Yes

It is an axiom !

[proven loom]

I see. Although I wonder why it is necessary to write it the complicated way then…

Mathematicians always seem to make their lives harder

[cinder tangle]

You are right

But then who will check that the reasonning is perfectly "clear" ?

[cinder tangle]

Because then you prove you can write it the easy way !

But it's way harder than this question

[cinder tangle]

I mean yes

The first thing you prove is that if you assume A => B, B=> C

You have A => C

[proven loom]

Can this be considered the full version then?

[proven loom]

Yeah that’s why I was asking about the AND earlier

[cinder tangle]

Because axiom 4, you choose (B=>C) => ((non A or B ) => (no A or C))

Yes !

Well done

[proven loom]

Thanks!

[cinder tangle]

||(A or A) => A
A => (A or B)
(A or B) => (B or A)
(A or B) => ((C or A) => (C or B))

((A => B) and (B => C)) => (A =>C))

"""" ((A => B) and (B => C)) => (A => C) """"

(B => C) => ((no A or B) => (no A or C))

we search to prove ((A => B)=>(noB => noC)) :

A => (A or A) ; (A or A) => A; A => A; (no A or A); (no A or A) => (A or noA); (A or no A); (noA or no(noA)); A => no(noA); (B => no(noB)) => ((noA or B)=>(noA or no(noB))); (noA or B) => (no A or no(noB)); (noA or no(noB)) => (no(noB) => noA); (noA or B) => (no(noB) => noA)

Which is (A=>B) => (no B => no A)

We assumed A=>B

A => B ; noB => noA; (no B => noA) => ((C or noB)=> (C or noA)) ; (C or noB)=> (C or noA); (noB or C) => (C or noB) ; (C or noA) => (no A or C); (C or no B) => (no A or C); (noB or C) => (noA or C)||

[cinder tangle]

You're welcomed ! Have you find it fun or boresome ?

[proven loom]

A mixture of both. But that’s why I love maths. It can be annoying to be very precise, but I always enjoy learning about the things we always assume as already proven. I study electrical engineering, so needless to say, in most cases we don’t even look at the proofs of the theorems we use

[lost wind]

I am 14 I do not know half of this🙏

[cinder tangle]

I'm a first year of engineering prep ! But I was burned out and during the last grade I did this useless precision instead of going to school

What year are you in electrical engineering ?

[proven loom]

Currently 3rd semester. The only time we needed logic was in one class where literally an entire list of different rules were given. Most of them were proven, but not in the „complete“ way (they basically assumed common sense)

[cinder tangle]

If I wanted to be more tiring I would not even assume !

Oops forgot the reply

To my solution

Yes ! I love to be able to prove common sense

But even logic has axioms, so it isn't rational to take logic as granted ( but we should take it for granted)

There is really no need to be that precise, but it is fun to get the skill to be so if needed !

[proven loom]

Exactly, that‘s what was so fun about this question

[cinder tangle]

Because the answer is found intuitively immediately !

I was really in meltdown today. It is 5 am for me

[proven loom]

But in some cases I honestly prefer not having to understand the proofs. The stuff we need for quantum mechanics is way too complicated and I honestly wouldn’t survive the exams if we were required to proof everything

[proven loom]

Yeah same for me lmao. I can finally go sleep XD

[cinder tangle]

Damn I prevented you sleeping :(

[cinder tangle]

I remember the formulas and the methods thanks to demos !

I forgot the know by heart

[proven loom]

Nah don’t worry. My sleep schedule is messed up anyways XD

[cinder tangle]

Where are you from ?

[proven loom]

Germany, but I study in Zurich

And you?

[cinder tangle]

France !

[proven loom]

Nice!

[cinder tangle]

You have school tomorrow ?

[proven loom]

Afternoon yes. But even if I don’t go, the lectures are recorded

[cinder tangle]

I don't have this chanve

[proven loom]

The nice thing about university is the fact you don’t have to worry about attendance

[cinder tangle]

I'm in a preparation class I HAVE to follow

[proven loom]

Poor soul

[cinder tangle]

I banned phones for weeks but today was too much I don't know why. Well we're flooding the solution chat. Good nigjt !

[proven loom]

Thanks! Good night!

[ashen sage]

I learned in logic class and idk this

Yeah idk where to start other than the "if A=>B" part

Do I have to start from the axioms?

[eager pond]

You probably do

My first thought was Boolean theorems but then I was like I bet he wouldn’t allow it

[forest cairn]

this kinda reminds me of hilbert type calculus

[ashen sage]

Probably, but thats not a format im too farmilliar with

[ashen sage]

Man idk where to go from here

[cinder tangle]

You can prove boolean theorems !

[eager pond]

I can’t stress this enough, but I don’t wanna

[cinder tangle]

Start proving the most you can, you can use assumptions to create =>; you can do small demonstrations showing the implications of the assumptions then you use the end result of the big implication

[ashen sage]

I try to do it using only the axiom given but Idk how but I know how to do it by implication chains

I guess de Morgan law is also not allowed lmao

[proven loom]

You can prove de Morgan, but it is harder than the actual solution. Also, I would recommend trying to go backwards along the chain, since it usually means that you essentially use the axioms to simplify instead of expanding the term. That’s how I solved the problem, and it’s my go to way for most mathematical proofs in general

[gleaming lake]

||Let us call the four axioms A1, A2, A3, A4. By substituting B, C, ~A for A, B, C in A4, we have (B => C) => ((A => B) => (A => C)). That is, if B => C is true, and if A => B is true, then A => C is as well. This is called hypothetical syllogism. Moreover, since A => A is true, "~A or A" is true; by applying A3, we have that "A or ~A" is true as well. By substituting ~A for A, we have "~A or ~~A", and thus "A => ~~A" is true; we will call this criteria 1. Let us substitute B, ~~B, ~A for A, B, C in A4; we have (B => ~~B) => ((A => B) => (A => ~~B)). Since B => ~~B is always true (criteria 1), we have that (A => B) => (A => ~~B) is always true. We shall call this criteria 2. By A3 we have (A => ~~B) => (~B => ~A), and by applying hypothetical syllogism to criteria 2 and the preceding application of A2, we have (A => B) => (~B => ~A); let us call this criteria 3. Finally, by substituting ~B, ~A, C for A, B, C in A4, we have (~B => ~A) => ((C or ~B) => (C or ~A)). Since A => B is given, by criteria 3 we have ~B => ~A; thus (C or ~B) => (C or ~A) is true. By trivial applications of A3 and hypothetical syllogism, we have (~B or C) => (~A or C); the proof is complete.||

[cinder tangle]

Perfet ! You just need to prove A => A but you can do it easily ! Well played :D

[distant hatch]

Lemma 0: [(A=>B) and (B=>C)] => (A=>C)
i refuse to do out notation for this
Lemma 1: A => A
A => (A or A) => A
Lemma 2: A => !(!A)
(!A=>!A) = (!(!A) or !A) => (!A or !(!A)) = [A=>!(!A)]
Lemma 3: (B or A) => [B or !(!A)]
[A=>!(!A)] => [(B or A) => [B or !(!A)]]
Proof:
(A=>B) = (!A or B) => [!A or !(!B)] => [!(!B) or !A] = (!B=>!A) => [(C or !B)=>(C or !A)] => [(!B or C)=>(!A or C)] = [(B=>C)=>(A=>C)]

@cinder tangle look fine?