First-order parser
Enter a term or formula and follow the construction of its syntax tree. The tree distinguishes objects named by terms from claims made by formulas.
Scope. The fixed signature below, with variables x, y, z, u, v,
and w, optionally indexed. Quantifiers, identity, and the propositional
connectives are supported. Both inputs use conventional bracket rules.
| Symbols | Names |
|---|---|
| Constants | Socrates, Xanthippe, Greece, LittleJimmy, MrSir, a, b, c |
| Unary functions | fatherOf, motherOf, birthplaceOf, capitalOf, f |
| Binary functions | distanceBetween, g |
| Unary predicates | Human, Mortal, P, Q |
| Binary predicates | BiggerThan, Sibling, R |
Terms
Enable JavaScript to step through the tree. The grammar and worked example remain available in the chapter.
Formulas
Enable JavaScript to step through the tree. The grammar and worked example remain available in the chapter.
Using it
The pencil unlocks the input. Use argument brackets, as in R(x,y) or
fatherOf(x), then choose Start parsing. LaTeX commands convert as you type.
Quantifiers bind tightly: bracket a compound scope, as in ∀x (P(x) → Q(x)).
The arrows step through parsing; the tree controls change its labels and export
PNG or LaTeX. The accessibility button opens the text tree.
In the book
- Chapter 8 · First-order syntax defines terms and formulas.
- Chapter 8 · Scope and open formulas explains variable binding.