First Order Logic - Hikkihiki/LogicVerifier GitHub Wiki
Prerequisite
First order logic is an extension over propositional logic with the following addition.
Variables
Denoted by ..., x, y, z. They are used to represent elements in the underlying set, which gives the name "first order". They cannot represent a set, which is the feature of "second order".
Constants
Denoted by a, b, c, .... A constant represent a specific element in the underlying set. Which could be assigned to a variable.
Functions
Denoted by lower case letters ..., f, g, h,..., e.g. f(x). Usually function maps elements to another element in the underlying set.
Relations
Denoted by upper case letters ..., P, Q, R, S, ..., e.g. R(x, y). Usually relations denote a truth value and is represented by a set, which is true if and only if the tuple (x ,y) is an element of the set.
Symbols
First order logic is composed of the following symbols: &, |, ~, ->, <->, (, ), \exists, \forall For simplicity, we add "=" which represents the relation equality that is commonly use in mathematics.
Syntax
A formula is represented by \phi, \psi etc.
Term
- Every variable and constant is a term.
- If f is a m-ary function and t1, ..., tm are term. Then f(t1, ..., tm) is also term.
Atomic Formula
An atomic formula is any m-ary relation R(t1, ..., tm), where t1, ..., tm are terms. This includes the binary relation "t1 = t2".
Syntax Rules
The ~, &, \exists form the primitive rules of constructing complex formula. For convenient, some other rules might be applied.
- If \phi is a formula, then ~\phi is also a formula.
- If \phi, \psi are formulas, then (\phi & \psi) is also a formula.
- If \phi is a formula, then \exists x \phi is also a formula for any variable x.
Subformula
(todo)
Free variables
The free variables of a formula \phi are the variables without quantifying by a quantifier. For example x is a free variable in the formula \forall y R(x, y).
Sentence
A sentence of first order logic is a formula without free variables. The notion of truth is only available in sentence but not formula with free variables.
Semantic
Structure
Just like assignment in propositional logic assign truth value to atomic formula, structure in first order logic gives context on determining the truth value to atomic formula.
A structure describes the underlying set, constants, functions and relations.