How can one prove that every propositional tautology, expressed with
the connectives '$\neg$' and '$\rightarrow$', can be proved with the axioms below?

(P0. $\phi \to \phi$)

P1. $\phi \to \left( \psi \to \phi \right)$

P2. $\left( \phi \to \left( \psi \rightarrow \xi \right) \right) \to \left( \left( \phi \to \psi \right) \to \left( \phi \to \xi \right) \right)$

P3. $\left ( \lnot \phi \to \lnot \psi \right) \to \left( \psi \to \phi \right)$

I'm especially interested in an eventual math-style proof:

Since all logical expressions have equivalents in form of elements in a Boolean ring with respect to XOR, AND and TRUE, and any tautology reduces to 1 in that ring, the Hilbert axioms can prove every tautology if they can prove all the axioms for a Boolean ring for the equivalents of $(1,\oplus,\cdot)$ expressed in only $(\neg,\rightarrow)$.

S1. $1\leftrightarrow (A\rightarrow A)$

S2. $AB\leftrightarrow\neg(A\rightarrow \neg B)$

S3. $A+B\leftrightarrow((A\rightarrow B)\rightarrow\neg(\neg A\rightarrow\neg B)) $

How to use P1-P3 to prove axioms of Boolean rings expressed with the substitution rules S1-S3? For example:

  • the law of commutativity for multiplication: $\neg(A\rightarrow\neg B)\rightarrow\neg(B\rightarrow\neg A)$
  • the law of multiplicative idempotence: $\neg(A\rightarrow\neg A)\rightarrow A$ and $A\rightarrow\neg(A\rightarrow\neg A)$
  • 1
    $\begingroup$ Google propositional calculus, completeness theorem.The answer depends on what you already know as from first principles it's a bit too complicated. $\endgroup$ – Git Gud Sep 26 '14 at 19:15
  • 1
    $\begingroup$ P1 is provable from P2 and P3. $\endgroup$ – Mauro ALLEGRANZA Sep 26 '14 at 19:21
  • 1
    $\begingroup$ @DougSpoonwood I spent many happy hours playing around with Lukasiewicz' axioms. Proving even quite simple things is hard. But some of the proofs are relatively short and can be proved by rather crude software (just try all possible sets of 10 or 20 steps and see if you hit what you want along the way). But I was completely unable to get any real intuition on how to do it by hand. I have no idea how he found some of the 1 or 2 axiom systems. But having got them, it is rather easier to show they work. There are dozens of published papers in the area (maybe far more). $\endgroup$ – almagest Oct 2 '14 at 16:19
  • 1
    $\begingroup$ @DougSpoonwood I was looking for novel Olympiad-style problems, but could not find any that I regarded as fair or reasonable! :) $\endgroup$ – almagest Oct 2 '14 at 16:22
  • 1
    $\begingroup$ @almagest Zeman's book gives you a way to do condensed detachment by hand: clas.ufl.edu/users/jzeman/modallogic/chapter01.htm It is possible to do that in an infix notation also. In my experience I've found the following process workable. I first set up something like the corresponding "natural deduction" system using only modus ponens as a rule of inference in one notebook. Then I use the proof procedure of the deduction metatheorem to change the "natural deduction" system proof into the axiomatic proof alternating back and forth between two notebooks.... but (1/2) $\endgroup$ – Doug Spoonwood Oct 2 '14 at 16:33

Essentially you are asking why every tautology is provable, I post here a demonstration taken from my own notes.

$\varphi$ is any propositional fromula.

Let $v$ be a truth assignment and let $A_1, \ldots ,A_k$ be the propositional variables in $\varphi$. Define

$$\psi_i=\begin{cases} A_i & v(A_i)=T\\ \neg A_i & v(A_i)=F\end{cases}$$

And let

$$\theta=\begin{cases} \varphi & v( \varphi)=T\\ \neg \varphi & v( \varphi)=F\end{cases}$$

Then we claim

