As in the title, the question is

Give a natural deduction proof of $\varphi\vdash\top$, where $\varphi$ is any formula.

Could I do this proof by deriving $\varphi \rightarrow \top$ with $ \rightarrow$-introduction rule which says that if you can derive a formula $\psi$ from a formula $\varphi$, then $\varphi \rightarrow \psi$ is true. So, with this derivation I will use $\varphi$ as an assumption and derive from $\varphi$, or am I thinking wrong? I prefer hints before solution!

  • $\begingroup$ No, it is not :P I am going to derive $\top$ from $φ$. But I wounder if I can proof that the derivation of $\top$ from $φ$ can be done by derive $\varphi \rightarrow \top$ instead. $\endgroup$ – Anna Sep 18 '14 at 8:16
  • $\begingroup$ Of course, if you have derived $\varphi \rightarrow \top$, then obviously assuming $\varphi$ licenses you to conclude with $\top$. But how you think to derive $\varphi \rightarrow \top$? if not using $\rightarrow$-intro from $\varphi \vdash \top$ ... And so we are back to the start. $\endgroup$ – Mauro ALLEGRANZA Sep 18 '14 at 8:27
  • $\begingroup$ I were thinking that I could start with the conclusion that $\varphi \rightarrow \top$ is true. Then I would use $\rightarrow-introduction$ rule to get and then use $V-elimination$ rule to get, above this line, $\varphi V\top$ and a derivation from $\varphi$, respectively $\top$, to $\top$. @MauroALLEGRANZA $\endgroup$ – Anna Sep 18 '14 at 8:32
  • $\begingroup$ I'm not sure about it ... You have to try to write it and see if it's right. If you assume $\varphi → ⊤$, are you sure that you are able to discharge it ? $\endgroup$ – Mauro ALLEGRANZA Sep 18 '14 at 8:41
  • $\begingroup$ The way I was taught, the Natural Deduction calculus had a $\top$ formation rule. That was kind of the whole use of introducing the predicate $\top$ in the first place. It might help to reference what exposition of Natural Deduction you are following. $\endgroup$ – Marcel Besixdouze Feb 21 '15 at 8:40


I'll give you an answer in Hilbert-style, and I suggest you to try to convert it into Natural Deduction.

A quite "ubiquitous" axiom in Hilbert-style propositional logic is :

$\vdash \psi \rightarrow (\varphi \rightarrow \psi)$.

Thus, if we can prove $\vdash \psi$, we can use modus ponens (i.e. $\rightarrow$-elimination) to conclude with :

$\vdash \varphi \rightarrow \psi$.

The lesson is :

if we have proved a formula $\psi$, we can always add a "premise" $\varphi$ whatever to assert $\vdash \varphi \rightarrow \psi$.

Thus, the question suggests the following strategy : we have to prove : $\vdash \top$ and then use it as $\psi$ above.


i) $\varphi$ --- assumed

ii) $\bot$ --- assumed

iii) $\bot \vdash \bot$ --- from ii)

iv) $\vdash \bot \rightarrow \bot$ --- from iii) by $\rightarrow$-intro

v) $\vdash \lnot \bot$ --- by def of $\lnot$

vi) $\vdash \top$ --- abbreviation.

Thus, from i) and vi) :

$\varphi \vdash \top$.

  • $\begingroup$ Since $\top$ is a 0-ary conjuction it should have 0 formulas above the line and the formula $\top$ below it. And accordning to the same analogy, it sohuld have 0 eliminatiuon rules. Therefore we can conclude that $\top$ symbolizes the true proposition? $\endgroup$ – Anna Sep 18 '14 at 8:49
  • $\begingroup$ Are my argument enought to prove $\vdash \top$ ? @MauroALLGRANZA $\endgroup$ – Anna Sep 18 '14 at 9:15
  • $\begingroup$ thanks :) @MauroALLEGRANZA $\endgroup$ – Anna Sep 18 '14 at 9:29
  • $\begingroup$ @Anna - Basically it's right, but in Natural Deduction ⊤ is not primitive; thus, there are no rules for it. But it is defined as : ¬⊥ ... and at this point we have the solution. Assume $\bot$; then $\bot \vdash \bot$. Apply $\rightarrow$-intro : $\vdash \bot \rightarrow \bot$ which, by def of $\lnot$ is : $\vdash \lnot \bot$ which we abbreviate as : $\vdash \top$. $\endgroup$ – Mauro ALLEGRANZA Sep 18 '14 at 9:30
  • $\begingroup$ Do you recommend any good page about these kinds of proofs? $\endgroup$ – Anna Sep 18 '14 at 10:10

Here is one way that might be proven using explosion (X), negation introduction (¬I), contradiction introduction (⊥I) and conditional introduction (→I).

To implement this in this proof checker I let $\top$ be the same as $\neg \bot$ and $P$ is any formula corresponding to $\psi$ in the question.

enter image description here

A shorter proof also works using negation introduction (¬I) and conditional introduction (⊥I):

enter image description here

Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/

P. D. Magnus, Tim Button with additions by J. Robert Loftis remixed and revised by Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Winter 2018. http://forallx.openlogicproject.org/


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.