I taught my first class in propositional logic today and one of the students asked a question I couldn't answer.

I had just presented De Morgan's laws and double negation elimination, and call them (rather informally) “calculus rules”.

They asked whether all tautologies could be transformed into the constant formula “TRUE” by applying a sequence of “calculus rules”.

I must say I don't know the answer. I know that every formula can be converted into either CNF or DNF, but I don't whether the CNF or DNF of a tautology is necessarily “TRUE”.

@otini what is a tautology? I thought it was things like 1=1,but that does trivially reduce to true, so I must be wrong on this.

@loke In the context of propositional logic, it's stuff like A or (not A), i.e. things that are true no matter what things like A stand for.

@otini OK, so what is the argument that these cannot be reduced to true? Seems pretty logical to me

@loke I am now able to make my question more precise: can they be reduced using only the transformations that I presented them (probably not, you need more), and is there an automated process to find such reduction sequence.

@otini @loke the automated process would be to transform it to Zhegalkin polynomial and proceed with usual rules of mod2 algebra.

X v !X
apply rule !X = X + 1
X v (X + 1)
apply rule X v Y = X + Y + XY
X + X + 1 + X(X+1)
distributive rule X(Y + Z) = XY + XZ
X + X + 1 + X^2 + X
powers are meaningless as XX = X
X + X + 1 + X + X
every number is it's own additive inverse in mod2! (aka most complicated way to say X + X = 0)
1

In context of boolean logic the addition here is exclusive or and the multiplication is conjunction.
To outline a more general algorithm: transform the negation and conjunction by those formulas above and open up all the parens. You will be left with a bunch of conjunctions stringed together with xor, very much like a normal polynomial but without powers, so basically just combinations of variables involved. Eliminate all the identical groups of conjunctions in pairs, and you will be left with 1 if it was a tautology.

@otini @loke transform the negation and *disjunction by those formulas -_-

@otini Come to think of it, if what you introduced is close enough to usual Boolean algebra, then since you can define xor as (X!Y v !XY), and derive all of it's properties, you can carry out all those derivations in place without the abstraction, but I imagine it's going to be an absolute nightmare.

@loke