Using the terms 'theorem 'and 'tautology'

Question

I would just like some clarification on the use of the terms "theorem" and "tautology".

I have read here that a theorem is a "formula for which a zero-premise derivation has been provided". But here it is a "logical consequence of the axioms". These definitions seem to be in conflict, as are not axioms just premises (Formulae which are assumed to be true)?

And what about a tautology. My understanding is that a tautology is the same as the first definition of a theorem. Or is tautology a semantic thing (i.e. valid) whereas theorem is syntactic (i.e. derivable)?

Answer 1

In mathematics a theorem is a statement that has a proof : in a theory, i.e. from the axioms of the theory.

In a "formal" context, nothing change: a theorem of e.g. first-order arithmetic is a formula that is derivable from the first-order Peano axioms.

---

A valid formula (in the context of propositional calculus : a tautology) is a formula that is true in every interpretation.

Logical calculus have more than one "modes of presentation" :

Hilbert-style : (logical) axioms and rules

Natural deduction and Sequent-calculus : rules only.

In the first case, we say that a theorem of "pure" logic (like e.g. $\forall x \ (x=x)$) is a formula derivable form logical axioms alone.

In the second case, a (logical) theorem has no premises : it needs no non-logical axioms.

Due to the soundness of the calculus, every (logical) theorem is valid (every theorem of propositional calculus is a tautology).

---

We say that a formula $\varphi$ is a logical consequence of a set $\Gamma$ of premises, in symbols:

$\Gamma \vDash \varphi$

if and only if

there is no model $\mathcal {M}$ in which all members of $\Gamma$ are true and $\varphi$ is false.

Due to (strong) soundness of first-order logic, every theorem (in the above sense) of first-order arithmetic is a logical consequence of (first-order) Peano axioms.