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) }.

Describe the given vocabulary using the right terminology (constants, relation, property, arity)

First-Order Models

A model is an ordered pair $(D,F)$ with domain $D$ and interpretation function $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)}.     

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.

The Satisfaction Definition

• Aim: define what it means that a sentences is true in a model.

• Why is it not trivial to define the truth of a sentence inductively (in terms of subformulas)?

• 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

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)]).

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önneten wir nicht direkt mit D anstelle von Dom in den Zeilen darüber arbeiten? ```{.prolog} % 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=Value2und 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?

Compositionality

Two experiments

%%%%%%%%%%%%%%%%%

% Syntax-Semantics Rules 

%%%%%%%%%%%%%%%%%
% quantifier free sentences

s(Sem)--> np(SemNP), vp(Sem), 
   {
    arg(1,Sem,SemNP)
   }.

np(Sem)--> pn(Sem).

vp(Sem)--> tv(Sem), np(SemNP), 
   { 
    arg(2,Sem,SemNP)
   }.

%%%%%%%%%%%%%%%%%

% quantifier sentences

s(Sem)--> np(Sem), vp(SemVP), 
   {
    arg(1,SemVP,X),
    arg(1,Sem,X),
    arg(2,Sem,Matrix),
    arg(2,Matrix,SemVP)
   }.
            

np(Sem)--> det(Sem), noun(SemNoun), 
   {
    arg(1,SemNoun,X),
    arg(1,Sem,X),
    arg(2,Sem,Matrix),
    arg(1,Matrix,SemNoun)
   }.


vp(Sem)--> tv(SemTV), np(Sem), 
   {
    arg(2,SemTV,X),
    arg(1,Sem,X),
    arg(2,Sem,Matrix),
    arg(2,Matrix,SemTV)
   }.
   
   
vp(Sem)--> iv(Sem).

%%%%%%%%%%%%%%%%%
% Lexicon
%%%%%%%%%%%%%%%%%

%  Proper Names

pn(mia)--> [mia].

%   Transitive Verbs

tv(love(_,_))--> [loves].

%  Intransitive Verbs

iv(snort(_))--> [snorts].

%  Determiners

det(exists(_,_ & _))--> [a].

% Nouns

noun(woman(_))--> [woman].

Experiment 2

* Wie arbeitet die Regel NP -> PN?

The Lambda Calculus