What is the correct reading of $\bot$?

Question

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 ?

Answer 1

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.

Answer 2

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.

Answer 3

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.

Answer 4

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

and

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