Hilbert system explained

In logic, especially mathematical logic, an axiomatic system is a type of system of formal deduction developed by Gottlob Frege,^[1] Jan Łukasiewicz,^[2] Russell and Whitehead,^[3] and David Hilbert. Axiomatic deductive systems are most often studied for first-order logic, but are of interest for other logics as well.

The term "Hilbert system", or "Hilbert-style" deductive system, is sometimes used to describe a deductive system that generates theorems from axioms and inference rules,^{[4] [5] [6]} especially if the only inference rule is modus ponens^{[7] [8]} —which is identical to how other authors define what they call simply an "axiomatic system of logic",^{[9] [10] [11]} with no adjective connecting it to Hilbert. In this context, "Hilbert systems" are contrasted with natural deduction systems, in which no axioms are used, only inference rules. Alternatively, Troelstra defines a "Hilbert system" as a system with axioms and with

{ → }E and {\forall}I as the only inference rules.^[12] A specific set of axioms is also sometimes called "the Hilbert system",^[13] or "the Hilbert-style calculus".^[14] Sometimes, "Hilbert-style" is used to convey the type of axiomatic system that has its axioms given in schematic form,^[15] as in the below—but other sources use the term "Hilbert-style" as encompassing both systems with schematic axioms and systems with a rule of substitution.^[16] One notable source^[17] claims that in "Hilbert-style" systems—as contrasted, again, with natural deduction systems—the inference rules are all categorical rather than conditional. The use of "Hilbert-style" and similar terms to describe axiom systems in logic is due to the influence of Hilbert and Ackermann's Principles of Mathematical Logic (1928).

Most variants of axiomatic systems take a characteristic tack in the way they balance a trade-off 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 Hilbert-Lewis 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 context-changing 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: 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 self-evident 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.^[18] Frege's system used only implication and negation as connectives, and it had six axioms, which were these ones:^{[19] [20]}

• Proposition 1:

a \supset (b \supset a)

• Proposition 2:

(c \supset (b \supset a)) \supset ((c \supset b) \supset (c \supset a))

• Proposition 8:

(d \supset (b \supset a)) \supset (b \supset (d \supset a))

• Proposition 28:

(b \supset a) \supset (\neg a \supset \neg b)

• Proposition 31:

\neg \neg a \supset a

• Proposition 41:

a \supset \neg \neg a

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 truth-functional propositional logic.

Łukasiewicz's P₂

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

CCNpNqCpq ". Which, taken out of Łukasiewicz's Polish notation into modern notation, means (\neg p → \neg q) → (p → q) . Hence, Łukasiewicz is credited with this system of three axioms:p \to (q \to p) (p \to (q \to r)) \to ((p \to q) \to (p \to r)) (\neg p \to \neg q) \to (q \to p)

Just like Frege's system, this system uses a substitution rule and uses modus ponens as an inference rule. The exact same system was given (with an explicit substitution rule) by Alonzo Church,^[21] who referred to it as the system P_2,^[22] and helped popularize it.

Schematic form of P₂

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 well-formed formulas), the axioms are given as:^[23]

\varphi \to (\psi \to \varphi) (\varphi \to (\psi \to \chi)) \to ((\varphi \to \psi) \to (\varphi \to \chi)) (\neg \varphi \to \neg \psi) \to (\psi \to \varphi)

The schematic version of P₂ is attributed to John von Neumann, and is used in the Metamath "set.mm" formal proof database. It has also been attributed to Hilbert,^[24] and named

l{H} in this context.

Proof example in P₂

As an example, a proof of

A \to A in P₂ is given below. First, the axioms are given names:

(A1)

(p \to (q \to p))

(A2)

((p \to (q \to r)) \to ((p \to q) \to (p \to r)))

(A3)

((\neg p \to \neg q) \to (q \to p))

And the proof is as follows:

A \to ((B \to A) \to A)       (instance of (A1))(A \to ((B \to A) \to A)) \to ((A \to (B \to A)) \to (A \to A))       (instance of (A2))(A \to (B \to A)) \to (A \to A)       (from (1) and (2) by modus ponens)A \to (B \to A)       (instance of (A1))A \to A       (from (4) and (3) by modus ponens)