$$\{ \psi_1, \ldots , \psi_k \} \vdash \theta$$ This is proved by induction on the number of connectives in $\varphi$. If there are no connectives then $\varphi$ is a propositional variable and the statement is trivial. Assume $\varphi =\neg \eta$. And let $v(\eta)=F$, then we have by induction $$\{ \psi_1, \ldots , \psi_k \} \vdash \neg \eta$$ which is the same as $$\{ \psi_1, \ldots , \psi_k \} \vdash \varphi$$ which is what is desired since $v(\varphi)=T$.

Now let $v(\eta)=T$

Then by induction $$\{ \psi_1, \ldots , \psi_k \} \vdash \eta.$$

In this case $v(\varphi)=F$, and so we have to show $$\{ \psi_1, \ldots , \psi_k \} \vdash \neg \varphi$$ or $$\{ \psi_1, \ldots , \psi_k \} \vdash \neg \neg \eta$$ But this follows since $\vdash \eta \rightarrow \neg \neg \eta$.

Now assume that

$\varphi =\eta \rightarrow \sigma$

If $v(\varphi)=T$ then either $v(\sigma)=T$ in which case, $$\{ \psi_1, \ldots , \psi_k \} \vdash \sigma $$ and $$\vdash \sigma \rightarrow (\eta \rightarrow \sigma)$$ or $v(\eta)=F$ for which $$\{ \psi_1, \ldots , \psi_k \} \vdash \neg \eta $$

and $$\vdash \neg \eta \rightarrow (\eta \rightarrow \sigma).$$

The final case is where

$v(\varphi)=F$ and so $v(\eta)=T$ and $v(\sigma)=F$. Thus we have $$\{ \psi_1, \ldots , \psi_k \} \vdash \eta $$ $$\{ \psi_1, \ldots , \psi_k \} \vdash \neg \sigma $$

and from the last theorem we have

$$\vdash \eta \rightarrow [\neg \sigma \rightarrow \neg ( \eta \rightarrow \sigma)].$$

Now to prove the completeness theorem, let $v$ and $w$ be truth assignments such that $v(A_i)=w(A_i)$ for $i<k$ and $v(A_k)\neq w(A_k)$ this means that if $\varphi$ is a tautology, we have $$\{ \psi_1, \ldots , \psi_{k-1}, A_k \} \vdash \varphi$$

and $$\{ \psi_1, \ldots , \psi_{k-1}, \neg A_k \} \vdash \varphi$$


$$\{ \psi_1, \ldots , \psi_{k-1}, \} \vdash \varphi$$

proceeding in this way we obtain $$\vdash \varphi.$$

  • $\begingroup$ Wow! I will study this later, but just a question: with provable you mean provable with just those three to four axioms? $\endgroup$ – Lehs Sep 26 '14 at 19:55
  • $\begingroup$ @Lehs Yes, and actually the first can be proved from the rest. $\endgroup$ – Rene Schipperus Sep 26 '14 at 20:02

See Derek Goldrei, Propositional and Predicate Calculus : A Model of Argument (2005).

See page 87 for the defnition of The formal system S that is based on your P2-P3-P4, of course with modus ponens.

See page 92 for the derivation of your P1 from P2 and P3.

See page 106 for the proof of

Theorem 3.9 Completeness theorem for S.

  • $\begingroup$ so at least there seems to be one interesting result from mathematical underground. $\endgroup$ – Lehs Sep 26 '14 at 19:37
  • $\begingroup$ Is the axioms from Wikipedia faulty or incomplete? $\endgroup$ – Lehs Sep 26 '14 at 19:39
  • $\begingroup$ @Lehs I dont understand your comment, can you please explain the joke to me. $\endgroup$ – Rene Schipperus Sep 26 '14 at 19:46
  • $\begingroup$ @Lehs - NO. The Wiki's page, after the list of the four axioms says : "The axiom P1 is redundant, as it follows from P3, P2 and modus ponens." This is exactly what I've written above ... $\endgroup$ – Mauro ALLEGRANZA Sep 26 '14 at 19:51

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.