Talk:List of Hilbert systems

Inaccessible

The article is utterly inaccessible for non-experts. Boris Tsirelson (talk) 15:06, 10 September 2010 (UTC)

It's rather inaccessible for experts too, since it uses an unnecessarily obscure prefix notation which has no utility in an age of LaTeX and MathML. -- Radagast3 (talk) 02:37, 11 September 2010 (UTC)

I have to agree that polish notation should be replaced. However I think the content is otherwise a wonderful contribution.Greg Bard (talk) 16:23, 12 September 2010 (UTC)

With the infix notation it will be still inaccessible unless a context will be explained, the meaning of it all, - what is happening, and what for. Boris Tsirelson (talk) 18:39, 12 September 2010 (UTC)

Now it makes sense. Boris Tsirelson (talk) 16:42, 13 September 2010 (UTC)

I'm not an expert, but it seems straight-forward enough, now. 67.198.37.16 (talk) 02:19, 31 August 2016 (UTC)

Modus Ponens

The article says all these logic systems include Modus Ponens, so they don't need to mention. But then under Tarski–Bernays–Wajsberg axiom system, an axiom is included ((A→B)→A)→B). Isn't this a version of Modus Ponens? Just to be clear, modus ponens should be added to all of them except Tarski–Bernays–Wajsberg? Or should be implicitly added to them all, including Tarski–Bernays–Wajsberg? -lethe ^{talk +} 05:28, 4 December 2017 (UTC)

The axiom $((A\to B)\to A)\to A$ is Peirce's law, not modus ponens. Modus ponens is a rule of inference, but not an axiom schema. (Axiom schemas are also rules of inference of an especially simple form.) JRSpriggs (talk) 05:52, 4 December 2017 (UTC)

I was thinking of some kind of currying principle. $(A\wedge B\to C)\leftrightarrow (A\to B\to C).$ So if modus ponens is $A\wedge (A\to B)\to B$, which currying transforms into $A\to (A\to B)\to B.$ I think I had guessed that some argument like this applies to the form of Pierce's law. But now I think Pierce's law is parenthesized wrong for currying to apply, among other discrepancies. -lethe ^{talk +} 16:34, 17 December 2017 (UTC)

How to establish completeness in a two-valued (i.e. classical) logic

To illustrate my point, I will take the Sheffer stroke as an example because it is a connective and system with which I am not used to working, but is also simple in that it has only one connective. First let me make two definitions (abbreviations) to make the formulas more readable and keep them from becoming excessively long:

$(\lnot P):=(P\uparrow P)$

$(P\to Q):=(P\uparrow \lnot Q)$.

We must show that modus ponens is a valid inference in these systems. It is so because ordinary modus ponens translates to

$P,P\uparrow (Q\uparrow Q)\vdash Q$

which is a special case of Nicod's modus ponens

$P,P\uparrow (R\uparrow Q)\vdash Q$.

To show completeness, we need to make sure that the deduction metatheorem holds (it is a feature of classical logic so it would have to hold even if one chooses some other way to get completeness), so we need

1. $P\to (Q\to P)$ and

2. $(P\to (Q\to R))\to ((P\to Q)\to (P\to R))$

to be theorems.

For a valuation v, any formula true in that valuation could be derived by induction on its subformulas P establishing

$v\models P$

for true subformulas and

$v\models \lnot P$

for false subformulas. In our example, subformulas (other than atoms) are formed in only one way, by using the Sheffer stroke. So we need

3. $P\to (Q\to \lnot (P\uparrow Q))$,

4. $\lnot P\to (P\uparrow Q))$, and

5. $\lnot Q\to (P\uparrow Q))$

to be theorems. These theorems encode the four entries in the truth-table for NAND.

