[FOM] Clean tautologies

[Robin Adams]

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:

> Hypothesis:
> 
> 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
> 
> tautology.

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

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