In logic, especially mathematical logic, an axiomatic system, sometimes called a "Hilbertstyle" deductive system, is a type of system of formal deduction developed by Gottlob Frege,^{[1]} Jan Łukasiewicz,^{[2]} Russell and Whitehead,^{[3]} and David Hilbert.^{[3]} These deductive systems are most often studied for firstorder logic, but are of interest for other logics as well.
Most variants of axiomatic systems take a characteristic tack in the way they balance a tradeoff between logical axioms and rules of inference.^{[1]} Axiomatic systems can be characterised by the choice of a large number of schemes of logical axioms and a small set of rules of inference. Systems of natural deduction take the opposite tack, including many deduction rules but very few or no axiom schemata. The most commonly studied axiomatic systems have either just one rule of inference – modus ponens, for propositional logics – or two – with generalisation, to handle predicate logics, as well – and several infinite axiom schemes. Axiomatic systems for alethic modal logics, sometimes called HilbertLewis systems, additionally require the necessitation rule. Some systems use a finite list of concrete formulas as axioms instead of an infinite set of formulas via axiom schemes, in which case the uniform substitution rule is required.
A characteristic feature of the many variants of axiomatic systems is that the context is not changed in any of their rules of inference, while both natural deduction and sequent calculus contain some contextchanging rules. Thus, if one is interested only in the derivability of tautologies, no hypothetical judgments, then one can formalize the axiomatic system in such a way that its rules of inference contain only judgments of a rather simple form. The same cannot be done with the other two deductions systems:^{[citation needed]} as context is changed in some of their rules of inferences, they cannot be formalized so that hypothetical judgments could be avoided – not even if we want to use them just for proving derivability of tautologies.
Propositional logic
In propositional logic, it is possible to perform proofs axiomatically, which means that certain tautologies are taken as selfevident and various others are deduced from them using modus ponens as an inference rule, and a rule of substitution. Alternatively, one uses axiom schemas instead of axioms, and no rule of substitution is used.
Frege's Begriffsschrift
Although axiomatic proof has been used since the famous Ancient Greek textbook, Euclid's Elements of Geometry, in propositional logic it dates back to Gottlob Frege's 1879 Begriffsschrift.^{[4]}^{[5]} Frege's system used only implication and negation as connectives,^{[6]} and it had six axioms,^{[5]} which were these ones:^{[7]}^{[8]}
 Proposition 1:
 Proposition 2:
 Proposition 8:
 Proposition 28:
 Proposition 31:
 Proposition 41:
These were used by Frege together with modus ponens and a rule of substitution (which was used but never precisely stated) to yield a complete and consistent axiomatization of classical truthfunctional propositional logic.^{[7]}
Łukasiewicz's P_{2}
Jan Łukasiewicz showed that, in Frege's system, "the third axiom is superfluous since it can be derived from the preceding two axioms, and that the last three axioms can be replaced by the single sentence ".^{[8]} Which, taken out of Łukasiewicz's Polish notation into modern notation, means . Hence, Łukasiewicz is credited^{[5]} with this system of three axioms:
Just like Frege's system, this system uses a substitution rule and uses modus ponens as an inference rule.^{[5]} The exact same system was given (with an explicit substitution rule) by Alonzo Church,^{[9]} who referred to it as the system P_{2,}^{[9]}^{[2]} and helped popularize it.^{[2]}
Schematic form of P_{2}
One may avoid using the rule of substitution by giving the axioms in schematic form, using them to generate an infinite set of axioms. Hence, using Greek letters to represent schemata (metalogical variables that may stand for any wellformed formulas), the axioms are given as:^{[4]}^{[2]}
The schematic version of P_{2} is attributed to John von Neumann,^{[5]} and is used in the Metamath "set.mm" formal proof database.^{[2]} It has also been attributed to Hilbert,^{[10]} and named in this context.^{[10]}
Proof example in P_{2}
As an example, a proof of in P_{2} is given below. First, the axioms are given names:
 (A1)
 (A2)
 (A3)
And the proof is as follows:
 (instance of (A1))
 (instance of (A2))
 (from (1) and (2) by modus ponens)
 (instance of (A1))
 (from (4) and (3) by modus ponens)