Consistency and completeness of P₂

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 satisfies a certain well-formed formula with the following rules:

• • satisfies the propositional variable if and only if satisfies if and only if does not satisfy
• satisfies if and only if satisfies both and
• satisfies if and only if satisfies at least one of either or
• satisfies if and only if it is not the case that satisfies but not
• satisfies if and only if 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 of formulas. Informally this is true if in all worlds that are possible given the set of formulas the formula also holds. This leads to the following formal definition: We say that a set of well-formed formulas semantically entails (or implies) a certain well-formed formula if all truth assignments that satisfy all the formulas in also satisfy .

Finally we define syntactical entailment such that is syntactically entailed by 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 well-formed formulas syntactically entails the well-formed formula then semantically entails .

Completeness: If the set of well-formed formulas semantically entails the well-formed formula then 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 be a variable ranging over sets of sentences. Let and range over sentences. For " syntactically entails " we write " proves ". For " semantically entails " we write " implies ".

We want to show: (if proves, then implies).

We note that " proves " has an inductive definition, and that gives us the immediate resources for demonstrating claims of the form "If proves, then ...". So our proof proceeds by induction.

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 are also implied by, for any . (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 "" we can derive " or ". In III.a We assume that if is provable it is implied. We also know that if is provable then " or " is provable. We have to show that then " or " too is implied. We do so by appeal to the semantic definition and the assumption we just made. is provable from, we assume. So it is also implied by . So any semantic valuation making all of true makes true. But any valuation making true makes " or " true, by the defined semantics for "or". So any valuation which makes all of true makes " or " true. So " or " is implied.) Generally, the Inductive step will consist of a lengthy but simple case-by-case 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, 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 implies, then proves . We proceed by contraposition: We show instead that if does not prove then does not imply . If we show that there is a model where does not hold despite being true, then obviously does not imply . The idea is to build such a model out of our very assumption that does not prove .

Thus every system that has modus ponens as an inference rule, and proves the following theorems (including substitutions thereof) is complete:

p \to (\neg p \to q) (p \to q) \to ((\neg p \to q) \to q) p \to (q \to (p \to q)) p \to (\neg q \to \neg (p \to q)) \neg p \to (p \to q) p \to p p \to (q \to p) (p \to (q \to r)) \to ((p \to q) \to (p \to r))

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,

(\neg q \to \neg p) \to (p \to q) , 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:

q \to (p \to q)       (instance of the 7th theorem)(q \to (p \to q)) \to ((\neg q \to \neg p) \to (q \to (p \to q)))       (instance of the 7th theorem)(\neg q \to \neg p) \to (q \to (p \to q))       (from (1) and (2) by modus ponens)(\neg p \to (p \to q)) \to ((\neg q \to \neg p) \to (\neg q\to (p\to q)))       (instance of the hypothetical syllogism theorem)(\neg p \to (p \to q))       (instance of the 5th theorem)(\neg q \to \neg p) \to (\neg q\to (p\to q))       (from (5) and (4) by modus ponens)(q \to (p \to q)) \to ((\neg q \to (p \to q)) \to (p \to q))       (instance of the 2nd theorem)((q \to (p \to q)) \to ((\neg q \to (p \to q)) \to (p \to q)) ) \to ((\neg q \to \neg p) \to ((q \to (p \to q)) \to ((\neg q \to (p \to q)) \to (p \to q))))       (instance of the 7th theorem)(\neg q \to \neg p) \to ((q \to (p \to q)) \to ((\neg q \to (p \to q)) \to (p \to q)))       (from (7) and (8) by modus ponens)((\neg q \to \neg p) \to ((q \to (p \to q)) \to ((\neg q \to (p \to q)) \to (p \to q)))) \to (((\neg q \to \neg p) \to (q \to (p \to q))) \to ((\neg q \to \neg p) \to ((\neg q \to (p \to q)) \to (p \to q))))       (instance of the 8th theorem)((\neg q \to \neg p) \to (q \to (p \to q))) \to ((\neg q \to \neg p) \to ((\neg q \to (p \to q)) \to (p \to q)))       (from (9) and (10) by modus ponens)(\neg q \to \neg p) \to ((\neg q \to (p \to q)) \to (p \to q))       (from (3) and (11) by modus ponens)((\neg q \to \neg p) \to ((\neg q \to (p \to q)) \to (p \to q))) \to (((\neg q \to \neg p) \to (\neg q \to (p \to q))) \to ((\neg q \to \neg p) \to (p \to q)))       (instance of the 8th theorem)((\neg q \to \neg p) \to (\neg q \to (p \to q))) \to ((\neg q \to \neg p) \to (p \to q))       (from (12) and (13) by modus ponens)(\neg q \to \neg p) \to (p \to q)       (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)

