1.1 First-Order Logic

Vocabularies

  • First, the vocabulary tells us what we’re going to be talking about:
    • individuals: Mia …;
    • 2-place relations: love, hate, …;
    • 1-place relation / property: robber, …
  • Second, the vocabulary also tells us how we are going to talk about these things: MIA as a symbol for Mia, LOVE as a symbol for the love relation,…
{ (LOVE,2),
(CUSTOMER,1),
(ROBBER,1),
(MIA,0),
(VINCENT,0),
(HONEY-BUNNY,0),
(YOLANDA,0) }.

First-Order Models

A model is an ordered pair \((D,F)\) with domain \(D\) and interpretation function \(F\).

Beschreiben sie \(F\).

D3 = { d1 , d2, d3, d4, d5}

F3(MIA) = d2     
F3(HONEY-BUNNY) = d1     
F3(VINCENT) = d4     
F3(YOLANDA) = d1     
F3(CUSTOMER) = {d1,d2,d4}     
F3(ROBBER) = {d3,d5}     
F3(LOVE) = {(d3,d4)}.

Exercise 1.1.4 Consider the following situation: There are four blocks. Two of the blocks are cubical, and two are pyramid shaped. The cubical blocks are small and red. The larger of the two pyramids is green, the smaller is yellow. Three of the blocks are sitting directly on the table, but the small pyramid is sitting on a cube. Devise a suitable vocabulary and present this situation as a model.

First-Order Languages (Note the plural!)

