= Solution
\b[Yes, for <soundness> and completeness of <theoremhood>.] An <axiom-only complete propositional calculus> is obtained as follows. Declare every propositional <tautology>, and only such a <tautology>, to be an <axiom>; supply no <inference rules>. A <formal proof> then consists of a single <axiom>. Every proved <logical formula> is valid, giving <soundness>, and every valid <logical formula> is already an <axiom>, giving completeness.
This is not merely an unspecified collection: whether a finite <propositional formula> is a <tautology> is decidable by its finite <truth table>, so the <axiom set> can be recognized effectively. It is a deliberately uninformative <Hilbert proof system>, since all the work has been put into <axiom> recognition. If one instead asked for strong completeness of derivations from arbitrary additional assumptions, a system whose only <formal proof> lines are <axioms> or assumptions would not suffice; the affirmative construction here concerns $\vdash\phi$ versus $\models\phi$.
Back to article page
