I have some doubts about the "natural" interpretation of $\bot$ in Natural Deduction and sequent calculus.

In Prawitz (1965) $\bot$ (falsehood or absurdity) is called a sentential constant [page 14]

Chiswell & Hodges (2007) list $\bot$ (absurdity) between the truth function symbols [page 32], and this is not very clear for me; then, in the formal definition of formula of a language [page 33] they say :

$\bot$ is a formula.

Negri & von Plato (2001) [page 2] list $\bot$ (falsity) between the prime formulas, specifying that :

Often $\bot$ is counted among the atomic formulas, but this will not work in proof theory. It is best viewed as a zero-place connective.

I think that the last comment is contra D.van Dalen, Logic and Structure (5th ed, 2013) [page 7] where $\bot$ is defined as a connective and :

The proposition symbols and $\bot$ stand for the indecomposable propositions, which we call atoms, or atomic propositions.

I'm wondering if all the above definitions are equivalent.

A (propositional) connective is an "operator" that maps one or more propositional variables into a formula; e.g.

$\land$ : <$P,Q$> $\quad \rightarrow \quad P \land Q$.

This means that the zero-place connective $\bot$ is a mapping

$\bot$ : $\emptyset \quad \rightarrow \quad \bot$.

If so, may we say that, being at the same time the mapping and the output of the mapping, it is both a connective and a formula ?

  • $\begingroup$ Thanks for asking @Mauro ALLEGRANZA, I had a similar question. The Laws of Truth by Nicholas Smith (page 129) also regards ⊤ and ⊥ as dual-purposed in that they are connectives but are also wffs, since they can be used as arguments to other connectives. But if verum and falsum can be wffs, then according to clause (2) of the syntax given on page 41, wouldn't they be basic propositions, with verum representing the proposition that is always true and falsum representing the proposition that is always false? $\endgroup$
    – user51462
    Commented Oct 23, 2023 at 9:24
  • $\begingroup$ Here is a link to the zero-place connectives explanation. $\endgroup$
    – user51462
    Commented Oct 23, 2023 at 9:26
  • $\begingroup$ And here is the syntax of PL as defined in the book. $\endgroup$
    – user51462
    Commented Oct 23, 2023 at 9:26
  • $\begingroup$ @user51462 - yes, if you define the language from the start with $\top$ and $\bot$, you need only one "traditional" connective: $\to$, because $\lnot A := A \to \bot$. and thus you have to modify syntax specification page 41: (ii) $\to, \top, \bot$ and 2 (ii) $\top, \bot, \alpha \to \beta$ are wffs, or something similar... $\endgroup$ Commented Oct 23, 2023 at 10:04
  • $\begingroup$ See van Dalen, page 7: "Def 1.1.1 The language of propositional logic has an alphabet consisting of (i) proposition symbols : $p_0, p_, \ldots$, (ii) connectives : $∧ , ∨ , → , ¬ , ↔ , ⊥$ , (iii) auxiliary symbols : ( , ). The proposition symbols and $⊥$ stand for the indecomposable propositions, which we call atoms, or atomic propositions. Def.1.1.2 The set PROP of propositions is the smallest set $X$ with the properties (i) $p_i ∈ X$, $⊥∈ X$, (ii) if $ϕ, ψ ∈ X$ then $ϕ \to ψ ∈ X$, ..." $\endgroup$ Commented Oct 23, 2023 at 11:22

4 Answers 4


You are mixing up different aspects of logic, also some parts of your question are more philosophical than mathematical.

First headline: $\bot$ and $\top$ are wellformed formulas.

(On purpose I mention them both here because in this aspect they are the same)

Different authors have different formulations of this fact:

  • $\bot$ and $\top$ are propositional constants
  • $\bot$ and $\top$ are a zero-place connectives
  • $\bot$ and $\top$ are atomic formula

