CSL is classical logic. So I'm talking about the basic introduction and elimination rules (conditional, biconditional, disjunction, conjunction and negation).

I'm not talking about his infinite-valued logical theory, but the 3-valued one where any atomic sentence can be given T,F or I. (See the Wikipedia article here:



The usual natural deduction rules all hold if you view the context $\Gamma$ in a sequent $\Gamma \vdash A$ as a multiset rather than a set.

  • $\begingroup$ If this holds true, I think your answer would come as much better if you explained how conditional introduction works from the perspective of viewing Γ as a multiset. $\endgroup$ – Doug Spoonwood Aug 4 '13 at 23:29
  • 1
    $\begingroup$ Conditional introduction says that from $\Gamma, A \vdash B$, we can infer $\Gamma \vdash A \implies B$. So treating the context $\Gamma, A$ as a multiset, from $A, A \vdash A \land A$, we can infer $A \vdash A \implies A \land A$, but not $\vdash A \implies A \land A$. $\endgroup$ – Rob Arthan Aug 4 '13 at 23:59
  • $\begingroup$ I've seen different, but what you've said doesn't doesn't exactly contradict what I've seen also. Thanks for the information. $\endgroup$ – Doug Spoonwood Aug 5 '13 at 0:32
  • $\begingroup$ Alright, so thinking about it, you're right about the multiset interpretation it matches what I've seen well enough... if not comes as superior. But, what about some negation introduction and elimination rules. Those similar to conditional introduction change scope or "the domain" as Jaskowski would call it. How do we know those rules work here, or do they? $\endgroup$ – Doug Spoonwood Aug 5 '13 at 2:00
  • 1
    $\begingroup$ The most economical way of dealing with negation in Lukasiewicz logic is to treat $\lnot A$ as an abbreviation for $A \Rightarrow \mbox{false}$. $\endgroup$ – Rob Arthan Aug 5 '13 at 12:34

try it out by 3 valued truthtables :)

out of my head all except the conjunction introduction , negation elimination and negation introduction rule are valid . but i can be wrong

added after Comment by Spoonwood

The problem with the conditional introduction rule is that it is normally a discharging rule and in Lukasiewicz 3 valued logic

(P -> (P-> Q)) -> (P -> Q) (contraction) is not a tautology in Lukasiewicz 3 valued logic : (I use i instead of 1/2, the designated value is 1, * is the problematic line)

 P | Q || (P -> (P -> Q)) -> (P -> Q)  
 1 | 1 ||    1     1      1     1  
 1 | i ||    i     i      1     i  
 1 | 0 ||    0     0      1     0  
 i | 1 ||    1     1      1     1  
 i | i ||    1     1      1     1  
 i | 0 ||    1     i      i*    i  
 0 | 1 ||    1     1      1     1  
 0 | i ||    1     1      1     1  
 0 | 0 ||    1     1      1     1  

so you should just not be able to deduce it but using the standard conditional introduction rule you can:

1 ||___ P -> (P -> Q)               Assumption
2 |||__ P                           Assumption
3 |||   P -> Q                      1,2 Conditional elimination
4 |||   Q                           2,3 Conditional elimination
5 ||<   P -> Q                      2-4 Conditional introduction
6 |<    (P -> (P -> Q)) -> (P -> Q) 1-5 Conditional introduction

so the conditional introduction rule as used here is not a valid rule in Lukasiewicz 3 valued logic.

You could have a rule

if P then Q -> P (without discharging an assumption) but that is not the standard rule.

While writing this I was also wondering about the or elimination rule, it depends a bit which or elimination rule you use, some are valid some are not, the same applies to the Not introduction rule.

In general non-discharging rules are valid, discharging rules are not

  • $\begingroup$ This could use more clarification... what's the truth table for conditional introduction? $\endgroup$ – Doug Spoonwood Aug 4 '13 at 23:17
  • $\begingroup$ Lukasiewicz logic is an affine logic. In a natural deduction presentation using proof trees rather than sequents, this means that when you discharge an assumption you remove at most one occurrence of the assumption from the leaves of the proof tree. $\endgroup$ – Rob Arthan Aug 5 '13 at 23:03

There does exist some variation in what "basic rules" means in natural deduction systems. But, hopefully that won't pose too much of a difficulty here. I use Polish notation. I also write "out" for elimination, and "in" for introduction. Also, when writing rules I will improperly write them with object language variables. I'll do this for two reasons. I'll talk about a key meta-theorem below, as well as using this form, I believe, helps you to check rules of inference via truth tables easier. The matrix for this logical system can get represented as follows:

   q = E  |f  i  t|  C |f  i  t|  A  |f  i  t|  K  |f  i  t|  N
     p=f  |t  i  f|    |t  t  t|     |f  i  t|     |f  f  f|  t  
     p=i  |i  t  i|    |i  t  t|     |i  i  t|     |f  i  i|  i
     p=t  |f  i  t|    |f  i  t|     |t  t  t|     |f  i  t|  f

