/ 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

    <variable><operator><expression>

instead of

    <operator><variable><expression>.

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