They all point to the same thing $\bot$ and $\top$ can be part of a formula, it can be used like a normal propositional variable in all rules of the logic. so if $ ( P \to (Q \to R )) \to ( (P \to Q )\to (P \to R )) $ is a theorem then so are $ ( \top \to (Q \to \bot )) \to ( (\top \to Q )\to (\top \to \bot )) $ and $ ( \bot \to (\bot \to R )) \to ( (\bot \to \bot )\to (\bot \to R )) $ and many more, they are not very helpful but that is beside the point)

This is all about being wellformed and how you can use them in formulas , it has nothing about what $\bot$ means.

Some logics just don't define $\bot$ or $\top$ as a wellformed formula, so in those logics they just do not exist.

What does $\bot$ mean?

This is a philosophical question.

If you see logic just as symbol manipulation (the philosophy of mathematics known as formalism) , no symbol means anything and so questioning what a particular symbol means is meaningless.

The above is I guess not very helpful, so different logicians come up with different ideas.

  • $\bot$ means absurd: $ P \to \bot$ means that P leads to absurdity ( and we don't want that)

  • $\bot$ means refutability: $ P \to \bot$ means that P is refutable ( and so P is false)

  • $\bot$ means non-demonstrability $ P \to \bot$ means that P is not demonstable (so not provably true)

The above is a rewriting from "Foundations of Mathematical logic" Curry (1963), chapter 6 "negation" , the chapter goes much deeper in it, there is a dover edition of it, highly recomended, but negation is much more complex than it looks, in another article I saw, I think 7 different negations appeared, and i do doubt that article mentioned them all.

Wittgenstein came up with " meaning follows from use " so maybe the only way you can find the meaning is to look at how it is used.

  • If $ \bot \to P $ is a theorem then $\bot$ means absurdity, it is quite absurd that every formula is true.

  • If $ ((P \lor R) \to ((P \to\bot) \to R) $ is a theorem then $\bot$ means refutability, P is refuted (and therefore R is true)

  • If $ (P \lor (P \to\bot) ) $ you have classical logic.

so it all depends, but can you expect anything else with a philosophical question.

  • 3
    $\begingroup$ Frankly I did not understand philosophy of negation. Until I read what you wrote everything was clear and simple. Now it is not. $\endgroup$ Commented Jan 31, 2014 at 10:30
  • $\begingroup$ Ok thanks - regarding the first part (that answer to my question) that is relevant to my previous post on [Consistency in Natural Deduction](math.stackexchange.com/questions/655776/… ), being $\bot$ a formula, we can say that, in absence of $\lnot$ , we must apply Post's definition of consistency, so that, proving the underivability of $\bot$ is equivalent to proving that not every proposition is derivable, and this must suffice to prove consistency. $\endgroup$ Commented Jan 31, 2014 at 10:52
  • $\begingroup$ @Trismegistos - I'm not asking for "philosophy of negation" (I will read Curry, in order to try to understand what it is about). I'm asking about way of proving consistency of systems of Natural Deduction without $\lnot$ as primitive. $\endgroup$ Commented Jan 31, 2014 at 11:27
  • 1
    $\begingroup$ @Trismegistos sorry but you were mistaken before, when you start with logic all is clear and simple, but when you really start thinking about it it get a philosophical quicksand. This question is not for beginning students $\endgroup$
    – Willemien
    Commented Jan 31, 2014 at 12:45

There is one simple "universal" answer to this question which depends neither on proof theory nor on semantics.

Think of the set of formulas of logic as a term algebra freely generated over a syntactic signature that describes its collection of connectives (or think of the set of formulas, for all that matters, as a context-free grammar). Assume there are denumerably many variables (or propositional parameters) in the underlying language. An abstract consequence relation is then defined over such propositional language, as usual, so as to recover the properties of a closure operator. A logic system is then given by a language $L$ and a substitution-invariant consequence relation $\vdash\;\subseteq 2^L\times L$. By 'substitution-invariant' we mean that $\Gamma\vdash A$ implies $\sigma[\Gamma]\vdash\sigma[A]$, where $\sigma$ denotes a substitution mapping in $L$ (i.e., a homomorphic mapping from variables to formulas).

Now, in the above construction $\bot$ (or $\top$) may be either a propositional parameter or a nullary connective. In the former scenario, substitution would apply to such symbol; in the latter, it wouldn't. However, in practice, $\bot\vdash p$ is usually assumed to hold for every variable $p$, but $q\vdash p$ in general fails for every variable $q$ distinct from $p$. Consequence would thus not be preserved under substitution, if one insisted that $\bot$ is a propositional parameter. The simplest way out is to assume it to be a nullary connective.

  • $\begingroup$ Thanks - may I "interpret" your answer also in this way : in Natural Deduction, if $\bot$ is a propositional parameter, I may use it e.g. in $\lor$-intro to pass from $A$ to $A \lor \bot$. If $\bot$ is instead a connective, I cannot. Is it right ? $\endgroup$ Commented Feb 9, 2014 at 21:42
  • $\begingroup$ @MauroALLEGRANZA No, in both cases you could use it: rule $\lor$-intro allows for any formula to be introduced, be it a propositional parameter, or a nullary connective, or a complex well-formed formula with many propositional parameters and connectives of all kinds. The point in this case is that the natural deduction rule is formulated with schematic letters, and such strategy automatically embeds substitution into the formalism. $\endgroup$
    – J Marcos
    Commented Feb 9, 2014 at 21:53

Regarding comment of Trismegistos about $\lnot$ I- and E-rules, we have ...

Dag Prawitz, Natural Deduction (1965) (page 20) defines the minimal system $\text M$ with the (now) usual five couples of I- and E-rules for $\lor, \land, \rightarrow, \forall$, and $\exists$.

The system for intuitionistic logic is defined as $\text M \cup \{ \bot_I \}$ where $\bot_I$ is :

(ex falso quodlibet) $$\frac {\bot} A$$

This rule is $\bot$-E; we do not have a $\bot$-I [we may expect this, in order to have soundness].

The system for classical logic is defined as $\text M \cup \{ \bot_C \}$ where $\bot_C$ is :

(RAA) $$\frac {\frac {[\lnot A]} \bot } A$$

The $\lnot$ symbol is an abbreviation [page 21], i.e. $\lnot A$ is $(A \rightarrow \bot)$.

With this abbreviation, we have that the two Gentzen’s rules for $\lnot$ are derived rules.

$\lnot$-I : $$\frac {\frac {[A]} \bot} {\lnot A}$$ is obtained from $\rightarrow$-I and

$\lnot$-E : $$\frac {A \quad \lnot A} \bot$$ from $\rightarrow$-E.

Instead of adding $\bot_C$, classical logic can be obtained adding :

(DN) $$\frac {\lnot \lnot A } A$$

in this way, $\bot_I$ becomes redundant [page 21].

Prawitz [page 35] consider also another possibility: in order to get classical logic, we can omit $\bot$ and introduce $\lnot$ as primitive, with the two rules :

$\lnot$-I : $$\frac { \frac {[A]} B \quad \frac {[A]} {\lnot B} } {\lnot A}$$


$\lnot$-E : $$\frac {\lnot \lnot A } A$$.

But he express unsatisfaction for this couples of rules, because they do not show the “symmetric” form of “standard” I- and E-rules [in $\lnot$-I the connective is already present in the premises].

Neil Tennant, Natural logic (1978) proceed as Prawitz, with the intuitionistic logic obtained adding to the “basic” system the rule :

(Absurdity) $$\frac {\bot } A$$

Then he consider four rules :

(EM) $$ \frac { } {A \lor \lnot A}$$

(Dilemma) $$\frac { \frac { [A] } B \frac { [\lnot A] } B } B$$

(RAA) $$\frac {\frac {[\lnot A]} \bot } A$$

(DN) $$\frac {\lnot \lnot A } A$$

Tennant proves that all four are inter-derivable.

Classical logic is obtained from the “basic” system with the addition of one of the four above rules (using the Absurdity rule).

Note : also very useful : Neil Tennant, Negation Absurdity and Contrariety (2004).

We can note that with Dilemma and RAA we have a couple of "symmetric" I- and E-rules for $\lnot$.

Ian Chiswell & Wilfrid Hodges, Mathematical Logic (2007), use (for classical logic) the three rules :

($\lnot$-E) $$\frac { A \quad \lnot A } \bot$$

($\lnot$-I) $$\frac { \frac { [A] } \bot } { \lnot A }$$

(RAA) $$\frac { \frac { [\lnot A] } \bot } A.$$

Also in this case we have a couple of "symmetric" I- and E-rules for $\lnot$.

  • $\begingroup$ "Classical logic is obtained from the “basic” system with the addition of one of the four above rules (and omitting Absurdity)." This didn't make sense to me, if you start with the basic system and add LEM without absurdity, you can't reach classical logic no? $\endgroup$
    – user525966
    Commented Jul 11, 2019 at 12:49
  • 1
    $\begingroup$ I understand that DN is strong enough to get absurdity, what I don't understand is that sentence mentioning that basic/minimal logic plus any of the four rules leads to classic logic, since I don't believe LEM (the first of the four) is strong enough for that $\endgroup$
    – user525966
    Commented Jul 11, 2019 at 13:26
  • $\begingroup$ @user525966 - correct; I'll fix it. $\endgroup$ Commented Jul 11, 2019 at 13:47

Here's the big divide over the use and meaning of an absurdity symbol in natural deduction systems: which of the following ways of treating the symbol should we take?

(i) $\bot$ can be assigned a truth-value and can appear embedded like a subformula in more complex formulas, or

(ii) $\bot$ merely serves to "close off" a line of reasoning when it contains contradictory wffs, so using it is like saying "Stop! Trouble!! Aaaarghhhh!!!!!"

Approach (i) is explored a bit in @Willemien's answer. And, concerning the fine print details within approach (i), it surely doesn't matter too much whether you officially call $\bot$ a zero place connective, or a propositional atomic formula (or rather, which way you go will depend on the further fine print of what you say elsewhere about connectives and atomic formulae).

Of those who have argued that we should best treat an absurdity marker using approach (ii), I think the most persuasive is Neil Tennant: see e.g. his paper http://people.cohums.ohio-state.edu/tennant9/nac.pdf for further details.

  • $\begingroup$ Thanks, I'll read it. Your (i) is exactly about what I'm trying to understand. In connection with my post on Consistency in Natural Deduction, from one side, being $\bot$ a formula, we can use it for Post-consistency. At the same time, being a formula, my feeling (but I've not yet sure about it) is that there are no rules in ND that introduce it. The only way it can "crops in" is trough $\lor_I$, (but see your (i)) and I think that $A \lor \bot$ does not count as a contradiction... $\endgroup$ Commented Jan 31, 2014 at 11:03
  • $\begingroup$ @MauroALLEGRANZA There is negation introduction in ND and unsurprisingly it introduces negation :D $\endgroup$ Commented Jan 31, 2014 at 12:30
  • $\begingroup$ @Trismegistos - as I said in my previous post about Consistency in ND, I'm reflecting on Prawitz (1965) system, wehere $\lnot A$ is an abbreviation for $(A \rightarrow \bot)$; so, we can dispense with negation. If I'm working with the intuistionistic portion of the system, the rule $\bot_I$, strictly speaknig, does not introduce $\bot$, but eliminate it. 1/2 $\endgroup$ Commented Jan 31, 2014 at 12:48
  • $\begingroup$ If we work in classical logic, we have also $RAA$, but see van Dalen, Logic and Structure, page 30 : "We have two rules for $\bot$, both of which eliminate $\bot$, but introduce a formula." 2/2 $\endgroup$ Commented Jan 31, 2014 at 12:48
  • $\begingroup$ @Peter Smith - van Dalen [2013] defines $\bot$ as a connective and also as an atomic proposition (pag.7). He says also (page 20) : "Let us make one more remark about the role of the two $0$-ary connectives, $\bot$ and $\top$". $\endgroup$ Commented Jan 31, 2014 at 12:52

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .