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

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!

• 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. – Anna Sep 18 '14 at 8:16
• 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. – Mauro ALLEGRANZA Sep 18 '14 at 8:27
• 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 – Anna Sep 18 '14 at 8:32
• 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 ? – Mauro ALLEGRANZA Sep 18 '14 at 8:41
• 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. – Marcel Besixdouze Feb 21 '15 at 8:40

HINT

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.

Proof

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$.

• 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? – Anna Sep 18 '14 at 8:49
• Are my argument enought to prove $\vdash \top$ ? @MauroALLGRANZA – Anna Sep 18 '14 at 9:15
• thanks :) @MauroALLEGRANZA – Anna Sep 18 '14 at 9:29
• @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$. – Mauro ALLEGRANZA Sep 18 '14 at 9:30
• Do you recommend any good page about these kinds of proofs? – 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.

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

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/