If the formula F in question is a tautology, then it is true in any valuation. So any combination of values assigned to its atoms will allow one to derive F. We can then remove the dependency on the specific valuation by backwards induction (see implicational propositional calculus#Completeness for an example). This requires one last theorem:

6. $(P\to Q)\to ((\lnot P\to Q)\to Q)$.

So the problem of establishing that all tautologies are theorems has been reduced to showing that six specific tautologies are theorems. JRSpriggs (talk) 04:13, 30 September 2018 (UTC)

Here is an example of how these six theorems can be used to prove any tautology, that is, show that it is a theorem.

To show: $(A\uparrow (B\uparrow A))\uparrow [(A\uparrow (B\uparrow A))\uparrow ((B\uparrow A)\uparrow [(A\uparrow B)\uparrow (A\uparrow B)])]$. Here I am using the deduction metatheorem so theorems 1 and 2 are being used implicitly throughout.

$A$ hypothesis

$B$ hypothesis

$B\to (A\to \lnot (B\uparrow A))$ theorem 3

$A\to \lnot (B\uparrow A)$ modus ponens

$\lnot (B\uparrow A)$ modus ponens

$\lnot (B\uparrow A)\to (A\uparrow (B\uparrow A))$ theorem 5

$A\uparrow (B\uparrow A)$ modus ponens

$\lnot (B\uparrow A)\to ((B\uparrow A)\uparrow [(A\uparrow B)\uparrow (A\uparrow B)])$ theorem 4

$(B\uparrow A)\uparrow [(A\uparrow B)\uparrow (A\uparrow B)]$ modus ponens

$(A\uparrow (B\uparrow A))\to (((B\uparrow A)\uparrow [(A\uparrow B)\uparrow (A\uparrow B)])\to \lnot [(A\uparrow (B\uparrow A))\uparrow ((B\uparrow A)\uparrow [(A\uparrow B)\uparrow (A\uparrow B)])])$ theorem 3

$((B\uparrow A)\uparrow [(A\uparrow B)\uparrow (A\uparrow B)])\to \lnot [(A\uparrow (B\uparrow A))\uparrow ((B\uparrow A)\uparrow [(A\uparrow B)\uparrow (A\uparrow B)])]$ modus ponens

$\lnot [(A\uparrow (B\uparrow A))\uparrow ((B\uparrow A)\uparrow [(A\uparrow B)\uparrow (A\uparrow B)])]$ modus ponens

$\lnot [(A\uparrow (B\uparrow A))\uparrow ((B\uparrow A)\uparrow [(A\uparrow B)\uparrow (A\uparrow B)])]\to ((A\uparrow (B\uparrow A))\uparrow [(A\uparrow (B\uparrow A))\uparrow ((B\uparrow A)\uparrow [(A\uparrow B)\uparrow (A\uparrow B)])])$ theorem 5

$(A\uparrow (B\uparrow A))\uparrow [(A\uparrow (B\uparrow A))\uparrow ((B\uparrow A)\uparrow [(A\uparrow B)\uparrow (A\uparrow B)])]$ modus ponens

$B\to ((A\uparrow (B\uparrow A))\uparrow [(A\uparrow (B\uparrow A))\uparrow ((B\uparrow A)\uparrow [(A\uparrow B)\uparrow (A\uparrow B)])])$ deduction

$\lnot B$ hypothesis

$\lnot B\to (B\uparrow A)$ theorem 4

$B\uparrow A$ modus ponens

$A\to ((B\uparrow A)\to \lnot (A\uparrow (B\uparrow A)))$ theorem 3

$(B\uparrow A)\to \lnot (A\uparrow (B\uparrow A))$ modus ponens

$\lnot (A\uparrow (B\uparrow A))$ modus ponens

$\lnot (A\uparrow (B\uparrow A))\to ((A\uparrow (B\uparrow A))\uparrow [(A\uparrow (B\uparrow A))\uparrow ((B\uparrow A)\uparrow [(A\uparrow B)\uparrow (A\uparrow B)])])$ theorem 4

$(A\uparrow (B\uparrow A))\uparrow [(A\uparrow (B\uparrow A))\uparrow ((B\uparrow A)\uparrow [(A\uparrow B)\uparrow (A\uparrow B)])]$ modus ponens

$\lnot B\to ((A\uparrow (B\uparrow A))\uparrow [(A\uparrow (B\uparrow A))\uparrow ((B\uparrow A)\uparrow [(A\uparrow B)\uparrow (A\uparrow B)])])$ deduction

$(B\to ((A\uparrow (B\uparrow A))\uparrow [(A\uparrow (B\uparrow A))\uparrow ((B\uparrow A)\uparrow [(A\uparrow B)\uparrow (A\uparrow B)])]))\to ((\lnot B\to ((A\uparrow (B\uparrow A))\uparrow [(A\uparrow (B\uparrow A))\uparrow ((B\uparrow A)\uparrow [(A\uparrow B)\uparrow (A\uparrow B)])]))\to ((A\uparrow (B\uparrow A))\uparrow [(A\uparrow (B\uparrow A))\uparrow ((B\uparrow A)\uparrow [(A\uparrow B)\uparrow (A\uparrow B)])]))$ theorem 6

$(\lnot B\to ((A\uparrow (B\uparrow A))\uparrow [(A\uparrow (B\uparrow A))\uparrow ((B\uparrow A)\uparrow [(A\uparrow B)\uparrow (A\uparrow B)])]))\to ((A\uparrow (B\uparrow A))\uparrow [(A\uparrow (B\uparrow A))\uparrow ((B\uparrow A)\uparrow [(A\uparrow B)\uparrow (A\uparrow B)])])$ modus ponens

$(A\uparrow (B\uparrow A))\uparrow [(A\uparrow (B\uparrow A))\uparrow ((B\uparrow A)\uparrow [(A\uparrow B)\uparrow (A\uparrow B)])]$ modus ponens

$A\to ((A\uparrow (B\uparrow A))\uparrow [(A\uparrow (B\uparrow A))\uparrow ((B\uparrow A)\uparrow [(A\uparrow B)\uparrow (A\uparrow B)])])$ deduction

$\lnot A$ hypothesis

$\lnot A\to (A\uparrow B)$ theorem 4

$A\uparrow B$ modus ponens

$(A\uparrow B)\to ((A\uparrow B)\to \lnot [(A\uparrow B)\uparrow (A\uparrow B)])$ theorem 3

$(A\uparrow B)\to \lnot [(A\uparrow B)\uparrow (A\uparrow B)]$ modus ponens

$\lnot [(A\uparrow B)\uparrow (A\uparrow B)]$ modus ponens

$\lnot [(A\uparrow B)\uparrow (A\uparrow B)]\to ((B\uparrow A)\uparrow [(A\uparrow B)\uparrow (A\uparrow B)])$ theorem 5

$(B\uparrow A)\uparrow [(A\uparrow B)\uparrow (A\uparrow B)]$ modus ponens

$\lnot A\to (A\uparrow (B\uparrow A))$ theorem 4

$A\uparrow (B\uparrow A)$ modus ponens

$(A\uparrow (B\uparrow A))\to (((B\uparrow A)\uparrow [(A\uparrow B)\uparrow (A\uparrow B)])\to \lnot [(A\uparrow (B\uparrow A))\uparrow ((B\uparrow A)\uparrow [(A\uparrow B)\uparrow (A\uparrow B)])])$ theorem 3

$((B\uparrow A)\uparrow [(A\uparrow B)\uparrow (A\uparrow B)])\to \lnot [(A\uparrow (B\uparrow A))\uparrow ((B\uparrow A)\uparrow [(A\uparrow B)\uparrow (A\uparrow B)])]$ modus ponens

$\lnot [(A\uparrow (B\uparrow A))\uparrow ((B\uparrow A)\uparrow [(A\uparrow B)\uparrow (A\uparrow B)])]$ modus ponens

$\lnot [(A\uparrow (B\uparrow A))\uparrow ((B\uparrow A)\uparrow [(A\uparrow B)\uparrow (A\uparrow B)])]\to ((A\uparrow (B\uparrow A))\uparrow [(A\uparrow (B\uparrow A))\uparrow ((B\uparrow A)\uparrow [(A\uparrow B)\uparrow (A\uparrow B)])])$ theorem 5

$(A\uparrow (B\uparrow A))\uparrow [(A\uparrow (B\uparrow A))\uparrow ((B\uparrow A)\uparrow [(A\uparrow B)\uparrow (A\uparrow B)])]$ modus ponens

$\lnot A\to ((A\uparrow (B\uparrow A))\uparrow [(A\uparrow (B\uparrow A))\uparrow ((B\uparrow A)\uparrow [(A\uparrow B)\uparrow (A\uparrow B)])])$ deduction

$(A\to ((A\uparrow (B\uparrow A))\uparrow [(A\uparrow (B\uparrow A))\uparrow ((B\uparrow A)\uparrow [(A\uparrow B)\uparrow (A\uparrow B)])]))\to ((\lnot A\to ((A\uparrow (B\uparrow A))\uparrow [(A\uparrow (B\uparrow A))\uparrow ((B\uparrow A)\uparrow [(A\uparrow B)\uparrow (A\uparrow B)])]))\to ((A\uparrow (B\uparrow A))\uparrow [(A\uparrow (B\uparrow A))\uparrow ((B\uparrow A)\uparrow [(A\uparrow B)\uparrow (A\uparrow B)])]))$ theorem 6

$(\lnot A\to ((A\uparrow (B\uparrow A))\uparrow [(A\uparrow (B\uparrow A))\uparrow ((B\uparrow A)\uparrow [(A\uparrow B)\uparrow (A\uparrow B)])]))\to ((A\uparrow (B\uparrow A))\uparrow [(A\uparrow (B\uparrow A))\uparrow ((B\uparrow A)\uparrow [(A\uparrow B)\uparrow (A\uparrow B)])])$ modus ponens

$(A\uparrow (B\uparrow A))\uparrow [(A\uparrow (B\uparrow A))\uparrow ((B\uparrow A)\uparrow [(A\uparrow B)\uparrow (A\uparrow B)])]$ modus ponens QED

You see how theorem 6 works together with the deduction step of the deduction metatheorem. OK? JRSpriggs (talk) 05:58, 1 October 2018 (UTC)

We do not have to use P to represent "P is true" and ¬P to represent "P is false"; there are other options. So here I will show one.

If F is the formula that we are trying to prove, we could use (P→F)→F to represent "P is true (or F is true)" and P→F to represent "P is false (or F is true)". In our example with the Sheffer stroke, this would change the needed theorems (after theorems 1 and 2 for the deduction meta-theorem, which do not change) to:

3. $((P\to F)\to F)\to (((Q\to F)\to F)\to ((P\uparrow Q)\to F)))$,