Consistency and completeness of P_{2}
The crucial properties of this set of rules are that they are sound and complete. Informally this means that the rules are correct and that no other rules are required. These claims can be made more formal as follows. The proofs for the soundness and completeness of the propositional logic are not themselves proofs in propositional logic; these are theorems in ZFC used as a metatheory to prove properties of propositional logic.
We define a truth assignment as a function that maps propositional variables to true or false. Informally such a truth assignment can be understood as the description of a possible state of affairs (or possible world) where certain statements are true and others are not. The semantics of formulas can then be formalized by defining for which "state of affairs" they are considered to be true, which is what is done by the following definition.
We define when such a truth assignment A satisfies a certain wellformed formula with the following rules:
 A satisfies the propositional variable P if and only if A(P) = true
 A satisfies ¬φ if and only if A does not satisfy φ
 A satisfies (φ ∧ ψ) if and only if A satisfies both φ and ψ
 A satisfies (φ ∨ ψ) if and only if A satisfies at least one of either φ or ψ
 A satisfies (φ → ψ) if and only if it is not the case that A satisfies φ but not ψ
 A satisfies (φ ↔ ψ) if and only if A satisfies both φ and ψ or satisfies neither one of them
With this definition we can now formalize what it means for a formula φ to be implied by a certain set S of formulas. Informally this is true if in all worlds that are possible given the set of formulas S the formula φ also holds. This leads to the following formal definition: We say that a set S of wellformed formulas semantically entails (or implies) a certain wellformed formula φ if all truth assignments that satisfy all the formulas in S also satisfy φ.
Finally we define syntactical entailment such that φ is syntactically entailed by S if and only if we can derive it with the inference rules that were presented above in a finite number of steps. This allows us to formulate exactly what it means for the set of inference rules to be sound and complete:
Soundness: If the set of wellformed formulas S syntactically entails the wellformed formula φ then S semantically entails φ.
Completeness: If the set of wellformed formulas S semantically entails the wellformed formula φ then S syntactically entails φ.
For the above set of rules this is indeed the case.
Sketch of a soundness proof
(For most logical systems, this is the comparatively "simple" direction of proof)
Notational conventions: Let G be a variable ranging over sets of sentences. Let A, B and C range over sentences. For "G syntactically entails A" we write "G proves A". For "G semantically entails A" we write "G implies A".
We want to show: (A)(G) (if G proves A, then G implies A).
We note that "G proves A" has an inductive definition, and that gives us the immediate resources for demonstrating claims of the form "If G proves A, then ...". So our proof proceeds by induction.
 Basis. Show: If A is a member of G, then G implies A.
 Basis. Show: If A is an axiom, then G implies A.
 Inductive step (induction on n, the length of the proof):
 Assume for arbitrary G and A that if G proves A in n or fewer steps, then G implies A.
 For each possible application of a rule of inference at step n + 1, leading to a new theorem B, show that G implies B.
