We are working on a question in which we have to prove that a certain set of logical connectives is functionally complete. It is said that we are allowed to use the fact that the set $\{\bot,\to\}$ is functionally complete. Our question is: how is the logical connective $\bot$ used in formulae? Is it possible to write something like $p\bot$? Or does $\bot$ always have to be used with an implication such as in $p\to\bot$.

Thanks in advance,


  • 7
    $\begingroup$ Syntactically it is used in the same way as a propositional letter. $\endgroup$ May 29 at 11:02
  • 1
    $\begingroup$ .... but it always evaluates to False. $\endgroup$ May 29 at 11:03
  • 7
    $\begingroup$ It acts like a propositional symbol. You can use to to define negation: $\lnot p := p \to \bot$. Or you can use it "stand alone" as in the EFQ rule: "from $\bot$, derive $\varphi$". $\endgroup$ May 29 at 11:12
  • $\begingroup$ @ancientmathematician I don't know why you say that. If we have an expression like (p→(q→p)), we can take p and uniformly substitute all 'p' with (a→b). Or we can instantiate ((a→b)→(q→(a→b))) from the schema (p→(q→p)). But, if we have an expression like (⊥→(q→⊥)) we can't do any sort of substitution or use (⊥→(q→⊥)) as a schema where something goes in the place of '⊥'. Variables are not constants, nor are constants variables! Permissible rules of transformation differ between '⊥' and propositional letters, so I don't see how syntactically they are the same. $\endgroup$ May 30 at 15:17
  • 1
    $\begingroup$ @DougSpoonwood I took syntax as being how one constructs formulas in the propositional language, and not the syntax of schema. $\endgroup$ May 30 at 16:53

1 Answer 1


If we use a rigorous definition of formulas (or well-formed formulas or meaningful expressions), symbols like '⊥' or '0' in Polish notation qualify as propositional constants. One possible definition of meaningful expressions goes as follows:

  1. All lower case letters in alphabetical order of the Latin alphabet up to 'y' qualify as meaningful expressions: {'a', 'b', ..., 'v', 'x'} are all meaningful expressions. Note that this definition could get extended by numerical subscripts in principle.
  2. '⊥' is a meaningful expression.
  3. If y and z are meaningful expressions, then so is Cyz.
  4. Nothing else is a meaningful expression.

This definition implies that every meaningful expression is either a lower case letter, '⊥', or starts with 'C'.

'p⊥' is not a lower case letter, nor does it start with 'C', nor is it '⊥'.

Therefore, it is not possible to correctly write 'p⊥' or something like it. But, '⊥' does not have to get used with an implication, since '⊥' is a standalone formula.

Algorithms also have gotten developed to determine whether a string of symbols is or is not a meaningful expression. Previous study of those algorithms also implies the above bold text.


You must log in to answer this question.

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