A first-order language over a vocabulary uses the following ingredients:

  1. All the symbols in the vocabulary. (non-logical symbols)
  2. A countably infinite collection of variables x, y, z, w, …
  3. The boolean connectives \(\neg\), (negation), \(\wedge\) (conjunction), \(\vee\) (disjunction), and \(\rightarrow\) (implication).
  4. The quantifiers \(\forall\) (the universal quantifier) and \(\exists\) (the existential quantifier).
  5. The round brackets ) and ( and the comma.

Some terminology:

  • term: any constant or any variable
  • atomic formula: If R is a relation symbol of arity n, and \(\tau_1, \ldots, \tau_n\) are terms, then \(R(\tau_1, \ldots, \tau_n)\) is an atomic formula.

Syntax

Defintion of well formed formulas (wffs):

  1. All atomic formulas are wffs.
  2. If \(\phi\) and \(\psi\) are wffs then so are \(\neg \phi, (\phi \wedge \psi), (\phi \vee \psi), (\phi \rightarrow \psi)\).
  3. If \(\phi\) is a wff, and x is \(a\) variable, then both \(\exists x \phi\) and \(\forall x \phi\) are wffs. (We call \(\phi\) the matrix of such wffs.)
  4. Nothing else is a wff.

Klammern werden wie üblich weggelassen (Präzedenz der Booleschen Operatoren beachten).

free/bound variables:

  1. Any occurrence of any variable is free in any atomic formula.
  2. If an occurrence of any variable is free in \(\phi\) or in \(\psi\), then that same occurrence is free in \(\neg\phi\), \((\phi \wedge \psi)\), \((\phi \vee \psi)\), and \((\phi \rightarrow \psi)\).
  3. If an occurrence of a variable \(x\) is free in \(\phi\), then that occurrence is free in \(\forall y \phi\) and \(\exists y \phi\) (for any variable y distinct from x). However, no occurrence of x is free in \(\forall x \phi\) and \(\exists x \phi\) .
  4. The only free variables in a formula \(\phi\) are those whose freeness follows from the preceding clauses. Any variable in a formula that is not free is said to be bound.

A formula that contains no occurrences of free variables is called a sentence of first-order logic.

Exercise 1.1.5 Represent the following English sentences in first-order logic:

  1. If someone is happy, then Vincent is happy.
  2. Some cars are damaged and there are bullet holes in some of the walls.
  3. Everybody in the basement is wearing a leather jacket or a dog collar.
  4. Either Butch and Pumpkin are fighting or Vincent has a weird experience

Exercise 1.1.8 Give an inductive definition of subformulahood. That is, for each kind of formula in the language (atomic, boolean, and quantified) specify exactly what its subformulas are. The subformulas of a formula \(\phi\) are \(\phi\) itself and all the formulas used to build \(\phi\).

The Satisfaction Definition

  • Ziel die Wahrheit von Sätzen in einem Modell zu definieren.

  • Warum lässt sich nicht so ohne weiteres induktiv (in terms of subformulas) definieren, wann ein Satz in einem Modell wahr ist?

  • satisfaction \(\subseteq\) formulas \(\times\) models \(\times\) assignments

Given a model M = (D, F), an assignment of values to variables in M (or more simply, an assignment in M) is a function g from the set of variables to D.

Let M = (D, F) be a model, let g be an assignment in M, and let \(\tau\) be a term. Then the interpretation of \(\tau\) with respect to M and g is F(\(\tau\)) if \(\tau\) is a constant, and g(\(\tau\)) if \(\tau\) is a variable. We denote the interpretation of \(\tau\) by \(I^g_F(\tau)\).

Let g be an assignment in some model M, and let x be a variable. If g’ is also an assignment in M, and for all variables y distinct from x we have that g’(y)= g(y), then we say that g’ is an x-variant of g.

Let \(\phi\) be a formula, let M = (D, F) be a model, and let g be an assignment in M. Then the relation \(M,g \models \phi\) (\(\phi\) is satisfied in M with respect to the assignment g) is defined inductively as follows:

A sentence \(\phi\) is true in a model M if and only if for any assignment g of values to variables in M, we have that \(M, g \models \phi\). If \(\phi\) is true in M we write \(M \models \phi\).

Function Symbols, Equality, and Sorted First-Order Logic

Function Symbols

  1. All constants and variables are terms.
  2. If f is a function symbol of arity n, and \(\tau_1, \ldots \tau_n\) are terms, then \(f(\tau_1, \ldots \tau_n)\) is also a term.
  3. Nothing else is a term.

A term is said to be closed if and only if it contains no variables.

if \(\tau\) is a term of the form \(f(\tau_1, \ldots \tau_n)\), then we define \(I^g_F(\tau)\) to be \(F(f)(I^g_F\tau_1, \ldots I^g_F\tau_n)\).

Equality

\(=\) is a two-place relational symbol with fixed interpretation (logical symbol): For any model M, any assignment g in M, and any terms \(\tau_1\) and \(\tau_2\): \[ M, g \models \tau_1= \tau_2 \text{ iff } I^g_F\tau_1 = I^g_F\tau_2\].

Sorted first-order logic

The domain can be sorted into subclasses (animate/inanimate ). The interpretation of a sorted variable is restricted to its corresponding subclass.

Exercise 1.1.18 There is a famous analysis, due to the philosopher Bertrand Russell, of the meaning of the determiner the in sentences like The robber is screaming. Russell claims that this sentence would be true in some situation if (a) there was at least one robber in the situation, (b) there was at most one robber in the situation, and (c) that robber was screaming. Write down a first-order sentence which expresses this analysis of The robber is screaming. Note: you will have to use the equality symbol.

some analogies made in the text:

  • Models \(\approx\) situations
  • formulas \(\approx\) descriptions
  • free variables \(\approx\) pronouns
  • terms are the noun phrases of FO-languages
  • assignment of values to variables \(\approx\) (highly idealised) mathematical model of context
  1. Haben sie noch mehr entdeckt? Können sie die Vergleiche nachvollziehen?
    1. Die Autoren betonen, dass aus Sicht der Linguistik satisfaction ein wichtiger Begriff ist als truth, warum?

1.2 Three Inference Tasks

The Querying Task

The Querying Task: Given a model M and a first-order formula \(\phi\), is \(\phi\) satisfied in M or not?

The Consistency Checking Task

pretheoretic concept:

  • consistency \(\approx\) makes sense
  • inconsistency \(\approx\) does not make sense

A first-order formula is called satisfiable if it is satisfied in at least one model. A formula that is not satisfiable in any model is called unsatisfiable.

A finite set of formulas \({\phi_1,\ldots \phi_n}\) is satisfiable if \(\phi_1 \wedge \ldots \wedge \phi_n\) is satisfiable.

Note that satisfiability (and unsatisfiability) are model-theoretic or (as it is sometimes put) semantic concepts. That is, both concepts are defined using the notion of satisfaction in a model, and nothing else. Furthermore, note that satisfiability (and unsatisfiability) are mathematically precise concepts: we know exactly what first-order languages and first-order models are, and we know exactly what it means when we claim that a formula is satisfied in a model.

The Consistency Checking Task: Given a first-order formula \(\phi\), is \(\phi\) consistent (that is: satisfiable) or inconsistent (that is: unsatisfiable)?

  • Consistency checking for first-order logic is undecidable
  • But, from a proof-theoretic (or syntactic, i.e. symbol manipulation) perspective rather than a model-theoretic perspective partial solution to the consistency checking problem are possible.

The Informativity Checking Task

  • informative = invalid
  • uninformative (=trivial) = valid

A valid formula is a formula that is satisfied in all models (of the appropriate vocabulary) given any variable assignment. If \(\phi\) is a valid formula we write \(\models \phi\). A formula that is not valid is called invalid (\(\not\models \phi\)).

Suppose \(\phi_1, \ldots , \phi_n\), and \(\psi\) are a finite collection of first-order formulas. Then we say that the argument with premises \(\phi_1, \ldots , \phi_n\) and conclusion \(\psi\) is a valid argument if and only if whenever all the premises are satisfied in some model, using some variable assignment, then the conclusion is satisfied in the same model using the same variable assignment. The notation \[ \phi_1, \ldots , \phi_n \models \phi\] means that the argument with premises \(\phi_1, \ldots , \phi_n\) and conclusion \(\psi\) is valid.

Alternative terminology:

  • \(\psi\) is a valid inference from the premises \(\phi_1, \ldots , \phi_n\)
  • \(\psi\) is a logical consequence of \(\phi_1, \ldots , \phi_n\)
  • \(\psi\) is a semantic consequence of \(\phi_1, \ldots , \phi_n\)
  1. Erkläre wie die Begriffe valid formula und valid argument zusammenhängen (Semantic Decuction Theorem).

The Informativity Checking Task: Given a first-order formula \(\phi\), is \(\phi\) informative (that is: invalid) or uninformative (that is: valid)?

  • The informativity checking task is undecidable.
  • But again, partial solution from a proof-theoretic perspective.
  • consistency and informativity are related concepts:
    1. \(\phi\) is consistent (that is, satisfiable) if and only if \(\neg\phi\) is informative (that is, invalid).
    2. \(\phi\) is inconsistent (that is, unsatisfiable) if and only if \(\neg\phi\) is uninformative (that is, valid).
    3. \(\phi\) is informative (that is, invalid) if and only if \(\neg\phi\) is consistent (that is, satisfiable).
    4. \(\phi\) is uninformative (that is, valid) if and only if \(\neg\phi\) is inconsistent (that is, unsatisfiable).
% Prolog representation of a vocabulary
relation(love,2).             
relation(hate,2).             
relation(tell,2). 
relation(customer,1).         
relation(robber,1).           
constant(mia).
constant(vincent).
constant(honey_bunny).
constant(pumpkin).
% example(Number, Model)
test(_).
member(X,"hello").
test(X).
example(1,[customer(mia),customer(vincent),
           robber(pumpkin),robber(honey_bunny),
           love(pumpkin,honey_bunny)]).

example(2,[customer(mia),
           robber(pumpkin),robber(honey_bunny),
           love(pumpkin,honey_bunny)]).

1.3 A First-Order Model Checker

Representing Models in Prolog

% Representing Models in Prolog
% model(Domain,InterpretationFunctionF)

model([d1,d2,d3,d4,d5],
  [f(O,jules,d1),
  f(O,vincent,d2),
  f(O,pumpkin,d3),
  f(O,honey_bunny,d4),
  f(O,yolanda,d5),
  f(1,customer,[d1,d2]),
  f(1,robber,[d3,d4]),
  f(2,love,[(d3,d4)])]).

The Satisfaction Definition in Prolog

% satisfy/4
% statisfy(Formula,Model,Assignment,Polarity)


%% complex formulas
% not
satisfy(not(Formula),Model,G,pos):
   satisfy(Formula,Model,G,neg).
satisfy(not(Formula),Model,G,neg):
   satisfy(Formula,Model,G,pos).

% and
satisfy(and(Formula1,Formula2),Model,G,pos):
   satisfy(Formula1,Model,G,pos),
   satisfy(Formula2,Model,G,pos).
satisfy(and(Formula1,Formula2),Model,G,neg):
   satisfy(Formula1,Model,G,neg);
   satisfy(Formula2,Model,G,neg).

% or
satisfy(or(Formula1,Formula2),Model,G,pos):
   satisfy(Formula1,Model,G,pos);
   satisfy(Formula2,Model,G,pos).
satisfy(or(Formula1,Formula2),Model,G,neg):
   satisfy(Formula1,Model,G,neg),
   satisfy(Formula2,Model,G,neg).
   
% imp
satisfy(imp(Formula1,Formula2),Model,G,Pol):
   satisfy(or(not(Formula1),Formula2),Model,G,Pol).

Warum ist satisfy4-stellig? Wozu benötigen wir das Polarity-Argument?

% satisfy/4
% statisfy(Formula,Model,Assignment,Polarity)
   
%% Quantifiers
% some
satisfy(some(X,Formula),model(D,F),G,pos):-
   memberList(V,D),
   satisfy(Formula,model(D,F),[g(X,V)|G],pos).
satisfy(some(X,Formula),model(D,F),G,neg):
   setof(V,(
      memberList(V,D),
      satisfy(Formula,model(D,F),[g(X,V)|G],neg)
      ),
      Dom),
   setof(V,memberList(V,D),Dom).

% all
satisfy(all(X,Formula),Model,G,Pol):
  satisfy(not(some(X,not(Formula))),Model,G,Pol).
  • memberList/2 hat dieselbe Definition wie member.
  • warum benötigen wir in der obigen Definition setof(V,memberList(V,D),Dom), könnten wir nicht direkt mit D anstelle von Dom in den Zeilen darüber arbeiten?
% satisfy/4
% statisfy(Formula,Model,Assignment,Polarity)

%% atomic formulas
% 1-place predicates
satisfy(Formula,model(D,F),G,pos):
  compose(Formula,Symbol,[Argument]),
  i(Argument,model(D,F),G,Value),
  memberList(f(1,Symbol,Values),F),
  memberList(Value,Values).
satisfy(Formula,model(D,F),G,neg):
  compose(Formula,Symbol, [Argument]),
  i(Argument,model(D,F),G,Value),
  memberList(f(1,Symbol,Values),F),
  \+ memberList(Value,Values).

% 2-place predicates
satisfy(Formula,model(D,F),G,pos):
   compose(Formula,Symbol,[Arg1,Arg2]),
   i(Arg1,model(D,F),G,Value1),
   i(Arg2,model(D,F),G,Value2),
   memberList(f(2,Symbol,Values),F),
   memberList((Value1,Value2),Values).
satisfy(Formula,model(D,F),G,neg):
   compose(Formula,Symbol,[Arg1,Arg2]),
   i(Arg1,model(D,F),G,Value1),
   i(Arg2,model(D,F),G,Value2),
   memberList(f(2,Symbol,Values),F),
   \+ memberList((Value1,Value2),Values).
   
% equality (2-place predicate with fixed interpretation)
satisfy(eq(X,Y),Model,G,pos):
   i(X,Model,G,Value1),
   i(Y,Model,G,Value2),
   Value1=Value2.
satisfy(eq(X,Y),Model,G,neg):
   i(X,Model,G,Value1),
   i(Y,Model,G,Value2),
   \+ Value1=Value2.
  • Warum haben wir in der equality-Definition Value1=Value2 und nicht Value1==Value2?
compose(Term,Symbol,ArgList):-
   Term = .. [SymbollArgList].

% i/4
% i(Variable,Model,Assignment,AssignedValue)
i(X,model(_,F),G,Value):-
   (var(X),
   memberList(g(Y,Value),G),
   Y==X, !
   atom(X),
   memberList(f(O,X,Value),F)
   ).
  • Wie muss die Anfrage an satisfy/4 lauten, um die Formel some(X,and(customer(X),some(X,robber(X)))) in Model 1 zu evaluieren?
  • Erklären Sie warum die Evaluation das gewünschte Ergebnis liefert und warum es zu keinem Problem kommt, obwohl die Variable X in zwei unterschiedlichen Bindungskontexten vorkommt.
  • Wenn man wissen möchte, welche Assignments die Anfrage customer(X) erfüllen, wie muss die Anfrage lauten?
  • Die Implementierung des Model-Checkers ist noch nicht perfekt. Welche Probleme treten auf?