logic question

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”.

logic question

@otini What's the system you've introduced in the class ? 1st order logic ? Do you have quantifiers ? What's the whole set of rules ?

re: logic question

@alice Only TRUE, FALSE, propositional variables (A, B, etc.) and the connectives “and”, “or”, “not”. No quantifiers.

The rewritings I've introduced are double-negation elimination and the De Morgan laws, but I would be curious to know if it's possible with any set of rules.

re: logic question

@otini Isn’t that way too small a system of rewriting rules ? I don’t even know how you’d rewrite : `A ∨ ¬A` into `True`.

If we consider the depth of the tree representing the expression as a norm on the formulas.

Double-negation : you can apply it on the whole expression but that makes it bigger. You can apply inside the ∨ on any of the As but that makes it as deeper and doesn’t change the symbol at the root of the expression.

De Morgan’s laws can yield only

``¬(¬A ∧ A)``

which, again, is deeper/bigger plus the term inside the parenthesis is completely analogous to the initial formula (by symmetry between ∧ and ∨ in the system) so we’ll succeed in reducing it (to False) exactly if we succeed in reducing the original one to True (so we’re not getting any closer to our goal).

No, I really think you can’t even reduce that trivial tautology. You can prove it’s a tautology by devising a truth table and checking all the 2^n cases (only 2 here, still feasible, but we know that won’t scale well), but I don’t see any way to reduce it to True with those «calculus rules».

re: logic question

@alice You're right, this set of rules is not enough. Perhaps by adding A ∨ ¬A = True?

re: logic question

@otini You'll probably also need axioms for commutativity, introduction and elimination rules for either ∨ or ∧ to make it complete.

For instance, here are a bunch of minimal sets of axioms for propositional logic, maybe something like Russel-Bernays' axioms + DeMorgan could work?
https://en.wikipedia.org/wiki/List_of_Hilbert_systems#Negation_and_disjunction
@alice

re: logic question

@carolynn @alice So what I see from Wikipedia pages about propositional logic is that it is complete in the sense that every tautology must be derivable, but for me it does not immediately imply that T can be derived from every tautology.

re: logic question

@otini Hmm, if we assume the axioms all derive to T, and semantic completeness means that every tautology is derivable from the axioms, then it seems to me it is the case?
Or do you mean "can be derived" in a computable sense? @alice

re: logic question

@carolynn @alice Yes I do, by “deriving” I mean obtaining T from a tautology by applying a finite sequence of rules.

logic question

@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.

re: logic question

@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.

re: logic question

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

re: logic question

@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.

re: logic question

@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.

re: logic question

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

re: logic question

@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

re: logic question

@namark @otini isn't xor just addition?

re: logic question

@loke
Yes it's common to look at it as addition, but don't think @otini introduced it as one of the rules yet.

re: logic question

@namark Oh, nice one! Thanks! The social network of the future: No ads, no corporate surveillance, ethical design, and decentralization! Own your data with Mastodon!