Notice that Basis Step II can be omitted for natural deduction systems because they have no axioms. When used, Step II involves showing that each of the axioms is a (semantic) logical truth.
The Basis steps demonstrate that the simplest provable sentences from G are also implied by G, for any G. (The proof is simple, since the semantic fact that a set implies any of its members, is also trivial.) The Inductive step will systematically cover all the further sentences that might be provable—by considering each case where we might reach a logical conclusion using an inference rule—and shows that if a new sentence is provable, it is also logically implied. (For example, we might have a rule telling us that from "A" we can derive "A or B". In III.a We assume that if A is provable it is implied. We also know that if A is provable then "A or B" is provable. We have to show that then "A or B" too is implied. We do so by appeal to the semantic definition and the assumption we just made. A is provable from G, we assume. So it is also implied by G. So any semantic valuation making all of G true makes A true. But any valuation making A true makes "A or B" true, by the defined semantics for "or". So any valuation which makes all of G true makes "A or B" true. So "A or B" is implied.) Generally, the Inductive step will consist of a lengthy but simple casebycase analysis of all the rules of inference, showing that each "preserves" semantic implication.
By the definition of provability, there are no sentences provable other than by being a member of G, an axiom, or following by a rule; so if all of those are semantically implied, the deduction calculus is sound.
Sketch of completeness proof
(This is usually the much harder direction of proof.)
We adopt the same notational conventions as above.
We want to show: If G implies A, then G proves A. We proceed by contraposition: We show instead that if G does not prove A then G does not imply A. If we show that there is a model where A does not hold despite G being true, then obviously G does not imply A. The idea is to build such a model out of our very assumption that G does not prove A.
 G does not prove A. (Assumption)
 If G does not prove A, then we can construct an (infinite) maximal set, G^{∗}, which is a superset of G and which also does not prove A.
 Place an ordering (with order type ω) on all the sentences in the language (e.g., shortest first, and equally long ones in extended alphabetical ordering), and number them (E_{1}, E_{2}, ...)
 Define a series G_{n} of sets (G_{0}, G_{1}, ...) inductively:
 If proves A, then
 If does not prove A, then
 Define G^{∗} as the union of all the G_{n}. (That is, G^{∗} is the set of all the sentences that are in any G_{n}.)
 It can be easily shown that
 G^{∗} contains (is a superset of) G (by (b.i));
 G^{∗} does not prove A (because the proof would contain only finitely many sentences and when the last of them is introduced in some G_{n}, that G_{n} would prove A contrary to the definition of G_{n}); and
 G^{∗} is a maximal set with respect to A: If any more sentences whatever were added to G^{∗}, it would prove A. (Because if it were possible to add any more sentences, they should have been added when they were encountered during the construction of the G_{n}, again by definition)
 If G^{∗} is a maximal set with respect to A, then it is truthlike. This means that it contains C if and only if it does not contain ¬C; If it contains C and contains "If C then B" then it also contains B; and so forth. In order to show this, one has to show the axiomatic system is strong enough for the following:
 For any formulas C and D, if it proves both C and ¬C, then it proves D. From this it follows, that a maximal set with respect to A cannot prove both C and ¬C, as otherwise it would prove A.
 For any formulas C and D, if it proves both C→D and ¬C→D, then it proves D. This is used, together with the deduction theorem, to show that for any formula, either it or its negation is in G^{∗}: Let B be a formula not in G^{∗}; then G^{∗} with the addition of B proves A. Thus from the deduction theorem it follows that G^{∗} proves B→A. But suppose ¬B were also not in G^{∗}, then by the same logic G^{∗} also proves ¬B→A; but then G^{∗} proves A, which we have already shown to be false.
 For any formulas C and D, if it proves C and D, then it proves C→D.
 For any formulas C and D, if it proves C and ¬D, then it proves ¬(C→D).
 For any formulas C and D, if it proves ¬C, then it proves C→D.
 If G^{∗} is truthlike there is a G^{∗}Canonical valuation of the language: one that makes every sentence in G^{∗} true and everything outside G^{∗} false while still obeying the laws of semantic composition in the language. The requirement that it is truthlike is needed to guarantee that the laws of semantic composition in the language will be satisfied by this truth assignment.
 A G^{∗}canonical valuation will make our original set G all true, and make A false.
 If there is a valuation on which G are true and A is false, then G does not (semantically) imply A.
Thus every system that has modus ponens as an inference rule, and proves the following theorems (including substitutions thereof) is complete:
The first five are used for the satisfaction of the five conditions in stage III above, and the last three for proving the deduction theorem.
Example
As an example, it can be shown that as any other tautology, the three axioms of the classical propositional calculus system described earlier can be proven in any system that satisfies the above, namely that has modus ponens as an inference rule, and proves the above eight theorems (including substitutions thereof). Out of the eight theorems, the last two are two of the three axioms; the third axiom, , can be proven as well, as we now show.
For the proof we may use the hypothetical syllogism theorem (in the form relevant for this axiomatic system), since it only relies on the two axioms that are already in the above set of eight theorems. The proof then is as follows:
 (instance of the 7th theorem)
 (instance of the 7th theorem)
 (from (1) and (2) by modus ponens)
 (instance of the hypothetical syllogism theorem)
 (instance of the 5th theorem)
 (from (5) and (4) by modus ponens)
 (instance of the 2nd theorem)
 (instance of the 7th theorem)
 (from (7) and (8) by modus ponens)

 (instance of the 8th theorem)
 (from (9) and (10) by modus ponens)
 (from (3) and (11) by modus ponens)
 (instance of the 8th theorem)
 (from (12) and (13) by modus ponens)
 (from (6) and (14) by modus ponens)
Verifying completeness for the classical propositional calculus system
We now verify that the classical propositional calculus system described earlier can indeed prove the required eight theorems mentioned above. We use several lemmas proven here:
 (DN1)  Double negation (one direction)
 (DN2)  Double negation (another direction)
 (HS1)  one form of Hypothetical syllogism
 (HS2)  another form of Hypothetical syllogism
 (TR1)  Transposition
 (TR2)  another form of transposition.
 (L1)
 (L3)