4. $(P\to F)\to (((P\uparrow Q)\to F)\to F)$, and

5. $(Q\to F)\to (((P\uparrow Q)\to F)\to F)$.

When the induction on sub-formulas reaches F, we would have (F→F)→F (if F is true in the valuation in question) which reduces to F itself (since F→F is a theorem by the deduction meta-theorem). The results of the deduction steps would be ((P→F)→F)→F and (P→F)→F. So we can get F by modus ponens rather than using a variant of theorem 6. JRSpriggs (talk) 00:30, 3 October 2018 (UTC)

Completeness of Mendelson's axioms for implication and negation

Mendelson uses the usual two axioms to get the deduction meta-theorem:

1. P→(Q→P)

2. (P→(Q→R))→((P→Q)→(P→R))

and one powerful axiom to handle negation and two-valuedness:

3. (¬P→¬Q)→((¬P→Q)→P).

To show their completeness, I use a somewhat different approach than he used in his book. I derive these seven theorems which are clearly sufficient (in light of what I said above) to establish completeness:

The first two are just his first two axioms, used for the same purpose to get the deduction meta-theorem. So their derivation is trivial.

1. P→(Q→P)

2. (P→(Q→R))→((P→Q)→(P→R))

If the conclusion of an implication is true, then the implication is true:

