# A question about the deduction theorem

The deduction theorem states that if $T \cup \{ \psi \} \vdash \varphi$ and the generalisation rule is not used to prove $\varphi$ then $T \vdash \psi \rightarrow \varphi$.

If I apply the generalisation rule, where exactly does it go wrong if I apply the deduction theorem thereafter? Can someone provide an example?

-
What does $\top \to x$ even mean, if $x$ is a variable (as opposed to a proposition or a predicate)? –  Zhen Lin Oct 23 '11 at 12:09
It could be an axiom but I wrote it as an example of the kind of example I'm looking for. –  Rudy the Reindeer Oct 23 '11 at 12:15
@Matt: It can't be an axiom, since it's not even a well-formed formula. –  Chris Eagle Oct 23 '11 at 12:25
@ChrisEagle: True! I'll delete it seeing as it's not relevant for my question. –  Rudy the Reindeer Oct 23 '11 at 12:33
Hint: Forget about $T$ (i.e., take $T = \emptyset$), and take $\psi$ as a formula with free variables (i.e., it is not a setence) such that $\varphi$ is the universal closure of $\psi$. –  boumol Oct 23 '11 at 15:20

The important thing to realise is that whatever is on the RHS of $\vdash$ has got to be an axiom (meaning: a universally true formula). On the other hand, on the LHS we can assume whatever we like. So for example if $T = \emptyset$ we can show that $\{ \varphi (x) \} \vdash \forall x \varphi(x)$. What we can't do is to show that $\emptyset \vdash \varphi(x) \to \forall x \varphi (x)$.

To see why we can't let's consider the example $\varphi (x) = (x = 1)$:

If we assume ($x = 1$) then we get the following formal proof of $\{ x = 1 \} \vdash \forall x (x = 1)$:

$(1) x = 1 ( \in T)$

$(2) \forall x (x = 1)$ (generalisation rule applied to ($1$))

On the other hand, if we use the deduction rule on this to get $\vdash (x = 1) \to \forall x (x = 1)$ then we have $\top \to \bot$ if we replace $x$ with $1$ where it's free. But this is false, hence the formula on the RHS is not universally true.

-
i think it is necessary to mention the Domain of your interpretation which can be natural numbers. –  kiyarash Jan 9 at 13:29
also it would be better to explain why $\vdash (x = 1) \to \forall x (x = 1)$ is not satisfied by your interpretation –  kiyarash Jan 9 at 13:30
{"extraction_info": {"found_math": true, "script_math_tex": 0, "script_math_asciimath": 0, "math_annotations": 0, "math_alttext": 0, "mathml": 0, "mathjax_tag": 0, "mathjax_inline_tex": 1, "mathjax_display_tex": 0, "mathjax_asciimath": 0, "img_math": 0, "codecogs_latex": 0, "wp_latex": 0, "mimetex.cgi": 0, "/images/math/codecogs": 0, "mathtex.cgi": 0, "katex": 0, "math-container": 0, "wp-katex-eq": 0, "align": 0, "equation": 0, "x-ck12": 0, "texerror": 0, "math_score": 0.9704135656356812, "perplexity": 276.78603356675853}, "config": {"markdown_headings": true, "markdown_code": true, "boilerplate_config": {"ratio_threshold": 0.18, "absolute_threshold": 10, "end_threshold": 15, "enable": true}, "remove_buttons": true, "remove_image_figures": true, "remove_link_clusters": true, "table_config": {"min_rows": 2, "min_cols": 3, "format": "plain"}, "remove_chinese": true, "remove_edit_buttons": true, "extract_latex": true}, "warc_path": "s3://commoncrawl/crawl-data/CC-MAIN-2015-27/segments/1435375097354.86/warc/CC-MAIN-20150627031817-00061-ip-10-179-60-89.ec2.internal.warc.gz"}