We also use the method of the hypothetical syllogism metatheorem as a shorthand for several proof steps.
  proof:
 (instance of (A1))
 (instance of (TR1))
 (from (1) and (2) using the hypothetical syllogism metatheorem)
 (instance of (DN1))
 (instance of (HS1))
 (from (4) and (5) using modus ponens)
 (from (3) and (6) using the hypothetical syllogism metatheorem)
  proof:
 (instance of (HS1))
 (instance of (L3))
 (instance of (HS1))
 (from (2) and (3) by modus ponens)
 (from (1) and (4) using the hypothetical syllogism metatheorem)
 (instance of (TR2))
 (instance of (HS2))
 (from (6) and (7) using modus ponens)
 (from (5) and (8) using the hypothetical syllogism metatheorem)
  proof:
 (instance of (A1))
 (instance of (A1))
 (from (1) and (2) using modus ponens)
  proof:
 (instance of (L1))
 (instance of (TR1))
 (from (1) and (2) using the hypothetical syllogism metatheorem)
  proof:
 (instance of (A1))
 (instance of (A3))
 (from (1) and (2) using the hypothetical syllogism metatheorem)
  proof given in the proof example above
  axiom (A1)
  axiom (A2)
Another outline for a completeness proof
If a formula is a tautology, then there is a truth table for it which shows that each valuation yields the value true for the formula. Consider such a valuation. By mathematical induction on the length of the subformulas, show that the truth or falsity of the subformula follows from the truth or falsity (as appropriate for the valuation) of each propositional variable in the subformula. Then combine the lines of the truth table together two at a time by using "(P is true implies S) implies ((P is false implies S) implies S)". Keep repeating this until all dependencies on propositional variables have been eliminated. The result is that we have proved the given tautology. Since every tautology is provable, the logic is complete.
Different axiomatic proof system
It is possible to define another version of propositional calculus, which defines most of the syntax of the logical operators by means of axioms, and which uses only one inference rule.
Axioms
Let φ, χ, and ψ stand for wellformed formulas. (The wellformed formulas themselves would not contain any Greek letters, but only capital Roman letters, connective operators, and parentheses.) Then the axioms are as follows:
Name  Axiom Schema  Description 

THEN1  Add hypothesis χ, implication introduction  
THEN2  Distribute hypothesis over implication  
AND1  Eliminate conjunction  
AND2  
AND3  Introduce conjunction  
OR1  Introduce disjunction  
OR2  
OR3  Eliminate disjunction  
NOT1  Introduce negation  
NOT2  Eliminate negation  
NOT3  Excluded middle, classical logic  
IFF1  Eliminate equivalence  
IFF2  
IFF3  Introduce equivalence 
 Axiom THEN2 may be considered to be a "distributive property of implication with respect to implication."
 Axioms AND1 and AND2 correspond to "conjunction elimination". The relation between AND1 and AND2 reflects the commutativity of the conjunction operator.
 Axiom AND3 corresponds to "conjunction introduction."
 Axioms OR1 and OR2 correspond to "disjunction introduction." The relation between OR1 and OR2 reflects the commutativity of the disjunction operator.
 Axiom NOT1 corresponds to "reductio ad absurdum."
 Axiom NOT2 says that "anything can be deduced from a contradiction."
 Axiom NOT3 is called "tertium non datur" (Latin: "a third is not given") and reflects the semantic valuation of propositional formulas: a formula can have a truthvalue of either true or false. There is no third truthvalue, at least not in classical logic. Intuitionistic logicians do not accept the axiom NOT3.
Inference rule
The inference rule is modus ponens:
 .
Example of a proof in the different axiomatic system
The following is an example of a (syntactical) demonstration, involving only axioms THEN1 and THEN2:
Prove: (Reflexivity of implication).
Proof:

 Axiom THEN2 with

 Axiom THEN1 with

 From (1) and (2) by modus ponens.

 Axiom THEN1 with

 From (3) and (4) by modus ponens.
Metalogic
Let a demonstration be represented by a sequence, with hypotheses to the left of the turnstile and the conclusion to the right of the turnstile. Then the deduction theorem can be stated as follows:
 If the sequence
 has been demonstrated, then it is also possible to demonstrate the sequence
 .