3. ((Q→F)→F)→(((P→Q)→F)→F)

Q→(P→Q) axiom 1

(P→Q)→F hypothesis

Q hypothesis

P→Q modus ponens

F modus ponens

Q→F deduction

((P→Q)→F)→(Q→F) deduction

(Q→F)→F hypothesis

(P→Q)→F hypothesis

Q→F modus ponens

F modus ponens

((P→Q)→F)→F deduction

((Q→F)→F)→(((P→Q)→F)→F) deduction QED

If the hypothesis of an implication is true and the conclusion is false, then the implication is false:

4. ((P→F)→F)→((Q→F)→((P→Q)→F))

(P→F)→F hypothesis

Q→F hypothesis

P→Q hypothesis

P hypothesis

Q modus ponens

F modus ponens

P→F deduction

F modus ponens

(P→Q)→F deduction

(Q→F)→((P→Q)→F) deduction

((P→F)→F)→((Q→F)→((P→Q)→F)) deduction QED

If the hypothesis of an implication is false, then the implication is true:

5. (P→F)→((P→Q)→F)→F)

The proof of theorem 5 requires that we first show Peirce's law and some other lemmas:

(¬P→¬P)→((¬P→P)→P) axiom 3

¬P hypothesis

¬P→¬P deduction

(¬P→P)→P modus ponens (lemma 1)

