[FOM] Clean tautologies
robin at cs.rhul.ac.uk
Thu Apr 22 11:35:24 EDT 2010
I am not aware of the concept of 'clean tautology' appearing anywhere else.
However, I expect there will be a connection to the concept of minimal
tautology. I notice that your example of an unclean tautology,
(a /\ (a -> a)) -> a,
is unclean because it is an instance of the (clean) minimal tautology
(a /\ b) -> a
On Tuesday 20 Apr 2010 20:35:40 Lucas Kruijswijk wrote:
> In a propositional proof system, if the axiom schemes
> are only instantiated to clean tautologies, then any
> theorem produced by the proof system, is also a clean
It depends on the rules of deduction of the proof system. If we have the ->
introduction rule of natural deduction, for example, then we can prove the
unclean tautology a -> (a -> a) without any axioms at all.
If you have in mind Hilbert-style systems, where the only rule of deduction is
Modus Ponens, then your hypothesis is true. What we must show is:
If P is a clean tautology, and P -> Q is a clean tautology, then Q is a clean
Proof: If we could replace variables in Q to obtain a tautology R, then P -> R
is a tautology, and so P -> Q is not clean.
Robin Adams <robin at cs.rhul.ac.uk>
Royal Holloway, University of London
More information about the FOM