Transcript Many Sorted First-order Logic

Many Sorted First-order Logic
Student: Liuxing Kan
Instructor: William Farmer
Dept. of Computing and Software
McMaster University, Hamilton, CA
Contents
•
•
•
•
•
•
•
•
•
Introduction: What is many sorted FOL
Syntax: Languages of many sorted FOL
Syntax: Terms and Formulas of many sorted FOL
Example of Many-sorted FOL Semantics
Semantics of many sorted FOL
Proof Theory of Many-sorted FOL
The completeness of many-sorted logic
Reduction many-sorted logic to one-sorted logic
Reference
Introduction: what is many-sorted FOL
•
Sometimes people want to express properties of structures of different sorts (types).
There are plenty of examples of subjects where the semantics of formulas are manysorted structures. For instance, in geometry, to take a simple and ancient example,
we use universes of pointes, lines, angles, triangles, rectangles, polygons, etc.
•
By adding to the formalism of first-order logic the notion of sort, we can obtain a
flexible and convenient logic called many-sorted first order logic, which has the same
properties as first order logic.
•
In contrast to FOL, in many-sorted FOL, the arguments of function and predicate
symbols may have different sorts, and constant and function symbols also have some
sorts.
•
Uses of many-sorted logic: abstract data types, semantics and program verification,
definition of programming languages, algebras for logic, databases, dynamic logic,
semantics of natural languages, computer-aided problem solving, knowledge
representation of design, logic programming and automated deduction.
Syntax: Languages of many sorted FOL
•
In contrast to standard first-order languages, in many-sorted first order languages,
the argument of function and predicate symbols may have different sorts, and
constant and function symbols also have some sort. Technically, this means that a
many-sorted alphabet is a many-sorted ranked alphabet. (An S-ranked alphabet is
pair(Σ,r) consisting of a set Σ together with a function r: Σ→S*×S assigning a rank (u,
s) to each symbol f in Σ )
•
Alphabet of many-sorted first order language:
－ S U {bool} of sorts containing the special sort bool
－ Connectives: Λ,ν,→,↔, all of rank (bool.bool, bool), ¬(not) of rank (bool, bool),
┴(of rank (e, bool));
－ Quantifiers: ∀ , ∃ , each of rank (bool, bool);
－ Variables: a countable set Vs={X0,X1,X2…}, each variable Xi being of rank (e,s).
－ Auxiliary symbols: “(” and “)”
－ Equality symbol ≒, of rank (ss, bool)
Syntax: Languages of many sorted FOL
•
A (S U {bool})-ranked alphabet L of nonlogical symbols consisting of:
－ FS: function symbols, FS→S+×S, assigning a pair r(f)=(u,s) called rank to every
function symbol f. The string u is called the arity of f, and the symbol s is the sort of f.
－ CSs: constants, For every sort s∈S, a set CSs of symbols c0,c1,…, each of rank (e,s).
The family of sets CSs is denoted by CS
－ PS: predicate symbols, A set PS of symbols P0,P1,…,and a rank function
r:PS→S+×{bool}, assigning a pair r(P)=(u,bool) called rank to each predicate symbol
P. The string u is called the arity of P. If u=e, P is a propositional letter.
•
It is assumed that the sets Vs, FS, CSs, and PS are disjoint for all s∈S. We will refer
to a many-sorted first order language with set of nonlogical symbols L as the
language L. Many-sorted first order languages obtained by omitting the equality
symbol are referred to as many-sorted first order languages without equality.
Syntax: Terms and Formulas of M-S FOL
•
Let L=(CS,FS,PS) be a language of many sorted FOL
•
Terms atomic formulas of L are defined as follows:
－ Each constant and each variable of sort sis a term of L.
－ If t1,…,tn are terms, each ti of sort ui, and f is function symbol of rank (u1…un,s),
then ft1…tn is a term of sort s
－ Each propositional letter is an atomic formula.
－ If t1,…,tn are terms, each ti of sort ui, and P is a predicate symbol of arity u1…un,
then Pt1…tn is an atomic formula:
•
Formulas are defined as follows:
－ Every atomic formula is a formula
－ For any two formula A and B, (AΛB), (AνB), (A →B), (A↔B ), ¬A are also formula
－ For any variable xi of sort s and any formula A, ∀sxiA and ∃sxiA are also formulas
Example of Many-sorted FOL
•
Let L be following many-sorted first order language for stacks, where S={stack,
integer}, CSinterger={0}, CSstack={Λ}, FS={Succ, +, *, push, pop, top}, and PS={<}
The rank functions are given by:
－ r(succ)=(integer, integer);
－ r(+)=r(*)=(integer.integer, integer);
－ r(push)=(stack.integer, stack);
－ r(pop)=(stack, stack);
－ r(top)=(stack, integer);
－ r(<)=(integer.integer, bool);
Then, the following are terms:
Succ 0
top push Λ Succ 0
The following are formulas:
< 0 Succ 0
∀integerx ∀stacky≒stack pop push y x y
Semantics of many sorted FOL
•
•
Many-sorted first order structures
－ First, let define many-sorted Σ-algebra A is a pair <A,I>, where A=(As)s∈S is an Sindexed family of nonempty sets, each As being called a carrier of sort s, and I is an
interpretation function assigning functions to the function symbols.
－ Give a many-sorted first order language L, a many-sorted L-structure M is a manysorted L-algebra, such that the carrier of sort bool is the set BOOL={T,F}
Semantics of formulas
Given a many-sorted L-structure M and an assignment v: V→M, the function tM:
[V→M]→Ms defined by a term t of sort s is the function such that for every
assignments v in [V→M], the value tM[v] is defined recursively as follows:
1. For a variable x of sort s, xM[v]=vs(x)
2. For a constant c, cM[v]= cM
3. Let t=f(t1…tn), then (ft1…tn)M[v]=fM((t1)M[v],…(tn)M[v])
4. Let A=P(t1…tn), then (Pt1…tn)M[v]=PM((t1)M[v],…(tn)M[v])
5. If (t1)M[v]=(t2)M[v] then (≒st1t2)M[v]=T otherwise F
6. Let * denotes {Λ, ν→, ↔}, then (A*B)M=*M(AM,BM)
7. (∀xi:sA)M[v]=T iff AM[v[xi:=m]]=T, for all m∈Ms and (∃ xi:sA)M[v]=T iff AM[v[xi:=m]]=T,
for some m∈Ms
Proof Theory of Many-sorted FOL
•
•
Gentzen System G for Many-sorted Languages Without Equality
Gentzen System G= for languages With Equality
The completeness of many-sorted logic
•
•
There are two degrees of completeness:
Weak completeness: Each validity is a theorem. That is, |=Φimplies |-Φ for every
formula Φ.
Strong completeness: Every consequence of a set of formulas is also derivable from
it. That is, for every set of formulas Γ and formulas Φ , when every Γ|=Φ then also Φ
can be deduced from Γ.
Henkin’s theorem: Γ consistent → Γ has a model.
Reduction to one-sorted logic
•
There is translation of many-sorted logic into one-sorted logic. Such a translation is
described in Enderton, 1972, and you can read it for details. The essential idea to
convert a many-sorted language L in to a one-sorted language L is to add domain
predicate symbols Ds, one for each sort, and to modify quantified formulas recursively
as follows:
Every formula A of the form ∀x : sB (or ∃: sB) is converted to the formula A’ = ∀
x(Ds(x)→B’ ), where B’ is the result of converting B
Reference
•
•
Many-Sorted Logic And its Applications, K.Meinke and J.V.Tucker
Logic for Computer Science: Foundations of Automatic Theorem Proving, Jean
Gallier