(¬Q→¬P)→((¬Q→P)→Q) axiom 3

¬P hypothesis

¬P→(¬Q→¬P) axiom 1

¬Q→¬P modus ponens

(¬Q→P)→Q modus ponens

P hypothesis

P→(¬Q→P) axiom 1

¬Q→P modus ponens

Q modus ponens

P→Q deduction

¬P→(P→Q) deduction (lemma 2)

(P→Q)→P hypothesis

¬P hypothesis

P→Q modus ponens (from lemma 2)

P modus ponens

¬P→P deduction

P modus ponens (from lemma 1)

((P→Q)→P)→P deduction (Peirce's law)

P→F hypothesis

(P→Q)→F hypothesis

F→Q hypothesis

P hypothesis

F modus ponens

Q modus ponens

P→Q deduction

F modus ponens

(F→Q)→F deduction

((F→Q)→F)→F Peirce's law

F modus ponens

((P→Q)→F)→F deduction

(P→F)→(((P→Q)→F)→F) deduction QED

If P is true, then ¬P is false:

6. ((P→F)→F)→(¬P→F)

¬P→(P→F) lemma 2

(P→F)→F hypothesis

¬P hypothesis

P→F modus ponens

F modus ponens

¬P→F deduction

((P→F)→F)→(¬P→F) deduction QED

If P is false, then ¬P is true:

7. (P→F)→((¬P→F)→F)

The proof of theorem 7 also requires some lemmas leading to the contra-positive:

(¬P→¬¬P)→((¬P→¬P)→P) axiom 3

¬¬P hypothesis

¬¬P→(¬P→¬¬P) axiom 1

¬P→¬¬P modus ponens

(¬P→¬P)→P modus ponens

¬P hypothesis

¬P→¬P deduction

P modus ponens

¬¬P→P deduction (lemma 3)

(¬¬¬P→¬P)→((¬¬¬P→P)→¬¬P) axiom 3

¬¬¬P→¬P lemma 3

(¬¬¬P→P)→¬¬P modus ponens

P hypothesis

P→(¬¬¬P→P) axiom 1

¬¬¬P→P modus ponens

¬¬P modus ponens

P→¬¬P deduction (lemma 4)

(¬¬P→¬¬Q)→((¬¬P→¬Q)→¬P) axiom 3

P→Q hypothesis

¬¬P hypothesis

¬¬P→P lemma 3

P modus ponens

Q modus ponens

Q→¬¬Q lemma 4

¬¬Q modus ponens

¬¬P→¬¬Q deduction

(¬¬P→¬Q)→¬P modus ponens

¬Q hypothesis

¬Q→(¬¬P→¬Q) axiom 1

¬¬P→¬Q modus ponens

¬P modus ponens

¬Q→¬P deduction

(P→Q)→(¬Q→¬P) deduction (contra-positive)

(¬F→¬¬P)→((¬F→¬P)→F) axiom 3

P→F hypothesis

(P→F)→(¬F→¬P) contra-positive

¬F→¬P modus ponens

¬P→F hypothesis

(¬P→F)→(¬F→¬¬P) contra-positive

¬F→¬¬P modus ponens

(¬F→¬P)→F modus ponens

F modus ponens

(¬P→F)→F deduction

(P→F)→((¬P→F)→F) deduction QED

Now, having proven all seven required theorems, we know that Mendelson's axiom system is complete. To show that another axiom system for implication and negation is complete, we could either prove the same seven theorems from it or we could prove the three axioms of Mendelson's system instead. JRSpriggs (talk) 03:34, 9 October 2018 (UTC)

Łukasiewicz's third axiom system is very similar to Mendelson's. The only difference is in axiom 3

$(\lnot P\to \lnot Q)\to ({\color {OliveGreen}(\neg P\to }Q{\color {OliveGreen})}\to P)$

where Łukasiewicz's axiom lacks the part in green. That part tends to strengthen Mendelson's axiom. Nonetheless, Łukasiewicz's system is still complete as I will show by deducing Mendelson's version of the third axiom from Łukasiewicz's version. To show:

3. (¬P→¬Q)→((¬P→Q)→P).

¬Q hypothesis

¬Q→(¬P→¬Q) axiom 1

¬P→¬Q modus ponens

(¬P→¬Q)→(Q→P) axiom 3

Q→P modus ponens

¬Q→(Q→P) deduction (lemma 1)

¬P→¬Q hypothesis

¬P→Q hypothesis

¬P hypothesis

¬Q modus ponens

Q modus ponens

¬Q→(Q→¬(P→P)) lemma 1

Q→¬(P→P) modus ponens

¬(P→P) modus ponens

¬P→¬(P→P) deduction

(¬P→¬(P→P))→((P→P)→P) axiom 3

(P→P)→P modus ponens

P hypothesis

P→P deduction

P modus ponens

(¬P→Q)→P deduction

(¬P→¬Q)→((¬P→Q)→P) deduction QED

So Łukasiewicz's third axiom system is complete. JRSpriggs (talk) 21:25, 17 October 2018 (UTC)

Completeness of Hilbert's system

To establish the completeness of Hilbert's system, we derive from it the axioms of Łukasiewicz's third system.
Axioms of Hilbert's system:

1. A→(B→A)

2. (A→(B→C))→(B→(A→C))

3. (B→C))→((A→B)→(A→C))

