# Syntax

**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:

1. **Constant:** A constant is a term with a fixed value belonging to the domain ( D ).
2. **Variable:** A variable is a term that may take values in the domain ( D ).
3. **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.
4. **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:

1. An atom is a WFF.
2. If ( P\[x] ) is a WFF, then ( \neg P\[x] ) is also a WFF.
3. 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.
4. If ( P\[x] ) is a WFF, then ( \forall x , P\[x] ) and ( \exists x , P\[x] ) are also WFFs.
5. 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:

* $$F1​,F2​,…,Fn​$$ are conjunctions.
* Each conjunction  Fi  is a conjunction of literals: $$Li1​∧Li2​∧…∧Lim​$$

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.