Formula Checker — Quantificational Logic

VOCABULARY

Constants
a, b, c, d, e (with optional numeric subscripts)

Variables
x, y, z (with optional numeric subscripts)

Predicates
P, Q, R, S, T (with optional numeric subscripts)

Connectives
¬ ∧ ∨ →

Quantifiers
∀ ∃

Identity
τ₁ = τ₂ (terms are constants or variables)

FORMATION RULES

1. If P is an n-place predicate and τ₁,…,τₙ are terms, then Pτ₁…τₙ is a formula.

2. If τ₁ and τ₂ are terms, then τ₁ = τ₂ is a formula.

3. If φ and ψ are formulas, so are:
¬φ, (φ ∧ ψ), (φ ∨ ψ), (φ → ψ)

4. If φ is a formula and x is a variable, then ∀x φ and ∃x φ are formulas.

5. Nothing else is a formula.

The outer parentheses of a formula not part of a larger formula may be dropped as an abbreviation.

EXAMPLES

Expression	Status
Pxy	official formula
x = y	official formula
∀x Pxy	official formula
(∀x Pxy → ∃y Qab)	official formula
∀x Pxy → ∃y Qab	unofficial formula (abbreviates (∀x Pxy → ∃y Qab))
¬(Px → A)	not a formula (A is not a term)

ASCII SHORTCUTS

Type	Symbol
~ -	¬
& /\	∧
\| \/	∨
-> =>	→
A (before variable)	∀
E (before variable)	∃

Formula

Examples:

Parse Tree

Enter a formula above to practice.