Relationship between logical axioms and tautologies?

Question

I was reading the mathematical logic paragraph of wikipedia page on Axioms. After dividing the "types" of axioms between logical and non-logical, the article goes on like that referring to propositional logic:

"Logical axioms are formulas that are satisfied by every assignment of values. Usually one takes as logical axioms at least some minimal set of tautologies that is sufficient for proving all tautologies in the language; in the case of predicate logic more logical axioms than that are required, in order to prove logical truths that are not tautologies in the strict sense."

This seems to imply that when you construct a deductive system you choose a "minimal set" of tautologies form the synctax of your formal language and you use them as axioms for your formal system.
These tautologies will be needed to help you proving all the other tautolgies.
What about all the sentences that aren't tautologies? Can you deduce them?
When it says that you can prove all other tautologies, does it mean that you need a rule of inference for that or are these trivially implied by the axioms?
What about theorems, do they follow from tautologies and sme rule of inference?
I feel like I'missing something, or It's not very clear what the article is saying.

Answer 1

Definitions and basic properties

In classical propositional calculus

"tautologies [deleted : Logical axioms] are formulas that are satisfied by every assignment of truth values".

"Usually one takes as logical axioms [deleted : at least some minimal] a suitable set of tautologies that is sufficient for proving all tautologies in the language".

See List of Hilbert systems for a collection of axioms systems for propositional calculus.

As you can see, there are many : classical, intuitionistic, with few basic connectives (one or two : the other defined from the basic ones) or with many.

"Suitable" means : enough to prove the Completeness Theorem, i.e. to prove that all formulas of the calculus with the "designated" property according to the relavant semantics [i.e. all tautologies, in the case of classical propositional calculsu] are derivable from the axioms with the rules of inference.

We write $\vDash \mathcal A$ to denotes the fact that formula $\mathcal A$ is a tautology.

"does it mean that you need a rule of inference for that or are these trivially implied by the axioms?"

"What about theorems, do they follow from tautologies and some rule of inference?"

As said, we can have many different versions of the calculus, vith different sets of axioms+rules.

With axioms, we need at least one rule : usually Modus Ponens.

But we may have calculus without axioms and rules only; see Natural Deduction.

The basic concept of the calculus is that of (formal) derivation :

a finite sequence of formulas where each formula is an axioms or derived from previous formulas in the sequence by way of the inference rule(s).

We write $\vdash \mathcal A$ to denotes the fact that formula $\mathcal A$ is derivable.

"These tautologies [the axioms] will be needed to prove [i.e. to derive] all other tautolgies."

This is sometimes called semantical completeness : if $\vDash \mathcal A$, then $\vdash \mathcal A$.

In addition, we can define the relation of derivability from assumption : $\Gamma \vdash \mathcal A$, where $\Gamma$ is a set of formulas, called assumptions.

In this case, the concept of derivation must be modified accordingly :

a derivation from assumptions is a finite sequence of formulas where each formula is either an axioms or a formula in the set of assumptions, or it is derived from previous formulas in the sequence by way of the inference rule(s).

In this case, we speak of strong completeness of the calculus : if $\Gamma \vDash \mathcal A$, then $\Gamma \vdash \mathcal A$.

"What about all the sentences that aren't tautologies? Can you deduce them?"

No; it is a basic result of propositional calculus that it is sound : it proves only tautologies, i.e. if $\vdash \mathcal A$, then $\vDash \mathcal A$.

But propositional calculus is not syntactically complete in the sense that it is not true that, for every formula $\varphi$ of the language, either $\varphi$ or $¬ \varphi$ is a theorem of the calculus.

Consider the simple formula consisting of a single propositional variable $P$; neither it nor its negation are derivable (they are not tautologies, and the calculus is sound, i.e. it proves only tautologies).

The same for first order predicate calculus.

But, and this is not the case for predicate calculus, propositional logic has the additional property that it is enough to add to the axioms a formula $\mathcal B$ that is not a tautology and the resulting system will be inconsistent.

"in the case of predicate logic more logical axioms than that are required, in order to prove logical truths that are not tautologies in the strict sense."

Yes; for first order predicate calculus we have to add suitable axioms and rules in order to manage quantifiers.

The basic properties required for first-order predicate calculus are the same listed above.

But we have to replace the semantical concept of tautology with that of valid formula :

a formula that is true under every possible interpretation of the language.

First-order instances of propositional tautologies, like e.g. $(x=c) \to (x=c)$, are valid.

But, in addition, there are valid first-order formulas that are not instances of propositional tautologies, like e.g. $\forall x (x=x)$.