Alphabet
The alphabet of a first-order language consists of the following distinct symbols:
Logical symbols
Logical symbols | |
---|---|
Logical connectives | |
Punctuation Symbols | Comma and Parentheses |
Variables () | |
Quantifier symbols | (universal quantification), (existential quantification) |
Equality (optional) |
Non-logical symbols (Signature)
Non-logical symbols | |
---|---|
Predicate Symbols | (For each arity ) |
Function Symbols (optional) | (For each arity ) |
Constant Symbols (optional) |
- The set of constant symbols, function symbols, and predicate symbols is called the signature of the language.
- The set of all symbols is called the alphabet of the language.
- The function that assigns to each symbol its arity is called the signature function.
Terms
The set of terms is inductively defined by the following rules:
- Each variable and each constant symbol is a term
- If is an -ary function symbol, and are terms, then is a term
Formulas
The set of formulas (also called well-formed formulas or WFFs) is inductively defined by the following rules:
- Predicate symbols. If is an -ary predicate symbol and are terms then is a formula.
- Negation. If is a formula, then is a formula.
- Binary connectives. If and are formulas, then is a formula. (Similar rules apply to other binary logical connectives).
- Quantifiers. If φ is a formula and is a variable, then (for all , holds) and (there exists such that ) are formulas
Only expressions which can be obtained by finitely many applications of rules are formulas.
The formulas obtained from the first two rules are said to be atomic formulas.
- Let be a set of formulas
- A boolean combination of formulas from is a formula that can be obtained from formulas from by finitely many applications of the rules for binary connectives and negation.
- A positive boolean combination of formulas from is a formula that can be obtained from formulas from by finitely many applications of the rules for binary connectives.
- The boolean closure of is the set of all boolean combinations of formulas from .
- A formula is positive if it can be obtained from atomic formulas using only binary connectives and quantifiers.
- A negative formula is a negated positive formula.
- A formula is quantifier-free if it contains no quantifiers
Unique Readability
Induction on wffs principle
- (Theorem 5.4)
- Prove for all atomic formulas Atodo
Free & Bound Variables
-
For each quantifier , and let be a formula , we say that is the scope of
-
The concept that a variable occurs free or bound (also: is a free or bound occurrence) in formula is defined recursively as follows:
- Atomic formulas:
- If is an atomic formula, then occurs free in if and only if occurs in .
- Moreover, there are no bound variables in any atomic formula.
- Negation:
- occurs free in if and only if occurs free in φ.
- occurs bound in if and only if occurs bound in φ
- Binary connectives:
- occurs free in if and only if occurs free in either or .
- occurs bound in if and only if occurs bound in either or .
- (The same rule applies to any other binary connective in place of .)
- Quantifiers: ( is either or )
- occurs free in , if and only if occurs free in and is a different symbol from .
- occurs bound in , if and only if is or occurs bound in .
- Atomic formulas:
-
A variable is a free variable in , if and only if, it has at least one free occurrence in
-
A variable is a bound variable in , if and only if, all occurrences of in are bound
Universal Closure
- Given is the set of free variables in , then is the universal closure of the formula
Sentence
- A formula is called a sentence (or closed formula), if these is no free variable in , i.e. all occurrences of in are bound
Substitution
-
The substitution replaces each free occurrence of the variable in the formula with the term
-
The substitution is a capture-avoiding substitution if and only if no variable occur in become bonud (we say that is substitutable for in , or the quantifier does not capture the variable in .)
-
If is a fresh variable (i.e. does not occur in (niether free nor bound)), then .
- The replacement of by is called renaming (רענון משתנים) of the variable to in .
Theory
- A theory is a consistent set of sentences
In the propositional logic a complete theory has unique model (4.5), but in the predicate logic, a complete theory may have many models.
A theory can be considered on two levels. One is the proof theory level (see Predicate Calculus), where we focus on the syntactic aspects (strings (which are formulas) and on manipulating strings according to rules). The other is the model theory level, where we focus on the semantic aspects as the class of all models of the theory.
Minimal Language
Normal Forms
Prenex Normal Form (5.7.2)
- A formula is said to be in prenex form if it is of the form where each is either or , and where contains no quantifiers.
- The sequence of quantifiers and variables at the beginning is called the prefix, and the quantifier-free formula that follows the matrix.
- If is in prenex form and its metrix is DNF then it is said to be in prenex normal form (PNF)
Skolem normal form
https://en.wikipedia.org/wiki/Skolem_normal_form
BNF
Restricted languages
If the set of relation symbols, function symbols, and constant symbols of a language $L$ is a subset of the set of alphabet symbols of $L'$, then $L$ is called a **reduction** of the language $L'$, and $L'$ is called an **enrichment** of the language L. Every noun in $L$ is also a noun in $L'$, and every formula in $L$ is also a formula in $L'$. If M is a model in the extended language $L'$, then the reduction of M to the language $L$ is obtained by ignoring the relations and functions that have been named in $L'$ but are not in the language $L$ (on the other hand, if M is a model in the language L, then there are many enrichments of the model to a model in the language $L'$, because there are many functions and relations in the model to which the additional names can be assigned). It is important to note that the locality of the definition by induction (of the value of a noun in an assignment, and of the truth value of a formula in an assignment) ensures that the definition of the truth value of a formula does not depend on the interpretation that the model gives to the symbols that are not mentioned in the formula. In precise terms, this means:
- (Theorem 5.7) Let $M_{1}$ and $M_{2}$ be two models in the languages $L_{1}$ and $L_{2}$, respectively, whose domain is the same set $A$, such that every assignment in one model is also an assignment in the other model. Let $\varphi$ be a formula that is in the intersection of the two languages. If the two models interpret the relation symbols, the function symbols, and the constant symbols that appear in the formula ϕ in the same way, then for every assignment S in the domain A: $M_{1}⊨_{S}\varphi\iff M_{2}⊨_{S}\varphi$
- In particular, if $L_{2}$ is a reduction of $L_{1}$ and $M_{2}$ is the reduction of $M_{1}$, then for every assignment $S$ and for every formula $\varphi$ in $L_{2}$: we have $M_{1}⊨_{S}\varphi\iff M_{2}⊨_{S}\varphi$
todo 5.4.6 #todo 5.4.7