\neg \neg p \to p - Double negation (one direction)

(DN2)

p \to \neg \neg p - Double negation (another direction)

(HS1)

(q \to r) \to ((p \to q) \to (p \to r)) - one form of Hypothetical syllogism

(HS2)

(p \to q) \to ((q \to r) \to (p \to r)) - another form of Hypothetical syllogism

(TR1)

(p \to q) \to (\neg q \to \neg p) - Transposition

(TR2)

(\neg p \to q) \to (\neg q \to p) - another form of transposition.

(L1)

p \to ((p \to q) \to q)

(L3)

(\neg p \to p) \to p We also use the method of the hypothetical syllogism metatheorem as a shorthand for several proof steps.p \to (\neg p \to q) - proof:p \to (\neg q \to p)       (instance of (A1))(\neg q \to p) \to (\neg p \to \neg\neg q)       (instance of (TR1))p \to (\neg p \to \neg\neg q)       (from (1) and (2) using the hypothetical syllogism metatheorem)\neg\neg q \to q       (instance of (DN1))(\neg\neg q \to q) \to ((\neg p \to \neg\neg q) \to (\neg p \to q))       (instance of (HS1))(\neg p \to \neg\neg q) \to (\neg p \to q)       (from (4) and (5) using modus ponens)p \to (\neg p \to q)       (from (3) and (6) using the hypothetical syllogism metatheorem)(p \to q) \to ((\neg p \to q) \to q) - proof:(p \to q) \to ((\neg q \to p) \to (\neg q \to q))       (instance of (HS1))(\neg q \to q) \to q       (instance of (L3))((\neg q \to q) \to q) \to (((\neg q \to p) \to (\neg q \to q)) \to ((\neg q \to p) \to q))       (instance of (HS1))((\neg q \to p) \to (\neg q \to q)) \to ((\neg q \to p) \to q)       (from (2) and (3) by modus ponens)(p \to q) \to ((\neg q \to p) \to q)       (from (1) and (4) using the hypothetical syllogism metatheorem)(\neg p \to q) \to (\neg q \to p)       (instance of (TR2))((\neg p \to q) \to (\neg q \to p)) \to (((\neg q \to p) \to q) \to ((\neg p \to q) \to q))       (instance of (HS2))((\neg q \to p) \to q) \to ((\neg p \to q) \to q)       (from (6) and (7) using modus ponens)(p \to q) \to ((\neg p \to q) \to q)       (from (5) and (8) using the hypothetical syllogism metatheorem)p \to (q \to (p \to q)) - proof:q \to (p \to q)       (instance of (A1))(q \to (p \to q)) \to (p \to (q \to (p \to q)))       (instance of (A1))p \to (q \to (p \to q))       (from (1) and (2) using modus ponens)p \to (\neg q \to \neg (p \to q)) - proof:p \to ((p \to q) \to q)       (instance of (L1))((p \to q) \to q) \to (\neg q \to \neg (p \to q))       (instance of (TR1))p \to (\neg q \to \neg (p \to q))       (from (1) and (2) using the hypothetical syllogism metatheorem)\neg p \to (p \to q) - proof:\neg p \to (\neg q \to \neg p)       (instance of (A1))(\neg q \to \neg p) \to (p \to q)       (instance of (A3))\neg p \to (p \to q)       (from (1) and (2) using the hypothetical syllogism metatheorem)p \to p - proof given in the proof example abovep \to (q \to p) - axiom (A1)(p \to (q \to r)) \to ((p \to q) \to (p \to r)) - 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 "(is true implies) implies ((is false implies) implies)". 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 well-formed formulas. (The well-formed formulas themselves would not contain any Greek letters, but only capital Roman letters, connective operators, and parentheses.) Then the axioms are as follows:

