forked from OpenLogicProject/forallx-cam
-
Notifications
You must be signed in to change notification settings - Fork 31
/
forallx-yyc-notation.tex
101 lines (70 loc) · 7.74 KB
/
forallx-yyc-notation.tex
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
%!TEX root = forallxyyc.tex
\chapter{Symbolic notation}
\label{app.notation}
\section{Alternative nomenclature}
\paragraph{Truth-functional logic} TFL goes by other names. Sometimes it is called \emph{sentential logic}, because it deals fundamentally with sentences. Sometimes it is called \emph{propositional logic}, on the idea that it deals fundamentally with propositions. We have stuck with \emph{truth-functional logic}, to emphasize the fact that it deals only with assignments of truth and falsity to sentences, and that its connectives are all truth-functional.
\paragraph{First-order logic} FOL goes by other names. Sometimes it is called \emph{predicate logic}, because it allows us to apply predicates to objects. Sometimes it is called \emph{quantified logic}, because it makes use of quantifiers.
\paragraph{Formulas} Some texts call formulas \emph{well-formed formulas}. Since `well-formed formula' is such a long and cumbersome phrase, they then abbreviate this as \emph{wff}. This is both barbarous and unnecessary (such texts do not countenance `ill-formed formulas'). We have stuck with `formula'.
In \cref{s:TFLSentences}, we defined \emph{sentences} of TFL. These are also sometimes called `formulas' (or `well-formed formulas') since in TFL, unlike FOL, there is no distinction between a formula and a sentence.
\paragraph{Valuations} Some texts call valuations \emph{truth-assignments}, or \emph{truth-value assignments}.
\paragraph{$n$-Place predicates} We have chosen to call predicates `one-place', `two-place', `three-place', etc. Other texts respectively call them `monadic', `dyadic', `triadic', etc. Still other texts call them `unary', `binary', `ternary', etc.
\paragraph{Names} In FOL, we have used `$a$', `$b$', `$c$', for names. Some texts call these `constants'. Other texts do not mark any difference between names and variables in the syntax. Those texts focus simply on whether the symbol occurs \emph{bound} or \emph{unbound}.
\paragraph{Domains} Some texts describe a domain as a `domain of discourse', or a `universe of discourse'.
\section{Alternative symbols}
In the history of formal logic, different symbols have been used at different times and by different authors. Often, authors were forced to use notation that their printers could typeset. This appendix presents some common symbols, so that you can recognize them if you encounter them in an article or in another book.
\paragraph{Negation} Two commonly used symbols are the
\emph{hoe},`$\neg$', and the \emph{swung dash} or \emph{tilde},
`${\sim}$.' In some more advanced formal systems it is necessary to
distinguish between two kinds of negation; the distinction is
sometimes represented by using both `$\neg$' and~`${\sim}$'. Older
texts sometimes indicate negation by a line over the formula being
negated, e.g., `$\overline{A \eand B}$', or by a minus sign~`$-$'.
Many texts use `$x \neq y$' to abbreviate `$\enot x = y$'.
\paragraph{Disjunction} The symbol `$\vee$' is typically used to
symbolize inclusive disjunction. One etymology is from the Latin word
`vel', meaning `or'. In some texts in the so-called algebraic
tradition, disjunction is written as addition~`$+$'. In many
programming languages, a vertical bar~`\verb+|+' (or two: `\verb+||+')
are used. (This lends itself to confusion with the Sheffer stroke of
\cref{c:FunctionalCompleteness}, which is standardly written
as~`$\mid$'.)
\paragraph{Conjunction}
Conjunction is often symbolized with the \emph{ampersand}, `{\&}'. The ampersand is a decorative form of the Latin word `et', which means `and'. (Its etymology still lingers in certain fonts, particularly in italic fonts; thus an italic ampersand might appear as `%
\iflatexml
\<span class="ltx\_text" style="font-family:Palatino; font-style:italic;">\&\</span>
\else
\emph{\&}
\fi
'.) This symbol is commonly used in natural English writing (e.g. `Smith \& Sons'), and so even though it is a natural choice, many logicians use a different symbol to avoid confusion between the object and metalanguage: as a symbol in a formal system, the ampersand is not the English word `\&'. The most common choice now is `$\wedge$', which is a counterpart to the symbol used for disjunction. Sometimes a single dot, `{\scriptsize\textbullet}', is used. In some older texts, there is no symbol for conjunction at all; `$A$ and $B$' is simply written `$AB$'.
\paragraph{Material conditional} There are two common symbols for the material conditional: the \emph{arrow}, `$\rightarrow$', and the \emph{horseshoe}, `$\supset$'.
\paragraph{Material biconditional} The \emph{double-headed arrow}, `$\leftrightarrow$', is used in systems that use the arrow to represent the material conditional. Systems that use the horseshoe for the conditional typically use the \emph{triple bar}, `$\equiv$', for the biconditional.
\paragraph{Quantifiers} The universal quantifier is typically
symbolized as a rotated `A', and the existential quantifier as a
rotated, `E'. In some texts, there is no separate symbol for the
universal quantifier. Instead, the variable is just written in
parentheses in front of the formula that it binds. For example, they
might write `$(x)\atom{P}{x}$' where we would write `$\forall x\,
\atom{P}{x}$'. Some texts also use large versions of our conjunction
and disjunction connectives, i.e., `$\bigwedge$' and `$\bigvee$', for
the universal and existential quantifier, respectively. (The variable
is sometimes set as a subscript to these symbols, or even underneath
them.)
\bigskip
These alternative typographies are summarised below:
\begin{center}
\begin{tabular}{rl}
negation & $\neg$, ${\sim}$, $-$, $\overline{A}$\\
conjunction & $\wedge$, $\&$, {\scriptsize\textbullet}\\
disjunction & $\vee$, $+$, \verb+|+, \verb+||+\\
conditional & $\rightarrow$, $\supset$\\
biconditional & $\leftrightarrow$, $\equiv$\\
universal quantifier & $\forall x$, $(x)$, $\bigwedge_x$\\
existential quantifier &$\exists x$, $\bigvee_x$
\end{tabular}
\end{center}
\section{Polish notation}
This section briefly discusses sentential logic in Polish notation, a system of notation introduced in the late 1920s by the Polish logician Jan {\L}ukasiewicz.
Lower case letters are used as sentence letters. The capital letter $N$ is used for negation. $A$ is used for disjunction, $K$ for conjunction, $C$ for the conditional, $E$ for the biconditional. (`$A$' is for alternation, another name for logical disjunction. `$E$' is for equivalence.)
In Polish notation, a binary connective is written \emph{before} the two sentences that it connects. For example, the sentence $A\eand B$ of TFL would be written $Kab$ in Polish notation.
The sentences $\enot A\eif B$ and $\enot (A\eif B)$ are very different; the main logical operator of the first is the conditional, but the main connective of the second is negation. In TFL, we show this by putting parentheses around the conditional in the second sentence. In Polish notation, parentheses are never required. The left-most connective is always the main connective. The first sentence would simply be written $CNab$ and the second $NCab$.
This feature of Polish notation means that it is possible to evaluate sentences simply by working through the symbols from right to left. If you were constructing a truth table for $NKab$, for example, you would first consider the truth-values assigned to $b$ and $a$, then consider their conjunction, and then negate the result. The general rule for what to evaluate next in TFL is not nearly so simple. In TFL, the truth table for $\enot(A\eand B)$ requires looking at $A$ and $B$, then looking in the middle of the sentence at the conjunction, and then at the beginning of the sentence at the negation. Because the order of operations can be specified more mechanically in Polish notation, variants of Polish notation are used as the internal structure for many computer programming languages.