/ Rationalized Notation for First-Order Logic
/ parse: E:E;e|e e:nve|te| t:n|v n:t[E]|(E)|N
p:{I::0;{:[l[x]&2=#x;x 1;x]}{:[l x;(,,","),1_ x;x]}t J::"(",x:n x _dv" "} / parse
n:{{:[1=#x;*x;x]}'(&b|1,(<':b:~x _lin"0123456789"))_ x} / numbers
c:{:[~4:x;"n";&/x _lin o;"v";"osn"(&/'x _lin/:(,"[";",)] "))?1]} / class of token
o:"~|&/{}!=",_ci 65+!26 / operators + predicates
j:{i -1+I+:1} / next token
i:{:[x<#J;J x;" "]} / safe indexing
k:{:[c[x]_in"nv";,x;x]} / f(
g:{x(1;)(~3>#x)|"v"=c x 1} / (v) -> (v)
l:{("("~*x)&~x~"()"} / ( but not ()
E:{|/",(["=*j`}{e t`}\ / (expression)
t:{:["s"=c i I;"";{"o"=c i I}{:["["=*i I;E x;(j`;x)]}/ :[~l i I;j`;g E i I]]} / term ("" = ::)
e:{:["s"=c i I;x;v[f:t`]>v`;(f;x;e t`);(x,":";e f)]} / expression
v:{c[i I-1]_in"vo"} / verb or (?
/ unparse
u:{:[1=#x;x;~(**x)_in o;m x;2=#x;(**x),u x 1;b[u x 1],x[0],u x 2]} / unparse
m:{:[@x;x;x[0],a s@u'1_ x]} / atom or f[
a:1!"][", / x -> [x]
b:{:[("("=*x)|@x;x;1!")(",x]} / parenthesize
s:1_,/",",' / separate
\
the grammar is simple. there are two syntax categories: nouns and verbs. nouns are variables (single lower-case letters)and positive whole numbers (sequences of numerals). verbs fall into four subcategories: predicates (single upper-case letters), the symbol @ for the contant falsum, and monadic and dyadic operators. dyads are further divided into overlapping semantic categories: logical connectives and variable binding operators.
predicates have finite valence: 0 (propositional letters), 1 (properties), 2 (binary relations), and so on.
it is convenient to treat predicate letters as verbs:
F[x,y] -> Fxy
xFy -> Fxy
xFG[y,z] -> ("F";"x";"Gyz")
two special predicates are { (membership) and = (identity).
x{y
the symbol for class-abstraction is chosen for its affinity to membership:
x}Fx
e.g.
F[a]~a{x}Fx
i.e. a is F iff a is a member of the class of F-ers.
nouns symbol
----- ------
variables a-z
numbers 0-9*
verbs symbol meaning
----- ------ -------
predicates A-Z { = predicates, membership, identity.
monads ~ | & negation, possibility, necessitation
connectives | & / ~ disjunction, conjunction, implication, equivalence
binding | & ! } universal, particular, definite, abstraction
iverson notation is used - there is no precedence. a monad is written to the left of its argument. a dyad is written between its arguments. note that ~ is ambivalent: ~x is negation, x~y is equivalence. dyadic & and | are conjunction and disjunction, monadic & and | are necessitation and possibility.
expressions are evaluated left-of-right:
a|b&c/d is a|(b&c/d)
(a|b)&~c/d is (a|b)&(~(c/d))
(a|b)&(~c)/d is (a|b)&((~c)/d)
variable-binding operators (all, some, the, class) are written
instead of
.
example:
if all the world loves a lover then if one loves one then all loves all:
(x&(y|xLy)/y|yLx)/(x|y|xLy)/x&y&xLy
parse/unparse:
q:"(x&(y|xLy)/y|yLx)/(x|y|xLy)/x&y&xLy"
p q
("/"
("&"
"x"
("/"
("|";"y";"Lxy")
("|";"y";"Lyx")))
("/"
("|"
"x"
("|";"y";"Lxy"))
("&"
"x"
("&";"y";"Lxy"))))
q~u p q
1