+ Axioms
Name	Axiom Schema	Description
	\phi \to (\chi \to \phi)	Add hypothesis, implication introduction
	(\phi \to (\chi \to \psi)) \to ((\phi \to \chi) \to (\phi \to \psi))	Distribute hypothesis \phi over implication
	\phi \land \chi \to \phi	Eliminate conjunction
	\phi \land \chi \to \chi
	\phi \to (\chi \to (\phi \land \chi))	Introduce conjunction
	\phi \to \phi \lor \chi	Introduce disjunction
	\chi \to \phi \lor \chi
	(\phi \to \psi) \to ((\chi \to \psi) \to (\phi \lor \chi \to \psi))	Eliminate disjunction
	(\phi \to \chi) \to ((\phi \to \neg \chi) \to \neg \phi)	Introduce negation
	\phi \to (\neg \phi \to \chi)	Eliminate negation
	\phi \lor \neg \phi	Excluded middle, classical logic
	(\phi \leftrightarrow \chi) \to (\phi \to \chi)	Eliminate equivalence
	(\phi \leftrightarrow \chi) \to (\chi \to \phi)
	(\phi \to \chi) \to ((\chi \to \phi) \to (\phi \leftrightarrow \chi))	Introduce equivalence

• Axiom may be considered to be a "distributive property of implication with respect to implication."
• Axioms and correspond to "conjunction elimination". The relation between and reflects the commutativity of the conjunction operator.
• Axiom corresponds to "conjunction introduction."
• Axioms and correspond to "disjunction introduction." The relation between and reflects the commutativity of the disjunction operator.
• Axiom corresponds to "reductio ad absurdum."
• Axiom says that "anything can be deduced from a contradiction."
• Axiom is called "tertium non datur" (Latin: "a third is not given") and reflects the semantic valuation of propositional formulas: a formula can have a truth-value of either true or false. There is no third truth-value, at least not in classical logic. Intuitionistic logicians do not accept the axiom .

Inference rule

The inference rule is modus ponens:

(\phi, \phi \to \chi)/(\chi) .

Example of a proof in the different axiomatic system

The following is an example of a (syntactical) demonstration, involving only axioms and :

Prove:

A \to A (Reflexivity of implication).

Proof:

(A \to ((B \to A) \to A)) \to ((A \to (B \to A)) \to (A \to A))

Axiom with

\phi = A, \chi = B \to A, \psi = A A \to ((B \to A) \to A)

Axiom with

\phi = A, \chi = B \to A (A \to (B \to A)) \to (A \to A)

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

A \to (B \to A)

Axiom with

\phi = A, \chi = B A \to A

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

\phi _{1,} \phi _{2,} ... , \phi _{n,} \chi \vdash \psi

has been demonstrated, then it is also possible to demonstrate the sequence

\phi _{1,} \phi _{2,} ..., \phi _{n} \vdash \chi \to \psi .

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 meta-theorem, 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

\phi _{1,} \phi _{2,} ..., \phi _{n} \vdash \chi \to \psi

has been demonstrated, then it is also possible to demonstrate the sequence

\phi _{1,} \phi _{2,} ... , \phi _{n,} \chi \vdash \psi in fact, the validity of the converse of DT is almost trivial compared to that of DT:

If

\phi _{1,} ... , \phi _{n} \vdash \chi \to \psi

then

1:

\phi _{1,} ... , \phi _{n,} \chi \vdash \chi \to \psi

2:

\phi _{1,} ... , \phi _{n,} \chi \vdash \chi

and from (1) and (2) can be deduced

3:

\phi _{1,} ... , \phi _{n,} \chi \vdash \psi

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 AND-1 we have,

\vdash \phi \wedge \chi \to \phi, which can be transformed by means of the converse of the deduction theorem into\phi \wedge \chi \vdash \phi, which tells us that the inference rule(\phi \wedge \chi)/(\phi) 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

\forall x(\phi \to \exists y(\phi[x: = y]))

