Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

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 ?

share|improve this question

4 Answers 4

up vote 3 down vote accepted

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.

share|improve this answer
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 ? –  Mauro ALLEGRANZA Feb 9 at 21:42
@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. –  J Marcos Feb 9 at 21:53

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.

share|improve this answer
Frankly I did not understand philosophy of negation. Until I read what you wrote everything was clear and simple. Now it is not. –  Trismegistos Jan 31 at 10:30
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. –  Mauro ALLEGRANZA Jan 31 at 10:52
@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. –  Mauro ALLEGRANZA Jan 31 at 11:27
@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 –  Willemien Jan 31 at 12:45

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.

share|improve this answer
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... –  Mauro ALLEGRANZA Jan 31 at 11:03
@MauroALLEGRANZA There is negation introduction in ND and unsurprisingly it introduces negation :D –  Trismegistos Jan 31 at 12:30
@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 –  Mauro ALLEGRANZA Jan 31 at 12:48
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 –  Mauro ALLEGRANZA Jan 31 at 12:48
@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$". –  Mauro ALLEGRANZA Jan 31 at 12:52

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

Dag Prawitz, Natural Deduction (1965) [page 20] defines the minimal system 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 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 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 (and omitting Absurdity).

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

share|improve this answer

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.