# Proof within Łukasiewicz's infinite-valued logic $Ł_{א}$

Using the axiom system for Łukasiewicz's infinite-valued logic $$Ł_{א}$$, I need to construct a proof of the following:

⊢ (A → B) ∨ (B → A)

⊢ (A → (B → C)) → (B → (A → C))

A → B ⊢ (A ∧ C) → B

A → B ⊢ ¬B → ¬A

But i have no idea what to do... The best known axiom system for Łא has the sole rule of inference modus ponens, and the following axioms:

(A → B) → ((B → C) → (A → C))

A → (B → A)

(A → ¬B) → (B → ¬A)

((A → B) → B) → ((B → A) → A)

((A → B) → B) → (A ∨ B)

(A ∨ B) → ((A → B) → B)

¬(¬A∨¬B) → (A∧B)

At this point, any lead you have would be useful. I feel like whatever axiom rule i apply to these arguments I don't go anywhere, certainly not in the direction of proving them...

• Given that $A \lor B$ is pretty much defined as $(A \to B) \to B$ and all the axioms except the fourth and the last are constructively valid, many or most of these will come down to the fourth axiom and the last one. Unfortunately, that’s all I have for you since this one seems pretty hard. Apr 14 at 1:43
• This might not be easier, but maybe try proving (A → (B → C)) → ((A → B) → (A → C)) for the second problem. I haven't found a proof yet (is it true in this logic?) Apr 16 at 16:49
• @confusedcius: $(A \to (B \to C)) \to ((A \to B) \to (A \to C))$ is not provable in this logic (as you can see using the real-valued model discussed in the Wikipedia page in the link). Apr 16 at 20:12
• What is the context of your question? Finding proofs in this logic is generally extremely tricky. If you are being asked these questions as part of course-work, then you should have been given a lot of help. I also think you need the converse of your last axiom (otherwise $A \land B$ could just be always valid). Apr 16 at 20:31
• @RobArthan I'm not sure, but I remember studying Luaksiewicz's preferred axiom system for classical logic: "CCpqCCqrCpr, CpCNpq, CCNppp", saying something like the ability to prove anything other than Cpp seemed incredible or something like that. For that system, I think that the vast majority of theorems necessarily have to go through some of the consequences of 'CCpqCCqrCpr' by itself before they can get proved. I suspect that holds here also... we need to focus first on the detachable consequences of the wff we can call 'hypothetical syllogism' before doing anything else. May 5 at 2:51

To even start to prove the 1st conjecture ACabCba (this is Lukasiewicz's notation, also known as Polish notation), or the rule of inference Cab $$\vdash$$ CKacb, we need to apply the appropriate definition.

Axy gets defined as CCxyy, with CCxyy as what does the defining (the definiendum) and Axy as what gets defined (the definiens). To use the axioms in the greatest number of contexts (including computer usage using an automated theorem prover as an assistant perhaps), all well-formed formulas need translated so that any definiens in a well-formed formula gets replaced by its definiendum. More shortly, we can write Axy := CCxyy.

With ACabCba we have a definiens, with 'Cab' for 'x', and 'Cba' for 'y'. Now applying those substitutions to 'x' and 'y' in CCxyy, we can obtain that well-formed formula which needs to get proven from the following axioms which get suggested the Wikipedia page:

L1. CaCba

L2. CCabCCbcCac

L3. CCCabbCCbaa

L4. CCNbNaCab

For the rule of inference above, we can use the definition

Kab := NANaNb.

One thing to note about proving well-formed formulas in systems comes as that some axioms don't need another axiom to have a consequence which we can detach. For instance, with L4 it's antecedent has the form CNbNa. But, L4 does not have that form. In other words, there do not exist any substitutions for 'b' and 'a' such that CNbNa can get transformed to CCNbNaCab, because the second symbol of 'CNbNa', is an 'N', while the second symbol of 'CCNbNaCab' is a 'C'.

However, some well-formed formulas can always produce a detachable consequent after substitution. Consider L1 for example. It has 'a' as it's antecedent. Every single last well-formed formula can get thought of as being an instance of that well-formed formula. We can substitute any well-formed formula for 'a'. Consequently, some well-formed formula of the type Cba can always get detached from some well-formed formula of the type CaCba, where 'a' consists of some well-formed forumla already assumed or proved.

That might not seem very useful, and I guess it probably isn't for these problems. However, we still have more axioms to consider. Take a look at L2:

CCabCCbcCac.

Well, every single last wff has the type Cab. So, what if CCabCCbcCac were our sole axiom?

Well, we might substitute 'a' with 'Cab' and 'b' with 'CCbcCac'. We could then detach another wff. But, note that if we do so, then the 'c' from 'CCbcCac' ends up becoming the same 'c' as we got from the substitution 'CCbcCac'. Can we deduce something with more variables?

Instead of starting with just one axiom, let's start with two! But, of course, note in any way that we violate any rules. So, let's start with 'CCabCCbcCac' and 'CCdeCCefCdf'. And for the moment, if necessary, shun anyone who wants to insist that such wffs are the same since they "isomorphically equivalent", or "alpha equivalent", or some such talk. Now, we can substitute 'a' with 'Cde', and 'b' with 'CCefCdf'. Symbolically, we can write a/Cde and b/CCefCdf. Then we can write the following:

L2 CCabCCbcCac
L2 a/d, b/e, c/f * 3


were '' indicates that the intended wff on the left of the '' matches that on the right hand side of it.

3 CCdeCCefCdf
L2 a/Cde, b/CCefCdf * 4
4 CCCdeCCefCdfCCCCefCdfcCCdec
4 * C3-5
5 CCCCefCdfcCCdec


where Cx-y means that we have a wff that starts with 'C', has 'x' already in the list of wffs in the theory, and 'y' as the detached wff.

For the next part, why have one wff CCCCefCdfcCCdec when you can have two instead? We can write 6 CCCCzyCxyvCCxzv.

I suggest you take 5 and 6 and see what you can deduce from them while doing as little substitution as possible.

Then, go back to the other exercises, and see if the above helps solve some of them.