Переменным приписываются истинностные значения, а формула интерпретируется как функция от этих значений. Если эта функция всегда принимает некоторое выделенное значение "истина", то формула - тавтология.
Если так рассуждать, то, понятное дело, все аксиомы исчисления высказываний можно вывести (из таблиц значений логических функций

,

,

и

). Но эти рассуждения основаны на априорном допущении, что мы знаем всё про "истинностные значения" и заведомо способны вычислить значение любой логической функции.
Наверное, конструктивисты с таким допущением не согласятся. Скажем, неочевидна вычислимость логической функции

: Допустим,

соответствует недоказуемому и неопровержимому в арифметике предложению

. В стандартной модели арифметики мы можем считать

ложным (не существует такого
стандартного 
, что...). Однако

недоказуемо в арифметике, т.е. мы не располагаем средствами вычислить
правильное значение данного выражения (если считать, что все наши средства ограничены арифметикой), т.е. логическая функция отрицания оказывается "невычислимой".
Что-то мне кажется, что не все так просто.
Может быть. Но если теорема компактности формулируется таким образом, что из

следует, что существует конечное множество

аксиом теории

такое, что

, то, вроде бы, из

следует

, а значит и

.