• Elimination

\forall x(\phi \to \psi) \to \exists x(\phi) \to \psi where x is not a free variable of \psi .

Conjunction and disjunction

• Conjunction introduction and elimination

introduction:

\alpha\to(\beta\to\alpha\land\beta)

elimination left:

\alpha\wedge\beta\to\alpha

elimination right:

\alpha\wedge\beta\to\beta

• Disjunction introduction and elimination

introduction left:

\alpha\to\alpha\vee\beta

introduction right:

\beta\to\alpha\vee\beta

elimination:

(\alpha\to\gamma)\to ((\beta\to\gamma) \to \alpha\vee\beta \to \gamma)

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:

\Gamma;\phi \vdash \psi if and only if \Gamma \vdash \phi \to \psi .\Gamma \vdash \phi \leftrightarrow \psi if and only if \Gamma \vdash \phi \to \psi and \Gamma \vdash \psi \to \phi .

• Contraposition: If

\Gamma;\phi \vdash \psi then \Gamma; ln ot \psi \vdash ln ot \phi .

• Generalization: If

\Gamma \vdash \phi and x does not occur free in any formula of \Gamma then \Gamma \vdash \forall x \phi .

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)

(q \to r) \to ((p \to q) \to (p \to r)) - Hypothetical syllogism, see proof.

(L1)

p \to ((p \to q) \to q) - proof:

(1)

((p \to q) \to (p \to q)) \to (((p \to q) \to p) \to ((p \to q) \to q))       (instance of (P3))

(2)

(p \to q) \to (p \to q)       (instance of (P1))

(3)

((p \to q) \to p) \to ((p \to q) \to q)       (from (2) and (1) by modus ponens)

(4)

(((p \to q) \to p) \to ((p \to q) \to q)) \to ((p \to ((p \to q) \to p)) \to (p \to ((p \to q) \to q)))       (instance of (HS1))

(5)

(p \to ((p \to q) \to p)) \to (p \to ((p \to q) \to q))       (from (3) and (4) by modus ponens)

(6)

p \to ((p \to q) \to p)       (instance of (P2))

(7)

p \to ((p \to q) \to q)       (from (6) and (5) by modus ponens)The following two theorems are known together as Double negation:

(DN1)

\neg \neg p \to p

(DN2)

p \to \neg \neg p

See proofs.

(L2)

(p \to (q \to r)) \to (q \to (p \to r)) - for this proof we use the method of the hypothetical syllogism metatheorem as a shorthand for several proof steps:

(1)

(p \to (q \to r)) \to ((p \to q) \to (p \to r))       (instance of (P3))

(2)

((p \to q) \to (p \to r)) \to ((q \to (p \to q)) \to (q \to (p \to r)))       (instance of (HS1))

(3)

(p \to (q \to r)) \to ((q \to (p \to q)) \to (q \to (p \to r)))       (from (1) and (2) using the hypothetical syllogism metatheorem)

(4)

((p \to (q \to r)) \to ((q \to (p \to q)) \to (q \to (p \to r)))) \to (((p \to (q \to r)) \to (q \to (p \to q))) \to ((p \to (q \to r)) \to (q \to (p \to r))))       (instance of (P3))

(5)

((p \to (q \to r)) \to (q \to (p \to q))) \to ((p \to (q \to r)) \to (q \to (p \to r)))       (from (3) and (4) using modus ponens)

(6)

q \to (p \to q)       (instance of (P2))

(7)

(q \to (p \to q)) \to ((p \to (q \to r)) \to (q \to (p \to q)))       (instance of (P2))

(8)

(p \to (q \to r)) \to (q \to (p \to q))       (from (6) and (7) using modus ponens)

(9)

(p \to (q \to r)) \to (q \to (p \to r))       (from (8) and (5) using modus ponens)

(HS2)

(p \to q) \to ((q \to r) \to (p \to r)) - an alternative form of the hypothetical syllogism. proof:

(1)

(q \to r) \to ((p \to q) \to (p \to r))       (instance of (HS1))

(2)

((q \to r) \to ((p \to q) \to (p \to r))) \to ((p \to q) \to ((q \to r) \to (p \to r)))       (instance of (L2))

