Теорема дедукции в различных аксиоматиках

[evalquote]

Подскажите, пожалуйста, как принято использовать (и/или вводить) теорему дедукции в произвольных аксиоматиках исчисления высказываний.
Нужно ли для каждой аксиоматики заново строить доказательство, или предполагается,
что раз уж это аксиоматика исчисления высказываний, и правило вывода modus ponens, то можно его опустить?

Вот, например, есть задание, в котором три задачи, и все в разных аксиоматиках, вида:
"Пускай в аксиоматической теории высказываний Ln используются связки ∧,¬. Построить выводы следующих формул: ..."

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

Посоветуйте, пожалуйста, как поступить: доказывать её для каждой задачи заново?
А может быть я просто не понимаю каких-нибудь устоявшихся традиций в формулировке задач на эту тему?

[jetyb]

Вы можете ссылаться на теорему, но должны уметь, если вас спросят, ее доказывать.
Так принято даже на вступительных экзаменах.
А писать в решении доказательство(если не боитесь забыть) нецелесообразно.

[evalquote]

Спасибо за совет.
Просто, насколько я понял, теорема дедукции - это метатеорема касательно формальных теорий исчисления высказываний.
И для каждой теории её доказательство будет различаться - ввиду различного набора аксиом,
но, наверное, если в конкретной теории выводимы A→A и (A→(B→C)) → ((A→B)→(A→C)),
то автоматически становится применимым доказательство для классического исчисления высказываний с →, ¬.
Тем не менее, выводить эти две связки, да еще из одних только аксиом - каждый раз разных - тоже не очень удобно и иногда очень сложно,
но тем не менее, совершенно точно возможно - потому что это ведь исчисление высказываний всё-таки.