The conjunction out rules say:

1 "From Kpq as true, we may infer p as true." In order to check this rule semantically we want to check that "If Kpq evaluates to the designated value for truth, then p evaluates to the designated value for truth." Of course, the designated value for truth here is T. Do you now see how to check this by the table or do you need more information?

The other conjunction out rule says

2 "From Kpq as true, we may infer q as true."

The conjunction in rule says:

3 "From p as true, as well as q as true, we may infer Kpq as true." So, we want to check "if p evaluates to T, as well as q evaluating to T, then Kpq evaluates to T."

The alternation or disjunction-in rules say:

4 "From p as true, we may infer Apq as true."

5 "From q as true, we may infer Apq as true."

So, I hope you can do all of that yourself now.

6 (improper for this logical system) The alternation of disjunction-out rule often says something like this:

"From a derivation (or deduction) which starts with p and ends with r, as well as a derivation which starts with q and ends with r, as well as Apq as true, we may infer r."

That rule as stated probably doesn't work, because the conditional in rule doesn't work in a form that allows it to work as stated:

"From a set Γ, as well as a derivation which starts with p and ends with q, we may infer, with Γ still in place Cpq."

No, we can't do that as stated! At least not un-limitedly. You can't do that in Lukasiewicz's three-valued logic (you can do it in a 3-valued logic that Slupecki developed, and it does have a formal proof apparatus, and can still get used to define all three-valued connectives if you really want to do so). One way to know this comes as to come up with an axiom set which enables you to prove The (Classical) Deduction Meta-Theorem. This axiom set will work:

A1 CpCqp axiom (simplification)

A2 CCpCqrCCpqCpr axiom (self-distribution of Frege)

But, check the truth tables for these (or come with an algebraic argument that one of them fails). One of them is NOT a tautology here. I hope you can do this. So, you can't prove The (Classical) Deduction Meta-Theorem.

There does exist a modified rule, which qualifies as quite different:

"From a set Γ, as well as a derivation which starts with p and ends with q, we may infer, with Γ still in place CpCpq."

That all said, you do have a modified alternation out rule which you could use (and some authors do use) instead:

6 proper: "From Cpr as true, as well as Cqr as true, as well as Apq as true, we may infer r true."

Now, I do NOT feel this so easy to do by checking the truth tables since they only have two variables, and this rule has three. So, how do you check it?

First we want to talk about the conditional-out rule:

7 "From Cpq as true, as well as p as true, we may infer q."

So, I hope you can check that for yourself now (if not, I will clarify upon request!).

Once you have that you have that as rule, you can prove "one half" of what many authors call The Deduction Theorem (a metalogical theorem). But, especially for this logical system, as well as many other systems, I think it deserves a special name:

The Detachment Theorem: "If C$\alpha$$\beta$ holds as true, as well as $\alpha$, then $\beta$ holds true."

First I will emphasize, is not a rule of inference of the object language, it comes over and above conditional-out in some sense. It comes as a metalogical statement at present, and though I believe you can prove it yourself, it comes as far too important in my mind to not make it as clear as I can that it does hold as a metalogical theorem.

Proof: Suppose C$\alpha$$\beta$ true, as well as $\alpha$. Then, whatever well-formed formula $\alpha$ represents, by the conditional out rule, we may infer $\beta$. Notice both $\alpha$ as well as $\beta$ come as arbitrary well-formed formulas, not particular ones. Consequently by applying universal quantification introduction twice, we may infer $\forall$$\alpha$$\forall$$\beta$"If C$\alpha$$\beta$ holds as true, as well as $\alpha$, then $\beta$ holds true." (to any objection that claims that I've implicitly used conditional introduction I will respond that I have not done so, because the conditional introduction rule works on meaningless object language symbols... this uses "if ... then", and "if" as well as "then" are not in the object language.)

The domain of $\alpha$ and $\beta$ come as any propositional language which has a conditional-out rule. In my opinion at least, I could hardly overstate how powerful and important The Detachment Theorem is, not only in classical logic, but possibly even more so in multi-valued logic. In fact, I believe that were the founders of modern logic to ever imagine some great catastrophe which destroyed all the books on the planet which contain snippets of metalogic except for one metalogical theorem, they would almost unanimously, if not completely agree to choose this one. The upshot can hardly get understated. The upshot can get stated as:

For every propositional logical tautology or theorem of any system of propositional logic which contains "C" (or an "equivalent" symbol) as its principal connective with a conditional out rule (or modus ponendo ponens), or any system which has a propositional logic contained in it, we can derive at least one rule of inference, and often enough a few rules of inference.

Now, moving back to A-out rule, you can check that this holds as a tautology:

C Cpr C Cqr C Apq r.

Given that you've checked that as a tautology, due to the completeness and soundness results (in Luaksiewicz's "C" and "N" here), you can derive as rules of inference:

