SKEDSOFT

Semantics: Before we can continue in the "syntactic" domain with concepts like Inference Rules and Proofs, we need to clarify the Semantics, or meaning, of First Order Logic.
An L-Structure or Conceptualization for a language L is a structure M= (U,I), where:

• U is a non-empty set, called the Domain, or Carrier, or Universe of Discourse of M, and
• I is an Interpretation that associates to each n-ary function symbol F of L a map

            I(F): UxU..xU -> U
and to each n-ary predicate symbol P of L a subset of UxU..xU.
The set of functions (predicates) so introduced form the Functional Basis (Relational Basis) of the conceptualization.

Given a language L and a conceptualization (U,I), an Assignment is a map from the variables of L to U. An X-Variant of an assignment s is an assignment that is identical to s everywhere except at x where it differs. Given a conceptualization M=(U,I) and an assignment s it is easy to extend s to map each term t of L to an individual s(t) in U by using induction on the structure of the term. Then

• M satisfies a formula A under s iff

1. A is atomic, say P(t1 .. tn), and (s(t1) ..s(tn)) is in I(P).
2. A is (NOT B) and M does not satisfy B under s.
3. A is (B OR C) and M satisfies B under s, or M satisfies C under s. [Similarly for all other connectives.]
4. A is (ALL x B) and M satisfies B under all x-variants of s.
5. A is (EXISTS x B) and M satisfies B under some x-variants of s.

• Formula A is satisfiable in M iff there is an assignment s such that M satisfies A under s.
• Formula A is satisfiable iff there is an L-structure M such that A is satisfiable in M.
• Formula A is valid or logically true in M iff M satisfies A under any s. We then say that M is a model of A.
• Formula A is Valid or Logically True iff for any L-structure M and any assignment s, M satisfies A under s.

Some of these definitions can be made relative to a set of formulae GAMMA:

• Formula A is a Logical Consequence of GAMMA in M iff M satisfies A under any s that also satisfies all the formulae in GAMMA.
• Formula A is a Logical Consequence of GAMMA iff for any L-structure M, A is a logical consequence of GAMMA in M. At times instead of "A is a logical consequence of GAMMA" we say "GAMMA entails A".

We say that formulae A and B are (logically) equivalent iff A is a logical consequence of {B} and B is a logical consequence of {A}.

EXAMPLE 1: A Block World
Here we look at a problem and see how to represent it in a language. We consider a simple world of blocks as described by the following figures:

We see two possible states of the world. On the left is the current state, on the right a desired new state. A robot is available to do the transformation. To describe these worlds we can use a structure with domain U = {a b c d e}, and with predicates {ON, ABOVE, CLEAR, TABLE} with the following meaning:

• ON: (ON x y) iff x is immediately above y. The interpretation of ON in the left world is {(a b) (b c) (d e)}, and in the right world is {(a e) (e c) (c d) (d b)}.
• ABOVE: (ABOVE x y) iff x is above y. The interpretation of ABOVE [in the left world] is {(a b) (b c) (a c) (d e)} and in the right world is {(a e) (a c) (a d) (a b) (e c) (e d) (e b) (c d) (c b) (d b)}
• CLEAR: (CLEAR x) iff x does not have anything above it. The interpretation of CLEAR [in the left world] is {a d} and in the right world is {a}
• TABLE: (TABLE x) iff x rests directly on the table. The interpretation of TABLE [in the left world] is {c e} and in the right world id {b}.

Examples of formulae true in the block world [both in the left and in the right state] are [these formulae are known as Non-Logical Axioms]:

• (ON x y) IMPLIES (ABOVE x y)
• ((ON x y) AND (ABOVE y z)) IMPLIES (ABOVE x z)
• (ABOVE x y) IMPLIES (NOT (ABOVE y x))
• (CLEAR x) IFF (NOT (EXISTS y (ON y x)))
• (TABLE x) IFF (NOT (EXISTS y (ON x y)))

Note that there are things that we cannot say about the block world with the current functional and predicate basis unless we use equality. Namely, we cannot say as we would like that a block can be ON at most one other block. For that we need to say that if x is ON y and x is ON z then y is z. That is, we need to use a logic with equality.
Not all formulae that are true on the left world are true on the right world and viceversa. For example, a formula true in the left world but not in the right world is (ON a b). Assertions about the left and right world can be in contradiction. For example (ABOVE b c) is true on left, (ABOVE c b) is true on right and together they contradict the non-logical axioms. This means that the theory that we have developed for talking about the block world can talk of only one world at a time. To talk about two worlds simultaneously we would need something like the Situation Calculus that we will study later.