This deduction theorem (DT) is not itself formulated with propositional calculus: it is not a theorem of propositional calculus, but a theorem about propositional calculus. In this sense, it is a metatheorem, comparable to theorems about the soundness or completeness of propositional calculus.
On the other hand, DT is so useful for simplifying the syntactical proof process that it can be considered and used as another inference rule, accompanying modus ponens. In this sense, DT corresponds to the natural conditional proof inference rule which is part of the first version of propositional calculus introduced in this article.
The converse of DT is also valid:
 If the sequence
 has been demonstrated, then it is also possible to demonstrate the sequence
in fact, the validity of the converse of DT is almost trivial compared to that of DT:
 If
 then
 1:
 2:
 and from (1) and (2) can be deduced
 3:
 by means of modus ponens, Q.E.D.
The converse of DT has powerful implications: it can be used to convert an axiom into an inference rule. For example, by axiom AND1 we have,
which can be transformed by means of the converse of the deduction theorem into
which tells us that the inference rule
is admissible. This inference rule is conjunction elimination, one of the inference rules used in natural deduction.
Conservative extensions
It is common to include in an axiomatic system for logic only axioms for implication and negation. Given these axioms, it is possible to form conservative extensions of the deduction theorem that permit the use of additional connectives. These extensions are called conservative because if a formula φ involving new connectives is rewritten as a logically equivalent formula θ involving only negation, implication, and universal quantification, then φ is derivable in the extended system if and only if θ is derivable in the original system. When fully extended, an axiomatic system will resemble more closely a system of natural deduction.
Existential quantification
 Introduction
 Elimination
 where is not a free variable of .
Conjunction and disjunction
 Conjunction introduction and elimination
 introduction:
 elimination left:
 elimination right:
 Disjunction introduction and elimination
 introduction left:
 introduction right:
 elimination:
Metatheorems
Because axiomatic logical systems have very few deduction rules, it is common to prove metatheorems that show that additional deduction rules add no deductive power, in the sense that a deduction using the new deduction rules can be converted into a deduction using only the original deduction rules.
Some common metatheorems of this form are:
 The deduction theorem: if and only if .
 if and only if and .
 Contraposition: If then .
 Generalization: If and x does not occur free in any formula of then .
Some useful theorems and their proofs
Following are several theorems in propositional logic, along with their proofs (or links to these proofs in other articles). Note that since (P1) itself can be proved using the other axioms, in fact (P2), (P3) and (P4) suffice for proving all these theorems.
 (HS1)  Hypothetical syllogism, see proof.
 (L1)  proof:
 (1) (instance of (P3))
 (2) (instance of (P1))
 (3) (from (2) and (1) by modus ponens)
 (4) (instance of (HS1))
 (5) (from (3) and (4) by modus ponens)
 (6) (instance of (P2))
 (7) (from (6) and (5) by modus ponens)
The following two theorems are known together as Double negation:
 (DN1)
 (DN2)
 See proofs.
 (L2)  for this proof we use the method of the hypothetical syllogism metatheorem as a shorthand for several proof steps:
 (1) (instance of (P3))
 (2) (instance of (HS1))
 (3) (from (1) and (2) using the hypothetical syllogism metatheorem)
 (4) (instance of (P3))
 (5) (from (3) and (4) using modus ponens)
 (6) (instance of (P2))
 (7) (instance of (P2))
 (8) (from (6) and (7) using modus ponens)
 (9) (from (8) and (5) using modus ponens)
 (HS2)  an alternative form of the hypothetical syllogism. proof:
 (1) (instance of (HS1))
 (2) (instance of (L2))
 (3) (from (1) and (2) by modus ponens)
 (TR1)  Transposition, see proof (the other direction of transposition is (P4)).
 (TR2)  another form of transposition; proof:
 (1) (instance of (TR1))
 (2) (instance of (DN1))
 (3) (instance of (HS1))
 (4) (from (2) and (3) by modus ponens)
 (5) (from (1) and (4) using the hypothetical syllogism metatheorem)
 (L3)  proof:
 (1) (instance of (P2))
 (2) (instance of (P4))
 (3) (from (1) and (2) using the hypothetical syllogism metatheorem)
 (4) (instance of (P3))
 (5) (from (3) and (4) using modes ponens)
 (6) (instance of (P4))
 (7) (from (5) and (6) using the hypothetical syllogism metatheorem)
 (8) (instance of (P1))
 (9) (instance of (L1))
 (10) (from (8) and (9) using modes ponens)
 (11) (from (7) and (10) using the hypothetical syllogism metatheorem)
