Symbol Charts and Taxonomy of Vocabulary
(with remarks upon the selection of primitives and on definition)

This discussion follows Kalish and Montague, [1], in part. We distinguish two kinds of meaningful expressions of a formal object language: terms and formulas. Terms and formulas are composed of the following symbols.

Classes of symbols (variables and constants):

Meta-linguistic symbols: For meta-linguistic notation we use Quine's corner notation, e.g. éFù , where the logical constants are used autonymously and Greek characters are metalinguistic variables, with typing as shown in the chart below. We use ':-' for syntactic implication, and ':=' for semantic implication. We use '\' for 'Therefore' when discussing English arguments, and 'À' (with subscripts) to indicate the infinite cardinality of a set.

Abbreviations: We use this notation for the signature of a symbol

<Type(logical constant/non-logical constant/variable), Arity(Number), Usage(prefix/infix/suffix/bracketing), Makes(term/formula), VariablesBound(Number), TermsTaken(Number), FormulasTaken(Number)>

to encode the following information pertaining to syntactic characteristics of logical and non-logical symbols.

Type of symbol:

Arity of symbol

Usage of symbol:

Constants:

Definition

Meta-Language Variables

Operation variables
I - W,   upper-case Greek alphabet, with integer subscripts and possibly superscripts
Predicate variables
A - Q, upper-case Greek alphabet, with integer subscripts and possibly superscripts
Individual variables
  a - w, lower-case Greek alphabet, with integer subscripts

 

Object Language Variables

Operation variables
a word beginning with '%', where % has integer subscripts and possibly superscripts
Predicate variables
a word beginning with '@', where @ has integer subscripts and possibly superscripts
Individual variables
    a word beginning with '?'

 

Logical Constants and VBOs

Symbol
Name/Interpretation
Type
Number of variables bound
Number of terms taken
Number of formulas taken
Usage
Ù
and
formula-maker
0
0
2 +
prefix, infix
Ú
or
formula-maker
0
0
2 +
prefix, infix
Þ
if ..., then ...
formula-maker
0
0
2
prefix, infix
Û
if and only if
formula-maker
0
0
2
prefix, infix
 Ø
not
formula-maker
0
0
1
prefix
"
for all
VBO/formula maker
1 +
0
1
prefix
$
there exists
VBO/formula maker
1 +
0
1
prefix
=
identical to
formula-maker
2
2
0
prefix, infix
¹
not identical to
formula-maker
2
2
0
infix
i
iota (description operator)
term-maker
1
0
1
prefix
l
lambda (function abstractor)
term-maker
1
0
1
prefix
k
kappa (set abstractor)
term-maker
1
0
1
prefix
T
true
term
0
0
0
predicate term constant
^
false
term
0
0
0
predicate term constant

 

Object language symbols: Non-logical constants and VBOs

Set-theoretic Symbols

Symbol
Name/Interpretation
Usage
Type
k
set abstractor/kappa
prefix
unary operator/term-maker
l
function abstractor/lambda
prefix
unary operator/term-maker
Î
member of
infix
binary relation
Ï
not a member of
infix
binary relation
 Í
subset
infix
binary relation
Ì
proper subset
infix
binary relation
È
union
infix for the binary operation/prefix for the generalized operation
binary or generalized (3+) operator
Ç
intersection
infix for the binary operation/prefix for the generalized operation
binary or generalized operator (3+)
P
generalized set product
prefix
generalized (3+) operator
*
binary set product
infix
binary operator
Æ
empty set
term
0-place operator/term

 

Arithmetical Symbols

Symbol
Name/Interpretation
Usage
Type
N(X)
natural number
prefix
unary predicate < >
Int(X)
integer
prefix
unary predicate <
Suc(X)
successor
prefix
unary operator <0,0,1,0>
0
zero
term
0-place operator <0,0,0,0>
X + Y
addition
infix
binary operator <0,0,2,0>
X - Y
subtraction/minus
prefix/infix
unary/binary operator <0,0,1,0> or <0,0,2,0>
X ´ Y
multiplication
infix
binary operator <0,0,2,0>
X¸ Y
division
infix
binary operator <0,0,2,0>
Xpow(Y)
exponentiation
infix
unary operator <0,0,1,0>
X ³ Y
greater than or equal
infix
binary relation <0,0,2,0>
X £ Y
less than or equal
infix
binary relation <0,0,2,0>
X > Y
less than
infix
binary relation <0,0,2,0>
X < Y
greater than
infix
binary relation <0,0,2,0>
| X |
absolute value
bracketing
unary operator <0,0,1,0>

 

Symbols of Differential and Integral Calculus

Symbol
Name/Interpretation
Usage
Type
«n
convergence of sequence A to sequence B as n approaches ¥
infix
VBO <1,1,2,0>
Limn
limit of a sequence A as n approaches ¥
prefix
VBO <0,1,1,0>
Limn®l
limit of a sequence A as n approaches L
prefix
VBO <0,1,2,0>
AvX
average velocity
prefix
VBO <0,1,3,0>
DerX
derivative of a sequence
prefix
VBO <0,1,2,0>
ContX
continuity of a sequence at X
prefix
VBO <1,1,2,0>
infX
term denoting the infimum of a set of reals
prefix
VBO <0,1,0,1>
supX
term denoting the supremum of a set of reals
prefix
VBO <0,1,0,1>
åi,n
finite sum from i to n-1
prefix
VBO <0,1,2,0>
ò dx
definite (Riemann) integral
bracketing
VBO <0,1,3,0>

à Possibility

↵ Necessity

References:

[1] Kalish, D., Montague, R., and Mar, G.
Logic: Techniques of Formal Reasoning (2nd Edition)
Harcourt, Brace & Johanovich, Inc.
New York, 1980