We originally defined a well-formed formula (WFF) for propositional logic; we'll extend this to WFFs for first-order logic, also known as predicate logic. At the same time, we'll more precisely define the binding of variables.
This logic allows use of both functions and relations. Since these functions' outputs are not Booleans (otherwise, we'd call them relations), but rather data than can be used as a relation's input, we separate the syntax into that of terms and formulas. Terms are all the possible inputs for a relation.
Definition 4.1: term
- A variable.
Example
a, b, ...
- A constant.
Example
WaterWorld location F , Kevin Bacon, or the number 3.
- A function applied to one or more terms.
Example
successor (3)
Definition 4.2: Well-Formed Formula (WFF) for first-order logic
- A constant: true or false.
- An atomic formula: a relation symbol applied to one or more terms.
Example
nhbr (x, F
)
- A negation of a WFF, ¬φ.
- A conjunction of WFFs, φ ∧ ψ.
- Adisjunction of WFFs, φ ∨ ψ.
- An implication of WFFs, φ ⇒ ψ.
- A universal quantification of a WFF, ∀x :(φ).
Example
∀x : (nhbr (x, F ))
- An existential quantification of a WFF, ∃x :(φ).
Example
∃x : (nhbr (x, F ))
While a formula is just a piece of syntax, the meaning of its connectives, including the quantifiers, is part of the definition of a WFF. However, as previously discussed, the meaning of a WFF also depends on the interpretation (Interpretations) we give to its relations.
- 瀏覽次數：3837