(3)

(p \to q) \to ((q \to r) \to (p \to r)) (from (1) and (2) by modus ponens)

(TR1)

(p \to q) \to (\neg q \to \neg p) - Transposition, see proof (the other direction of transposition is (P4)).

(TR2)

(\neg p \to q) \to (\neg q \to p) - another form of transposition; proof:

(1)

(\neg p \to q) \to (\neg q \to \neg \neg p)       (instance of (TR1))

(2)

\neg \neg p \to p       (instance of (DN1))

(3)

(\neg \neg p \to p) \to ((\neg q \to \neg \neg p) \to (\neg q \to p))       (instance of (HS1))

(4)

(\neg q \to \neg \neg p) \to (\neg q \to p)       (from (2) and (3) by modus ponens)

(5)

(\neg p \to q) \to (\neg q \to p)       (from (1) and (4) using the hypothetical syllogism metatheorem)

(L3)

(\neg p \to p) \to p - proof:

(1)

\neg p \to (\neg \neg (q \to q) \to \neg p)       (instance of (P2))

(2)

(\neg \neg (q \to q) \to \neg p) \to (p \to \neg (q \to q))       (instance of (P4))

(3)

\neg p \to (p \to \neg (q \to q))       (from (1) and (2) using the hypothetical syllogism metatheorem)

(4)

(\neg p \to (p \to \neg (q \to q))) \to ((\neg p \to p) \to (\neg p \to \neg (q \to q)))       (instance of (P3))

(5)

(\neg p \to p) \to (\neg p \to \neg (q \to q))       (from (3) and (4) using modes ponens)

(6)

(\neg p \to \neg (q \to q)) \to ((q \to q) \to p)       (instance of (P4))

(7)

(\neg p \to p) \to ((q \to q) \to p)       (from (5) and (6) using the hypothetical syllogism metatheorem)

(8)

q \to q       (instance of (P1))

(9)

(q \to q) \to (((q \to q) \to p) \to p)       (instance of (L1))

(10)

((q \to q) \to p) \to p       (from (8) and (9) using modes ponens)

(11)

(\neg p \to p) \to p       (from (7) and (10) using the hypothetical syllogism metatheorem)

See also

• List of axiomatic systems in logic
• Natural deduction
• Curry–Howard correspondence
• Combinatory logic

Notes