4. A→(¬A→B)

5. (A→B)→((¬A→B)→B)

Theorems:

6. (A→(B→A))→(B→(A→A)) 2

7. B→(A→A) mp 1,6

8. (A→(B→A))→(A→A) 7

9. A→A mp 1,8

10. (A→A)→((¬A→A)→A) 5

11. (¬A→A)→A mp 9,10

12. [(B→C))→((A→B)→(A→C))]→[(A→B)→((B→C)→(A→C))] 2

13. (A→B)→((B→C)→(A→C)) mp 3,12

14. [A→(¬A→B)]→[¬A→(A→B)] 2

15. ¬A→(A→B) mp 4,14

16. (¬A→(A→B))→[((A→B)→A)→(¬A→A)] 13

17. ((A→B)→A)→(¬A→A) mp 15,16

18. (((A→B)→A)→(¬A→A))→[((¬A→A)→A)→(((A→B)→A)→A)] 13

19. ((¬A→A)→A)→(((A→B)→A)→A) mp 17,18

20. ((A→B)→A)→A mp 11,19

21. (A→(A→C))→[((A→C)→C)→(A→C)] 13

22. [((A→C)→C)→(A→C)]→(A→C) 20

23. ((A→(A→C))→[((A→C)→C)→(A→C)])→[([((A→C)→C)→(A→C)]→(A→C))→((A→(A→C))→(A→C))] 13

24. ([((A→C)→C)→(A→C)]→(A→C))→((A→(A→C))→(A→C)) mp 21,23

