# How is the logical connective $\bot$ used in formulae

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

Hugo

• Syntactically it is used in the same way as a propositional letter. May 29 at 11:02
• .... but it always evaluates to False. May 29 at 11:03
• 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$". May 29 at 11:12
• @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. May 30 at 15:17
• @DougSpoonwood I took syntax as being how one constructs formulas in the propositional language, and not the syntax of schema. May 30 at 16:53

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.