In Propositional Logic, one is often tasked with showing that some particular formula is a theorem of a given deductive system, i.e. $\emptyset \vdash \psi$. These formulas can look very simple and intuitive, e.g. $(\alpha \rightarrow \alpha)$, but the derivation can be rather cumbersome. That examples takes around 6 steps for instance, and is one of the simpler cases.

My question is immediate then: Is there any way of anticipating the correct strategy for making such derivations, and thus avoiding the lengthy 'trial and error' process of applying different axioms (and rules of inference) until something works?

Essentially, are there any 'tricks' that are unlikely to appear in notes etc. but which you are aware of the help look ahead and spot the right path?

For completeness (no pun intended), I've included the particular deductive system I am working with below, and a few indicative theorems.

$((\neg \alpha \rightarrow \alpha)\rightarrow\alpha))$




The above cases can be dealt with a little more tidily by applying the Deduction Theorem. Do any other results like this exist? Also, supposing the Deduction Theorem cannot be used, do strategies still exist?

Let $\mathcal{L}_0=\mathcal{L}[\{\neg, \rightarrow\}]$. Define the system $L_0$ as follows:

An axiom of $L_0$ is any formula of $\mathcal{L}_0$ of the form

  • (A1) $(\alpha \rightarrow ( \beta \rightarrow \alpha))$
  • (A2) $((\alpha \rightarrow ( \beta \rightarrow \gamma) \rightarrow ((\alpha \rightarrow \beta) \rightarrow ( \alpha \rightarrow \gamma)))$
  • (A3) $((\neg \beta \rightarrow \neg \alpha ) \rightarrow (\alpha \rightarrow \beta))$

The only rule of inference in $L_0$ is modus ponens, i.e. from $\alpha$ and $(\alpha \rightarrow \beta)$ infer $\beta$.

  • $\begingroup$ One possible strategy is to use the proof of the deduction theorem to find the formal proof. $\endgroup$ – Git Gud Apr 16 '14 at 9:15
  • 1
    $\begingroup$ Ah, the age-old question of how to do Hilbert-style proofs. We'd all benefit if someone dedicated a book on how to work with them. There are some relevant posts here with suggestions, search for Hilbert. $\endgroup$ – Hunan Rostomyan Apr 16 '14 at 9:15
  • $\begingroup$ One might look into using a theorem prover. There exist certain strategies one can use when using a theorem prover also, such as resonance and using hints. $\endgroup$ – Doug Spoonwood Jun 3 '14 at 17:31

Some proofs of the completeness of a propositional proof system can actually be turned easily to an algorithm for proving any propositional statement $Q$ from a proposition statement $P$ if $Q$ is a consequence of $P$

This gives you a strategy for always finding proofs of propositional consequences.

  • $\begingroup$ @DougSpoonwood I understand what you mean and I will edit it. Thanks. $\endgroup$ – Amr Jun 3 '14 at 17:47


In Propositional Logic, one is often tasked with showing that some particular formula is a theorem of a given deductive system [of a Hilbert style]

Often tasked by whom? Teachers with a very mean streak, perhaps. But surely very rarely in real logical life, so to speak. If you genuinely want to know whether a bunch of propositional assumptions do or don't entail a given conclusion (not just because some instructor asks you, and moreover asks you to do it with one hand tied behind your back), either you do a truth-table, or (usually faster) use a tableau, or (if you think the argument is valid and just want to confirm that) run up an informal natural deduction proof (the clue is in the name! -- such proofs do indeed regiment natural ways of reasoning).

Over three-quarters of a century since Gentzen, it is pretty odd still to be making students tackle Hilbert systems. For there is very little serious logical interest in the combinatorial puzzle-solving task of finding Hilbert proofs (as opposed to proofs in more user-friendly systems of logic).


  • $\begingroup$ This isn't an answer. One can also talk about how finding the shortest axiom for a given system under a given rule also necessitates a serious logical interest in finding such Hilbert proofs, and how theorem provers have gotten employed for finding such proofs. $\endgroup$ – Doug Spoonwood Apr 19 '14 at 12:34
  • $\begingroup$ It isn't an answer, it's a sermon. Or rant. But it is worth occasionally saying, as we don't want beginning students put off logic by having to tangle from the off with user-unfriendly Hilbert systems ... $\endgroup$ – Peter Smith Apr 19 '14 at 12:37
  • $\begingroup$ Truth tables aren't possible for any infinite-valued logic, and natural deduction systems aren't feasible for say Lukasiewicz infinite-valued logic. Natural deduction systems also can get characterized as misleading in that introduction and elimination rules sometimes do not enable the deduction of all tautologies for a given connective. The introduction and elimination rules for "C" do not enable you to deduce CCCpqpp, nor doe the introduction and elimination rules for "E" (and those for "C") enable you to deduce EEEpqrEpEqr. $\endgroup$ – Doug Spoonwood Jun 3 '14 at 17:13
  • $\begingroup$ Using a truth table only tells you that a result holds for a particular model (or a certain class of models similar to a prototype). A formal proof on the other hand tells you that for any model of the formulas of the system, a certain result holds under the conditions of the formal system (given soundness). As too simple of any example, if you prove CCCpqrCqr from CCpqCCqrCpr and CpCqp under detachment, the formal proof tells that for any suitable model for "C", CCCpqrCqr follows. This includes 2-valued logic, Lukasiewicz 3-valued logic, AND Lukasiewicz infinite-valued logic. $\endgroup$ – Doug Spoonwood Jun 3 '14 at 17:23
  • $\begingroup$ Natural deduction derivations of theorems also only end up proving one theorem at a time. Truth-tables also only end up only establishing one tautology at a time. Admittedly they can give you other tautologies when you interpret them, but even then they only give you tautologies according to a pattern of sorts. On the other hand, Hilbert-Frege style proofs (usually) end up establishing many theorems when someone tries to prove just one theorem. For instance, if you prove CCpqCCrpCrq in the Hilbert-Frege system {CpCqp, CCpCqrCCpqCpr} you'll prove two other theorems along the way... $\endgroup$ – Doug Spoonwood Oct 13 '14 at 5:42

There exists a similar question here... my best response to that question may be the September 30th response (I employ the same conventions in this answer as I did in that answer). Condensed detachment may help, as well as using a theorem-prover.

For this system you can prove everything by the deduction (meta) theorem, a theorem which allows to get NCpNq (this is Polish notation) from "p" and "q", and a form of proof-by-contradiction. The proof-by-contradiction roughly goes "if we assume the negation of a well-formed formula "Nw" and it leads to a contradiction, then the formula "w" is either a theorem or true under the scope of the other hypotheses." The relevant theorems you need for this are (in Polish notation):

Recursive Letter Prefixing [RLP]: CpCqp

Self-Distribution [SD]: CCpCqrCCpqCpr [these two give you The Deduction Theorem, and if you have The Deduction Theorem, then these two are theorems].

Conjunction-introduction [Ki]: CpCqNCpNq.


Negation elimination [No]: CCNpNCqNNqp.

I used Prover9 to find proofs of the last two theorems in this system.

Proofs of CNNpp and CNpCpq emerged when I ran Prover9 for the proofs of negation elimination and conjunction introduction. Now say you want to prove Clavius: CCNppp, which you mentioned before. We can assume CNpp as a hypothesis and proceed as follows.

 hypothesis 1 |  CNpp  
 hypothesis 2 || Np   
 D1.2       3 || p    
 D[Ki.3]*4  4 || CNaNCpNa
 D4.2*5     5 || NCpNNp
 Ci 2-5 *6  6 |  CNpNCpNNp
 D[No.6]*7  7 |  p
 Ci 1-7*8   8    CCNppp

C2-2 is the law of identity. C2-3 is the hypothesis.

 hypothesis   1 | CNpp
 D[RLP.Ki]*2  2 | CaCbCcNCbNc  (this enables C2-Ki)
 D[SD.2]*3    3 | CCabCaCcNCbNc  
 D3.1*4       4 | CNpCcNCpNc  (this enables C2-4)
 D[SD.4]*5    5 | CCNpcCNpNCpNc
 D5.[Cpp]*6   6 | CNpNCpNNp
 D[No.6]*7    7 | p
 Ci 1-7*8     8   CCNppp

 axiom        0 CCNpNqCqp (not used here)
 axiom        1 CpCqp
 axiom        2 CCpCqrCCpqCpr
 theorem      3 CpCqNCpNq
 theorem      4 CCNpNCqNNqp
 D2.1*5       5 CCpqCpp
 D5.1*6       6 Cpp  (this enables C1-1)
 D1.3*7       7 CpCqCrNCqNr (this enables C1-Ki)
 D1.4*8       8 CpCqCrCsNCrNs (this enables C1-2)
 D1.1*9       9 CpCqCrq (this enables C1-RLP)
 D1.2*10     10 CpCCqCrsCCqrCqs
 D2.10*11    11 CCpCqCrsCpCCqrCqs
 D11.8*12    12 CpCCqrCqCsNCrNs (this enables C1-3) 
 D12.6*13    13 CCpqCpCrNCqNr (this enables C1-4)
 D11.3*14    14 CCpqCCprCpNCqNr (this enables C1-5)  
 D1.6*15     15 CpCqq (this enables C1-Cpp)
 C2.14*16    16 CCCpqCprCCpqCpNCqNr
 D16.15*17   17 CCpqCpNCqNp  (this enables C1-6)
 D1.4*18     18 CpCCNqNCrNNrq
 D2.18*19    19 CCpCNqNCrNNrCpq
 D19.17*20   20 CCNppp

A useful pattern here is to take any axiom or theorem "x", then go D[RLP.x], and then distribute that result. D[SD].[D[RLP.x]]. Interestingly enough, you can prove CNpCpq by starting this way... D D[SD].[D[RLP.0]].[RLP] is a proof of CNpCpq.


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.