I am trying to teach myself some logic by means of "A Friendly Introduction to Mathematical Logic" of Leary and Kristiansen.

It has a focus on formulas in the sense that axioms are not necessarily sentences.

Interference rules practicized in that book are PC (propositional consequence) and the quantifier rule QR stating that from $\psi\to\phi$ we can deduce $\psi\to\forall x\phi$ if $x$ is not free in $\psi$.

Let $\mathcal{L}$ be a first order language, let $\bot$ denote some $\mathcal{L}$-sentence of the form $\psi\wedge\neg\psi$ and let $\phi$ be an $\mathcal{L}$-formula.

Then $\Sigma:=\left\{ \phi\right\} $ is by definition inconsistent if there is a deduction from $\Sigma$ to $\bot$.

Now my question:

If $\left\{ \phi\right\} $ is inconsistent then can it be proved that also: $\vdash\phi\to\bot$?

It is clear to me that the answer is "yes" if $\phi$ is a sentence because then we can apply the deduction theorem.

But what if $\phi$ is not a sentence?

My try:

If $\tilde{\phi}$ denotes a universal closure of $\phi$ then $\left\{ \tilde{\phi}\right\} \vdash\phi$ so that by transitivity of $\vdash$ we have $\left\{ \tilde{\phi}\right\} \vdash\bot$ and appying deduction theorem we have $\vdash\tilde{\phi}\to\bot$.

But this only shifts the problem to another question:

If there is a deduction $\vdash\tilde{\phi}\to\bot$ then is there also a deduction $\vdash\phi\to\bot$?

Thank you in advance and my apologies if this question is a duplicate.

  • $\begingroup$ Intuitively, YES. Leary's system logic is sound and complete and both theorems are stated for formulas (see page 54). Thus, if $\phi \vdash \bot$, then $\phi \vDash \bot$. But this means that there is no interpretation where $\phi$ is True and $\bot$ is False, i.e. $\phi$ must be False for every interpretation. This means that $\phi \to \bot$ is a tautology, and thus, by Completeness: $\vdash \phi \to \bot$ $\endgroup$ Aug 23, 2020 at 16:28
  • $\begingroup$ @MauroALLEGRANZA So you are saying is: $$\left(\phi\vdash\bot\right)\implies\left(\phi\vDash\bot\right)\implies\left(\vDash\phi\to\bot\right)\implies\left(\vdash\phi\to\bot\right)$$right?Thank you. I will have a look at that but hope for a deduction. One in which the quantifier-rule can be missed I guess. Uptil now I did some vain efforts to prove that by induction (let $(\phi_1,\dots,\phi_n)$ be a deduction of $\bot$ from $\phi$ and then showing that we have $\phi\to\phi_i$ for every $i$). My interest is in the set of formulas preordered by $\leq$ where $\phi\leq\psi\iff\vdash\phi\to\psi$. $\endgroup$
    – drhab
    Aug 23, 2020 at 16:53
  • $\begingroup$ The details of the meta-proof depend on the detail of the proof system and its semantics as well... In Enderton's system, where we have only MP inference rule (and no Gen rule) the Ded Th holds for formulas. The key-point is that $\phi$ is valid iff $\forall x \phi$ is valid. $\endgroup$ Aug 24, 2020 at 8:18
  • $\begingroup$ See also Leary, Lemma 2.7.2 and 2.7.3 and note page 64: "Notice that one consequence of this lemma is the fact that if we know $\Sigma \vdash \theta$, we can assume (if we like) that every element of $\Sigma$ is a sentence: By quoting Lemma 2.7.3 several times, we can replace each $\sigma \in \Sigma$ with its universal closure." $\endgroup$ Aug 24, 2020 at 8:26
  • $\begingroup$ @MauroALLEGRANZA Inspired by your first comment I had a look at the semantic version. Unfortunately I did not succeed to arrive at the same conclusion as you. In this new question I make clear why not and also ask for help. $\endgroup$
    – drhab
    Aug 24, 2020 at 17:07

1 Answer 1


I didn't read Leary and Kristiansen book but I'm currently reading "Introduction to mathematical logic" from Mendelson so i hope i can answer your first question.

As for your first question that states "if a formula ϕ (being ϕ : ψ ∧ ¬ ψ ) proves a contradiction ⊥ then do we have ⊢ ϕ → ⊥ ?" I can answer: effectively a formula that states ψ ∧ ¬ ψ is going to make us conclude ⊥ , this ( ψ ∧ ¬ ψ ) → ⊥ formula is a theorem, here's a proof of the formula using natural deduction rules:

1) ψ ∧ ¬ ψ - assumtion

2) ψ - rule E∧ in 1

3)¬ ψ - rule E∧ in 1

4) ⊥ - in 2,3

5)( ψ ∧ ¬ ψ ) → ⊥ - rule I→ in 1,4

If we look at the truth table of ψ ∧ ¬ ψ all values are false, this means that, not only ( ψ ∧ ¬ ψ ) → ⊥ is a tautology, but also ( ψ ∧ ¬ ψ ) → X (where X is an arbitrary formula) is a tautology. If a formula proves a contradiction u have probe all the formulas.

As for your second question I'm not confident enought to give an answer, im currently reading chapter two of Mendelson's book (first-order logic) so I share your doubt.

  • $\begingroup$ Thank you for your effort to help me. I am aware that $(\psi\wedge\neg\psi)\to\alpha$ is true for every $\alpha$ (so also for $\bot$) but that is not the essence of my problem. You speak of "first question" and "second question" but actually I only meant to pose one question. The essence of it is: if we can deduce $\bot$ on base of hypothese $\phi$ then can we deduce $\phi\to\bot$ without using any hypotheses? I already know that the answer is "yes" if $\phi$ is a sentence. Also it seems that in your answer $\phi$ is identified with $\psi\wedge\neg\psi$ but that is not what I meant. $\endgroup$
    – drhab
    Aug 21, 2020 at 6:46
  • $\begingroup$ First, i should have asked what u mean by "sentence" (since i didn't read that book and english is not my first languege, I may be missing something) (and also i can't add a comment since I'm not 50 raputation yet). Can u give me an example of a sentence? $\endgroup$ Aug 21, 2020 at 16:01
  • $\begingroup$ In predicate logic a sentence is a formula that has no free variables. For instance $\forall x[x=x]$ is a sentence. Formula $x=x$ is not a sentence because variable $x$ is free in that formula. $\endgroup$
    – drhab
    Aug 21, 2020 at 18:27
  • $\begingroup$ Thank you drhab for the example, now I understand beter your question and realise I did not understand your question correctly in first place. I don't think I'm able to give a proper answer yet, but I will have in mind your question as I read Mendelson. If I find an answer I will come back. $\endgroup$ Aug 22, 2020 at 15:57
  • 1
    $\begingroup$ Okay Mauro. Again thanks for your try. If I receive no answers then I consider to put a bounty on this question (unless I find it myself). If that does not work then I will pose the same question on math.overflow to see what real professionals have to say. If no one comes up with an answer then I will not only be disappointed but will celebrate it as a victory as well. It is a merit to come up with a well posed question that no one can answer. Cheers and good luck with your study of logics. $\endgroup$
    – drhab
    Aug 22, 2020 at 16:59

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.