See also
Notes
 ^ ^{a} ^{b} Máté & Ruzsa 1997:129
 ^ ^{a} ^{b} ^{c} ^{d} ^{e} "Proof Explorer  Home Page  Metamath". us.metamath.org. Retrieved 20240702.
 ^ ^{a} ^{b} Craig, Edward (1998). Routledge Encyclopedia of Philosophy. Taylor & Francis. p. 733. ISBN 9780415187107.
 ^ ^{a} ^{b} Bostock, David (1997). Intermediate logic. Oxford : New York: Clarendon Press ; Oxford University Press. pp. 4–5, 8–13, 18–19, 22, 27, 29, 191, 194. ISBN 9780198751410.
 ^ ^{a} ^{b} ^{c} ^{d} ^{e} Smullyan, Raymond M. (20140723). A Beginner's Guide to Mathematical Logic. Courier Corporation. pp. 102–103. ISBN 9780486492377.
 ^ Franks, Curtis (2023), "Propositional Logic", in Zalta, Edward N.; Nodelman, Uri (eds.), The Stanford Encyclopedia of Philosophy (Fall 2023 ed.), Metaphysics Research Lab, Stanford University, retrieved 20240322
 ^ ^{a} ^{b} Mendelsohn, Richard L. (20050110). The Philosophy of Gottlob Frege. Cambridge University Press. p. 185. ISBN 9781139444033.
 ^ ^{a} ^{b} Łukasiewicz, Jan (1970). Jan Lukasiewicz: Selected Works. NorthHolland. p. 136.
 ^ ^{a} ^{b} Church, Alonzo (1996). Introduction to Mathematical Logic. Princeton University Press. p. 119. ISBN 9780691029061.
 ^ ^{a} ^{b} Walicki, Michał (2017). Introduction to mathematical logic (Extended ed.). New Jersey: World Scientific. p. 126. ISBN 9789814719957.
References
 Curry, Haskell B.; Robert Feys (1958). Combinatory Logic Vol. I. Vol. 1. Amsterdam: North Holland.
 Monk, J. Donald (1976). Mathematical Logic. Graduate Texts in Mathematics. Berlin, New York: SpringerVerlag. ISBN 9780387901701.
 Ruzsa, Imre; Máté, András (1997). Bevezetés a modern logikába (in Hungarian). Budapest: Osiris Kiadó.
 Tarski, Alfred (1990). Bizonyítás és igazság (in Hungarian). Budapest: Gondolat. It is a Hungarian translation of Alfred Tarski's selected papers on semantic theory of truth.
 David Hilbert (1927) "The foundations of mathematics", translated by Stephan BauerMenglerberg and Dagfinn Føllesdal (pp. 464–479). in:
 van Heijenoort, Jean (1967). From Frege to Gödel: A Source Book in Mathematical Logic, 1879–1931 (3rd printing 1976 ed.). Cambridge MA: Harvard University Press. ISBN 0674324498.
 Hilbert's 1927, Based on an earlier 1925 "foundations" lecture (pp. 367–392), presents his 17 axioms  axioms of implication #14, axioms about & and V #510, axioms of negation #1112, his logical εaxiom #13, axioms of equality #1415, and axioms of number #1617  along with the other necessary elements of his Formalist "proof theory"  e.g. induction axioms, recursion axioms, etc; he also offers up a spirited defense against L.E.J. Brouwer's Intuitionism. Also see Hermann Weyl's (1927) comments and rebuttal (pp. 480–484), Paul Bernay's (1927) appendix to Hilbert's lecture (pp. 485–489) and Luitzen Egbertus Jan Brouwer's (1927) response (pp. 490–495)
 Kleene, Stephen Cole (1952). Introduction to Metamathematics (10th impression with 1971 corrections ed.). Amsterdam NY: North Holland Publishing Company. ISBN 0720421039.
 See in particular Chapter IV Formal System (pp. 69–85) wherein Kleene presents subchapters §16 Formal symbols, §17 Formation rules, §18 Free and bound variables (including substitution), §19 Transformation rules (e.g. modus ponens)  and from these he presents 21 "postulates"  18 axioms and 3 "immediateconsequence" relations divided as follows: Postulates for the propostional calculus #18, Additional postulates for the predicate calculus #912, and Additional postulates for number theory #1321.
External links
 Gaifman, Haim. "A Hilbert Type Deductive System for Sentential Logic, Completeness and Compactness" (PDF).
 Farmer, W. M. "Propositional logic" (PDF). It describes (among others) a part of the Hilbertstyle deduction system (restricted to propositional calculus).