"From Cpr as true, we may infer CCqrCApqr as true." "From Cpr as true, as well as Cqr as true, we may infer CApqr as true."

And the next rule you can derive in this patten, gives you alternation out (or disjunction out).

Equivalence-out can get written:

8 "From Epq as true, we may infer Cpq as true."

Can you do this? (hint: note the diagonals of E and C).

Equivalence-in can get written:

9 "From Cpq as true, as well as Cqp as true, we may infer Epq as true."

So, due to the The Detachment Theorem if CCpqCCqpEpq holds as a tautology, we can derive rule 9 as a valid rule of inference (proof-theoretically we'll need some axiom set... usually only C and N get used here).

Negation in can get written:

10? "From a derivation which starts with p and which contains q, as well as Nq somewhere, we may infer Np."

I can't honestly answer you here. The problem comes as that such a rule changes scope just like the conditional in rule of most natural deduction systems. Such a rule talks about a derivation also.

11? Somewhat similarly, negation out can get written "from a derivation which starts with Np and ends with q, as well as contains Nq somewhere, we may infer p." Again, I can't quite tell.

That all said, you can check that:

C p C Np q holds as a tautology also, as well as C Np C p q.

The system is consistent.


1) I believe that Conditional introduction works: My experience is that the problem lies in getting a getting valid derivation from a set of premises, given the other rules that don't work.

2) Conditional elimination does not. This is the chief thing that cripples Lukasiewicz logic as a logic. Modus Ponens and the transitivity of the conditional both fail for the Lukasiewicz conditional, as they properly should, given that it allows conditionals with a value of I. If your conditionals are doubtful, you should not expect inference using them to be valid. (It is not generally known that this can be remedied: Define Spq as NCCpqNCpq and use that for the conditional)

3) Biconditional introduction works. 4) Biconditional elimination works. 5) Conjunction introduction works. 6) Conjunction elimination works
7) Disjunction introduction works.

8) Disjunction elimination does not work.
9) Negation introduction does not work. 10) Negation elimination does not work. Classically, 9 and 10 depend on the Law of the Excluded Middle, which doesn't hold in Lukasiewicz logic.

  • $\begingroup$ Semantically speaking, CCpqCpq is a tautology of Lukasiewicz logic, since Cpp is and uniform substitution works. Conditional elimination consists of the rule {C$\alpha$$\beta$, $\alpha$} |= $\beta$. Consequently, conditional elimination does consist of a valid rule of inference here. Conditional introduction does NOT work here. If it were, then both contraction "CCpCpqCpq" and self-distribution "CCpCqrCCpqCpr" would qualify as tautologies. $\endgroup$ – Doug Spoonwood May 13 '14 at 14:26
  • $\begingroup$ Given CCpqCpq and Cpq, it is then possible to conclude Cpq, but this is no more than was already given. I don't see how CCpqCpq permits conditional elimination in the more general case. I will agree that conditional introduction and elimination don't both work, and that contraction and self distribution fail as tautologies. $\endgroup$ – Confutus May 14 '14 at 1:32
  • $\begingroup$ First method, suppose that "if $\gamma$ |=C$\alpha$$\beta$, then {$\gamma$, $\alpha$} |= $\beta$". Thus, if we have |= CCpqCpq by one application of the hypothesis we have Cpq |= Cpq. By a second application of the hypothesis we have {Cpq, p} |= q. That is conditional elimination in semantic form. Thus, if |=CCpqCpq, then conditional elimination holds (given the above hypothesis). Without the hypothesis, the truth table tells us that where C$\alpha$$\beta$ holds true, and $\alpha$ holds true, that $\beta$ will also hold true also. In more detail 1/2 $\endgroup$ – Doug Spoonwood May 14 '14 at 1:43
  • $\begingroup$ If C$\alpha$$\beta$ holds true, then the pair ($\alpha$, $\beta$) belongs to {(T, T), (I, T), (I, I), (F, T), (F, I), (F, F)}. Now if $\alpha$ holds true, then the pair here must come as (T, T) since that's the only pair that works. Consequently, $\beta$ does hold true also. Therefore, conditional elimination "{|=C$\alpha$$\beta$, |=$\alpha$} |= $\beta$" works as a valid rule of inference. $\endgroup$ – Doug Spoonwood May 14 '14 at 1:48
  • $\begingroup$ Since CKpCpqq does not hold in Lukasiewicz logic, I would be doubtful about accepting the hypothesis "if γ |=Cαβ, then {γ, α} |= β" in the first place. The difficulty as I see it is in assuring that Cαβ is in fact true. I would be willing to accept "if γ |=Sαβ, then {γ, α} |= β" (with S as I have defined it above). $\endgroup$ – Confutus May 14 '14 at 2:21

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.