First-order logic provides a powerful framework for expressing complex statements about objects and their relationships. It builds on propositional logic by introducing quantifiers and predicates, allowing for more nuanced and expressive logical formulations.
The syntax of first-order logic consists of symbols, terms, and formulas. These elements combine to create well-formed formulas that can represent intricate logical statements, laying the groundwork for formal reasoning and proof construction in mathematical and philosophical contexts.
Vocabulary
Symbols and Constants
Top images from around the web for Symbols and Constants Logic for Computer Scientists/Predicate Logic/Syntax - Wikibooks, open books for an open world View original
Is this image relevant?
Logic for Computer Scientists/Predicate Logic/Syntax - Wikibooks, open books for an open world View original
Is this image relevant?
1 of 3
Top images from around the web for Symbols and Constants Logic for Computer Scientists/Predicate Logic/Syntax - Wikibooks, open books for an open world View original
Is this image relevant?
Logic for Computer Scientists/Predicate Logic/Syntax - Wikibooks, open books for an open world View original
Is this image relevant?
1 of 3
Predicate symbols represent relations between objects (Loves, IsGreaterThan)
Function symbols denote functions that map objects to other objects (MotherOf, Successor)
Constants refer to specific objects in the domain of discourse (Alice, Bob, 0, 1)
Variables are used to represent arbitrary objects (x, y, z)
Building Blocks of First-Order Logic
Terms are expressions that refer to objects
Can be constants (a, b, c), variables (x, y, z), or function applications (f(x), g(a, y))
Function applications consist of a function symbol followed by a tuple of terms (MotherOf(Alice), Successor(0))
Atomic formulas are the simplest type of well-formed formulas in first-order logic
Formed by applying a predicate symbol to a tuple of terms (Loves(Alice, Bob), IsGreaterThan(x, y))
Represent basic assertions about objects and their relations
Logical Connectives and Quantifiers
Logical connectives are used to combine simpler formulas into more complex ones
Conjunction (∧ \land ∧ ): "and" connects two formulas (ϕ ∧ ψ \phi \land \psi ϕ ∧ ψ )
Disjunction (∨ \lor ∨ ): "or" connects two formulas (ϕ ∨ ψ \phi \lor \psi ϕ ∨ ψ )
Implication (→ \rightarrow → ): "if...then" connects two formulas (ϕ → ψ \phi \rightarrow \psi ϕ → ψ )
Negation (¬ \lnot ¬ ): "not" negates a formula (¬ ϕ \lnot \phi ¬ ϕ )
Quantifiers express properties about collections of objects
Universal quantifier (∀ \forall ∀ ): "for all" specifies that a formula holds for all objects (∀ x ϕ ( x ) \forall x \, \phi(x) ∀ x ϕ ( x ) )
Existential quantifier (∃ \exists ∃ ): "there exists" specifies that a formula holds for at least one object (∃ x ϕ ( x ) \exists x \, \phi(x) ∃ x ϕ ( x ) )
Well-formed formulas (wffs) are syntactically correct expressions in first-order logic
Atomic formulas are wffs
If ϕ \phi ϕ and ψ \psi ψ are wffs, then so are (ϕ ∧ ψ \phi \land \psi ϕ ∧ ψ ), (ϕ ∨ ψ \phi \lor \psi ϕ ∨ ψ ), (ϕ → ψ \phi \rightarrow \psi ϕ → ψ ), and (¬ ϕ \lnot \phi ¬ ϕ )
If ϕ \phi ϕ is a wff and x x x is a variable, then ∀ x ϕ \forall x \, \phi ∀ x ϕ and ∃ x ϕ \exists x \, \phi ∃ x ϕ are also wffs
Free and bound variables
A variable x x x is bound in a formula if it falls within the scope of a quantifier (∀ x \forall x ∀ x or ∃ x \exists x ∃ x )
A variable is free if it is not bound by any quantifier
In ∀ x ∃ y ( P ( x ) ∧ Q ( x , y , z ) ) \forall x \, \exists y \, (P(x) \land Q(x,y,z)) ∀ x ∃ y ( P ( x ) ∧ Q ( x , y , z )) , x x x and y y y are bound, while z z z is free
Scope of quantifiers
The scope of a quantifier is the portion of the formula it applies to
In ∀ x ( P ( x ) ∧ ∃ y Q ( x , y ) ) \forall x \, (P(x) \land \exists y \, Q(x,y)) ∀ x ( P ( x ) ∧ ∃ y Q ( x , y )) , the scope of ∀ x \forall x ∀ x is the entire formula, while the scope of ∃ y \exists y ∃ y is Q ( x , y ) Q(x,y) Q ( x , y )