Syntax
These rules define the syntax of first-order predicate logic and specify how valid formulas are constructed from atomic components.
3.1 Syntax:
In first-order predicate logic, the syntax defines the rules for constructing well-formed formulas (WFFs) from the basic components of the language. These components include terms, predicates, quantifiers, logical connectives, and variables.
Terms: A term represents an object within the domain of discourse. It can be constructed according to the following rules:
Constant: A constant is a term with a fixed value belonging to the domain ( D ).
Variable: A variable is a term that may take values in the domain ( D ).
Function Application: If ( f ) is a function of ( n ) arguments and ( t_1, \ldots, t_n ) are terms, then ( f(t_1, \ldots, t_n) ) is also a term.
Generation: All terms are generated by applying the rules above.
Predicates of Arity ( n ): A predicate represents a property or relation between objects. It is defined by its arity, which specifies the number of arguments it takes.
Atom or Atomic Formula: An atomic formula in first-order predicate logic consists of a predicate symbol followed by a list of ( n ) terms, where ( n ) is the arity of the predicate. It represents a basic assertion about objects in the domain.
Literal: A literal in first-order logic is either an atomic formula or the negation of an atomic formula.
Well-Formed Formula (WFF): A well-formed formula in first-order predicate logic is constructed according to the following rules:
An atom is a WFF.
If ( P[x] ) is a WFF, then ( \neg P[x] ) is also a WFF.
If ( P[x] ) and ( Q[x] ) are WFFs, then ( P[x] \land Q[x] ), ( P[x] \lor Q[x] ), ( P[x] \rightarrow Q[x] ), and ( P[x] \leftrightarrow Q[x] ) are also WFFs.
If ( P[x] ) is a WFF, then ( \forall x , P[x] ) and ( \exists x , P[x] ) are also WFFs.
The set of all WFFs can be generated by repeatedly applying rules (1) to (4).
Well-formed formulas serve as the basis for expressing logical statements and reasoning about objects and relationships within a formal system.
CNF (Conjunctive Normal Form):
Conjunctive Normal Form (CNF) is a standard form used in propositional logic and boolean algebra to represent logical formulas as a conjunction of clauses, where each clause is a disjunction of literals. In CNF, a logical formula is represented as the conjunction (AND) of multiple clauses, each of which is a disjunction (OR) of literals. CNF is important in logic because any propositional formula can be converted into an equivalent formula in CNF.
CNF is represented as follows:
F 1 ∧F 2 ∧…∧ F n
Where:
F 1 ,F 2 ,…,F n are clauses.
Each clause Fi is a disjunction of literals: L i1 ∨L i2 ∨…∨L im .
DNF (Disjunctive Normal Form):
Disjunctive Normal Form (DNF) is another standard form used in propositional logic and boolean algebra to represent logical formulas as a disjunction of conjunctions, where each conjunction is a conjunction of literals. In DNF, a logical formula is represented as the disjunction (OR) of multiple conjunctions, each of which is a conjunction (AND) of literals. DNF is also important because any propositional formula can be converted into an equivalent formula in DNF.
DNF is represented as follows:
F 1 ∨F 2 ∨…∨F n
Where:
are conjunctions.
Each conjunction Fi is a conjunction of literals:
CNF and DNF are standard forms used to represent logical formulas in propositional logic. CNF represents formulas as a conjunction of clauses, each of which is a disjunction of literals, while DNF represents formulas as a disjunction of conjunctions, each of which is a conjunction of literals. These forms are useful for simplifying and manipulating logical formulas in various applications, including theorem proving, model checking, and circuit design.
Last updated