What is the correct reading of $\bot$?

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 ?


Solution 1:

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.

Solution 2:

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.