25. (A→(A→C))→(A→C) mp 22,24

26. ((B→C)→(A→C))→[(A→(B→C))→(A→(A→C)))] 3

27. [(A→B)→((B→C)→(A→C))]→([((B→C)→(A→C))→[(A→(B→C))→(A→(A→C)))]]→[(A→B)→[(A→(B→C))→(A→(A→C))]]) 13

28. [((B→C)→(A→C))→[(A→(B→C))→(A→(A→C)))]]→[(A→B)→[(A→(B→C))→(A→(A→C))]] mp 13,27

29. (A→B)→[(A→(B→C))→(A→(A→C))] mp 26,28

30. ((A→B)→[(A→(B→C))→(A→(A→C))])→((A→(B→C))→[(A→B)→(A→(A→C))]) 2

31. (A→(B→C))→[(A→B)→(A→(A→C))] mp 29,30

32. ((A→(A→C))→(A→C))→[((A→B)→(A→(A→C)))→((A→B)→(A→C))] 3

33. ((A→B)→(A→(A→C)))→((A→B)→(A→C)) mp 25,32

34. [((A→B)→(A→(A→C)))→((A→B)→(A→C))]→[((A→(B→C))→((A→B)→(A→(A→C))))→((A→(B→C))→((A→B)→(A→C)))] 3

35. ((A→(B→C))→((A→B)→(A→(A→C))))→((A→(B→C))→((A→B)→(A→C))) mp 33,34

36. (A→(B→C))→((A→B)→(A→C)) mp 31,35

Now we have proven the two theorems, 1 and 36, needed to make the deduction theorem work. So we can switch to that, much easier, method of proof.

¬A→¬B hypothesis

B hypothesis

¬A hypothesis

¬B modus ponens

B→(¬B→A) 4

¬B→A modus ponens

A modus ponens

¬A→A deduction

(¬A→A)→A 11

A modus ponens

B→A deduction

(¬A→¬B)→(B→A) deduction QED (converse contra-positive)

These are the three axioms of Łukasiewicz's third system (which we showed above was complete), our theorems: 1, 36, and converse contra-positive. So we have proved that Hilbert's system is complete. JRSpriggs (talk) 06:38, 19 October 2018 (UTC)

@JRSpriggs: Nice! I think this stuff belongs inside the article (or another article if you prefer), not (just) in the talk page. Dan Gluck (talk) 11:14, 23 July 2020 (UTC)

P.S I haven't reviewed the proofs (yet?)Dan Gluck (talk) 11:15, 23 July 2020 (UTC)

At the time I wrote this, I was trying to comply with the wishes of EmilJ (talk · contribs) which he expressed at Talk:Implicational propositional calculus where he said "... no more proofs, please. There should be less proofs in the article, not more. This is an encyclopedia, not a textbook.". I think his point was that we require verifiability, not proof. Indeed, a proof like this would be considered Original Research, the original sin of encyclopedia writers. I was trying to get around that by putting my proofs on the talk pages where standards are looser. JRSpriggs (talk) 12:21, 23 July 2020 (UTC)

Why is Rosser's system not included in the list?

Basic symbols: $\neg$ and $\wedge$

Axiom schemes:

1) $p\rightarrow p\wedge p$

2) $p\wedge q\rightarrow p$

3) $\left(p\rightarrow q\right)\rightarrow \left[\neg \left(q\wedge r\right)\rightarrow \neg \left(r\wedge p\right)\right]$

Inference rule: Modus Ponens.

- Aris Makridis (talk) 13:41, 24 October 2023 (UTC)

I do not see a section in the article on logics based on conjunction and negation. If you find a another reference for such a logic, then you could reasonably add such a section with Rosser and the other reference to support it. JRSpriggs (talk) 07:23, 26 October 2023 (UTC)

See Rosser J. Barkley, "Logic for Mathematicians", New York, McGraw-Hill, 1953. Here is a link:

https://archive.org/details/logicformathemat00ross/mode/2up

So, I am adding the section. Aris Makridis (talk) 07:43, 31 October 2023 (UTC)