1. Máté & Ruzsa 1997:129
2. Web site: Proof Explorer - Home Page - Metamath . 2024-07-02 . us.metamath.org . EN-US.
3. Book: Craig, Edward . Routledge Encyclopedia of Philosophy . 1998 . Taylor & Francis . 978-0-415-18710-7 . 733 . en.
4. Book: Restall, Greg . An Introduction to Substructural Logics . 2002-09-11 . Routledge . 978-1-135-11131-1 . 73-74 . en.
5. Web site: Gaifman . Haim . 2002 . A Hilbert Type Deductive System for Sentential Logic, Completeness and Compactness . 2024-08-19 . Columbia.
6. Book: Benthem, Johan van . Proof, Computation and Agency: Logic at the Crossroads . Gupta . Amitabha . Parikh . Rohit . 2011-04-02 . Springer Science & Business Media . 978-94-007-0080-2 . 41 . en.
7. Book: Bacon, Andrew . A Philosophical Introduction to Higher-order Logics . 2023-09-29 . Taylor & Francis . 978-1-000-92575-3 . 424 . en.
8. Book: Eijck, Jan van . Logics in AI: European Workshop JELIA '90, Amsterdam, The Netherlands, September 10-14, 1990. Proceedings . 1991-02-26 . Springer Science & Business Media . 978-3-540-53686-4 . 113 . en.
9. Book: Haack, Susan . Philosophy of Logics . 1978-07-27 . Cambridge University Press . 978-0-521-29329-7 . 19 . en.
10. Book: Bostock, David . Intermediate Logic . 1997-08-07 . Clarendon Press . 978-0-19-103722-1 . 192 . en.
11. Book: Lucas, J. R. . A Treatise on Time and Space . 2018-10-10 . Routledge . 978-0-429-68517-0 . 152 . en.
12. Book: Troelstra, A. S. . Basic Proof Theory . Schwichtenberg . H. . 2000 . Cambridge University Press . 978-0-521-77911-1 . 2 . Cambridge Tracts in Theoretical Computer Science . Cambridge . 51 . 10.1017/cbo9781139168717.
13. Web site: Introduction to Logic - Chapter 4 . 2024-08-16 . intrologic.stanford.edu.
14. Book: Buss, S. R. . Handbook of Proof Theory . 1998-07-09 . Elsevier . 978-0-08-053318-6 . 552-553 . en.
15. Book: Smith, Peter . An Introduction to Gödel's Theorems . 2013-02-21 . Cambridge University Press . 978-1-107-02284-3 . 10 . en.
16. Book: Ono, Hiroakira . Proof Theory and Algebra in Logic . 2019-08-02 . Springer . 978-981-13-7997-0 . 5 . en.
17. Book: Gabbay, Dov M. . Handbook of Philosophical Logic . Guenthner . Franz . 2013-03-14 . Springer Science & Business Media . 978-94-017-0458-8 . 201 . en.
18. Book: Smullyan, Raymond M. . A Beginner's Guide to Mathematical Logic . 2014-07-23 . Courier Corporation . 978-0-486-49237-7 . 102–103 . en.
19. Book: Mendelsohn, Richard L. . The Philosophy of Gottlob Frege . 2005-01-10 . Cambridge University Press . 978-1-139-44403-3 . 185 . en.
20. Book: Łukasiewicz, Jan . Jan Lukasiewicz: Selected Works . 1970 . North-Holland . 136 . en.
21. Book: Church, Alonzo . Introduction to Mathematical Logic . 1996 . Princeton University Press . 978-0-691-02906-1 . 119 . en.
22. Web site: Proof Explorer - Home Page - Metamath . 2024-07-02 . us.metamath.org . EN-US.
23. Book: Bostock, David . Intermediate logic . 1997 . Clarendon Press ; Oxford University Press . 978-0-19-875141-0 . Oxford : New York . 4-5, 8-13, 18-19, 22, 27, 29, 191, 194.
24. Book: Walicki, Michał . Introduction to mathematical logic . 2017 . World Scientific . 978-981-4719-95-7 . Extended . New Jersey . 126.

References

• Book: Curry , Haskell B. . Robert Feys. Combinatory Logic Vol. I. 1. 1958. North Holland. Amsterdam.
• Book: Monk . J. Donald . 1976 . Mathematical Logic . . Berlin, New York . Graduate Texts in Mathematics . 978-0-387-90170-1 . registration .
• Book: Ruzsa . Imre . Máté . András . 1997 . Bevezetés a modern logikába . Hungarian . Osiris Kiadó . Budapest.
• Book: Tarski, Alfred . 1990 . Bizonyítás és igazság . Hungarian . Gondolat . Budapest. 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 Bauer-Menglerberg and Dagfinn Føllesdal (pp. 464 - 479). in:
  • Book: van Heijenoort , Jean . 1967. From Frege to Gödel: A Source Book in Mathematical Logic, 1879 - 1931. 3rd printing 1976. Harvard University Press. Cambridge MA. 0-674-32449-8. registration.
  • Hilbert's 1927, Based on an earlier 1925 "foundations" lecture (pp. 367 - 392), presents his 17 axioms -- axioms of implication #1-4, axioms about & and V #5-10, axioms of negation #11-12, his logical ε-axiom #13, axioms of equality #14-15, and axioms of number #16-17 -- 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)
• Book: Kleene , Stephen Cole . 1952. Introduction to Metamathematics. 10th impression with 1971 corrections. North Holland Publishing Company. Amsterdam NY. 0-7204-2103-9.
  • 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 "immediate-consequence" relations divided as follows: Postulates for the propostional calculus #1-8, Additional postulates for the predicate calculus #9-12, and Additional postulates for number theory #13-21.

External links

• Web site: Gaifman . Haim. A Hilbert Type Deductive System for Sentential Logic, Completeness and Compactness..
• Web site: Farmer . W. M . Propositional logic . It describes (among others) a part of the Hilbert-style deduction system (restricted to propositional calculus).