FO[Core]

This chapter describes the syntax and semantics of the minimal language constructs supported by every member of the FO[·] language family. Some of the constraints introduced by this minimal language are removed by extensions such as FO[Infinite].

Goal

FO[Core] is a typed (aka multi-sorted) first order logic with equality, if-then-else, and special constructs to facilitate the creation of identifiers and to specify the interpretation of predicates and functions. All types have a finite interpretation, allowing grounding [WMarienD14]. (This constraint is removed in FO[Int] and FO[Real])

Knowledge Base

This section describes the high-level structure of a knowledge base.

Lexicon

A Knowledge Base is a text file encoded in UTF-8.

The following character(s) are “white spaces”: they separate tokens, but have no meaning by themselves.

  • 0x09 (tab)

  • 0x10 (new line)

  • 0x13 (line feed)

  • 0x32 (space)

  • comments: string starting from // till the end of the line (0x10 or 0x13).

Token

Pattern

Example

ID

[^\d\W]\w*\b

Color

NAME_V

ID

V, the name of a vocabulary

NAME_TH

ID

T, the name of a theory

Syntax

KnowledgeBase ← VocabularyBlock { (VocabularyBlock | TheoryBlock | StructureBlock) };
  VocabularyBlock ← 'vocabulary' [NAME_V] '{' { Declaration } '}';
  TheoryBlock ← 'theory' [ NAME_TH [: NAME_V] ] '{' { Assertion } '}';
  StructureBlock ← 'structure' [ NAME_TH [: NAME_V] ] '{' { Interpretation } '}';
flowchart LR subgraph Knowledge Base direction LR begin{ } --> vocabulary([Vocabulary block]); vocabulary --> Block; vocabulary --> endF{ }; Block --> vocabulary; Block --> endF{ }; end;
flowchart LR subgraph Block direction LR start{ } --> vocabulary([Vocabulary block]); start --> theory([Theory block]); start --> structure([Structure block]); vocabulary --> endB{ }; theory --> endB; structure --> endB; end;
flowchart LR subgraph Vocabulary block direction LR vocabulary['vocabulary'] --> NAME_V([NAME_V]); NAME_V --> left["'{'"]; vocabulary --> left; left --> declaration([Declaration]); declaration --> declaration; declaration --> right["'}'"]; end;
flowchart LR subgraph Theory block direction LR theory['theory'] --> NAME_TH([NAME_TH]); theory --> leftT; NAME_TH --> dot[':']; NAME_TH --> leftT; dot --> voc([NAME_V]); voc --> leftT["'{'"]; leftT --> rightT; leftT --> assertion([Assertion]); assertion --> rightT["'}'"]; assertion --> assertion; end;
flowchart LR subgraph Structure block direction LR theory['structure'] --> NAME_TH([NAME_TH]); theory --> leftT; NAME_TH --> dot[':']; NAME_TH --> leftT; dot --> voc([NAME_V]); voc --> leftT["'{'"]; leftT --> rightT; leftT --> interpretation([Interpretation]); interpretation --> rightT["'}'"]; interpretation --> interpretation; end;

Well-formedness

  1. The Knowledge Base must have at least one vocabulary and one theory block.

  2. The Knowledge Base may contain other types of block, e.g., procedural blocks to perform reasoning tasks. These blocks are not part of this standard.

  3. If omitted, NAME_V (resp. NAME_TH) is assumed to be the string V (resp. T).

  4. The NAME_V in a theory (or structure) block must be the same as the NAME_V of a previous vocabulary block.

  5. When the Knowledge Base has several vocabulary (resp. theory or structure) blocks, two vocabulary (resp. theory or structure) blocks cannot have the same NAME_V (resp. NAME_TH).

Semantics

  1. A state of affairs is a static “mental world” that can be communicated by a set of descriptive sentences in natural language (e.g., in English). (A state of affairs is similar to a mental model in cognitive science [JL08])

  2. A knowledge base is a formal description of all the possible (or desirable, or acceptable) states of affairs in a problem domain.

  3. A vocabulary declares the symbols denoting important concepts in a problem domain. Each symbol has an informal meaning in natural language in the problem domain. There are 3 types of symbols: type, function and predicate symbols.

  4. A particular state of affairs is described by giving a total interpretation to every symbol. The set of these interpretations is a total structure. A structure is an abstraction of a state of affairs.

  5. A theory (over a vocabulary) is a set of assertions that are true in every model, i.e., in every structure that are possible (or desirable, or acceptable). A structure in which all assertions are true is a model of the theory.

  6. Many reasoning tasks involve only one vocabulary and theory, but some reasoning tasks, such as “determine if 2 theories are equivalent” require more.

  7. A structure block is a special kind of theory blocks that only contains interpretations of types and symbols. They typically contain observations about a state of affairs.

Example

    vocabulary {
        // here comes the declaration of types and symbols
    }

    theory {
        // here comes the definitions and axioms
    }

    structure {
        // here comes the interpretation of some symbols
    }

Type declaration

This section describes how a type is declared in the vocabulary.

Lexicon

Token

Pattern

Example

ACCESSOR

ID

BOOL

either 𝔹 or Bool

CONSTRUCTOR

ID

NAME_T

ID

NAME_I

ID or '[^']*'

‘John Doe’

Syntax

Declaration ← 'type' NAME_T [':=' TypeInterpretation] ;
  TypeInterpretation ← '{' NAME_I { ',' NAME_I } '}';
  TypeInterpretation ← 'constructed' 'from'
        '{' ConstructorDeclaration { ',' ConstructorDeclaration } '}';
    ConstructorDeclaration ← NAME_I;
    ConstructorDeclaration ← CONSTRUCTOR '(' [ACCESSOR ':' ] Type
            {',' [ACCESSOR ':' ] Type} ')';
      Type ← NAME_T | BOOL;
flowchart LR subgraph Declaration direction LR type['type'] --> NAME_T([NAME_T]); NAME_T --> endD{ }; NAME_T --> eq["':='"]; eq --> TypeInterpretation([TypeInterpretation]); TypeInterpretation --> endD; end;
flowchart LR subgraph TypeInterpretation direction LR eq{ } --> lb["'{'"]; lb --> NAME_I; NAME_I --> rb["'}'"]; rb --> endD{ }; NAME_I --> comma[',']; comma --> NAME_I([NAME_I]); eq --> constructed["'constructed'"]; constructed --> from["'from'"]; from --> lb2["'{'"]; lb2 --> constructorT([ConstructorDeclaration]); constructorT --> rb2["'}'"]; constructorT --> comma2["','"]; comma2 --> constructorT; rb2 --> endD; end;
flowchart LR subgraph ConstructorDeclaration direction LR start{ } --> NAME_I([NAME_I]); start --> constructorT; NAME_I --> endd; constructorT([CONSTRUCTOR]) --> lp["'('"]; lp --> ACCESSOR([ACCESSOR]); comma --> ACCESSOR; ACCESSOR --> colon["':'"]; colon --> type lp --> type([Type]); comma --> type; type --> comma["','"]; type --> rp["')'"]; rp --> endd{ }; end;
flowchart LR subgraph Type direction LR start{ } --> NAME_T([NAME_T]); start --> BOOL; NAME_T --> endT{ }; BOOL --> endT; end;

Well-formedness

  1. A NAME_T (resp. NAME_I, CONSTRUCTOR, ACCESSOR) can be declared only once. A NAME_T cannot conflict with another Type (e.g., Bool). A NAME_I cannot conflict with another Identifier.

  2. The 4 sets of Type, Identifier, CONSTRUCTOR and ACCESSOR strings must be disjoint.

  3. Constructors are not recursive: NAME_T occurring as argument of a CONSTRUCTOR must have been previously declared (relaxed in FO[Infinite]).

Semantics

  1. The domain of discourse is a set of objects (aka individuals) in the state of affairs.

  2. Types are disjoint subsets of the domain of discourse. The domain of discourse is the union of the types. All types are finite sets in FO[Core].

  3. A type interpretation gives a unique name to each element of the subset (UNA: Unique Name Axiom). Every element in the subset has a name (DCA: Domain Closure Axiom).

  4. A name can be an identifier or a compound identifier.

  5. A “direct” type declaration consists of a set of identifiers.

  6. A “constructed type” declaration consists of a set of constructor declarations. All the compound identifiers of the constructed type are obtained by applying each constructor in the declaration to each possible tuple of elements of their Type arguments (if any).

Examples

type Color := {red, blue, green}
type RGB := constructed from {RGB(Bool, Bool, Bool)}

red, blue and green are the 3 different Colors. There are only 3 Colors. RGB(true, false, false) is an element of type RGB. This type has \(2⨯2⨯2=8\) elements.

Function and Predicate declaration

This section describes how functions and predicates are declared in the vocabulary.

Lexicon

Token

Pattern

Example

ANNOT

\[[^\]]*\]

[This is an annotation]

NAME_S

ID

TIMES

*|⨯

TO

->|→

Syntax

  Declaration ← { ANNOT } NAME_S { ',' NAME_S } ':' Signature;
    Signature ← '(' [ Type { TIMES Type } ] ')' TO Type;
    Signature ←  Type { TIMES Type } TO Type;
flowchart LR subgraph Declaration direction LR begin{ } --> annotation([ANNOT]); begin --> NAME_S([NAME_S]); annotation --> annotation; annotation --> NAME_S; NAME_S --> comma["','"]; comma --> NAME_S; NAME_S --> colon["':'"]; colon --> Signature([Signature]); end;
flowchart LR subgraph Signature direction LR begin{ } --> leftP["'('"]; leftP --> rightP; leftP --> Type; Type --> rightP["')'"]; rightP --> to; Type --> comma2["TIMES"]; comma2 --> Type; to --> type2([Type]); begin --> Type2([Type]); Type2 --> to["TO"]; Type2 --> comma["TIMES"]; comma --> Type2; end;

Well-formedness

  1. A NAME_S can be declared only once. It cannot conflict with another (built-in) symbol (such as abs in FO[Int]).

  2. A NAME_T cannot occur in a Signature before it has been declared.

  3. The 5 sets of Type, Symbol, Identifier, CONSTRUCTOR and ACCESSOR strings must be disjoint.

Semantics

  1. This Declaration declares one (or more) function symbol and its type signature. The Types before TO specify the domain of the function; the Type after TO specify its range.

  2. A function whose range is BOOL is also called a predicate.

  3. Annotations do not have logic meaning, but can be parsed by a reasoning engine. They may be used to, e.g., specify the informal semantics of a symbol, for display to a user. Their use is not specified in this standard.

Examples

convex, equilateral : () → 𝔹
colorOf: Country → Color

[edge of a graph]
edge : Node ⨯ Node → Bool

Import

This section declares how declarations can be imported from a vocabulary in another.

Syntax

Declaration ← 'import' NAME_V;
flowchart LR subgraph Declaration direction LR import["'import'"] --> NAME_V([NAME_V]); end;

Well-formedness

  1. vocabulary NAME_V must have been declared previously in the knowledge base.

Semantics

  1. the declarations in the vocabulary named NAME_V are added to the vocabulary that contains the import declaration.

Axiom

This section describes how logic statements are added to a theory.

Lexicon

Token

Pattern

Example

AND

&|∧

EQUIVALENCE

<=>|⇔

IMPLICATION

=>|⇒

IN

in|∈

OR

\||∨

QUANTOR

[∀!∃?]

R_IMPLICATION

<=|⇐

UNARY

~|¬

VARIABLE

ID

Syntax

Assertion ← Axiom;
Axiom ← Expression '.';
Expression ← [ { ANNOT } QUANTOR Quantee {',' Quantee} ':' ] RImplication;
             Quantee ← VARIABLE {',' VARIABLE} IN Type;
    RImplication ← Equivalence [R_IMPLICATION Equivalence];
    Equivalence  ← Implication [EQUIVALENCE   Implication];
    Implication  ← Disjunction [IMPLICATION   Disjunction];
    Disjunction  ← Conjunction {OR            Conjunction};
    Conjunction  ← Unary       {AND           Unary};
    Unary        ← { UNARY }  Base;

    Base ← 'if' Expression 'then' Expression 'else' Expression;
    Base ← { ANNOT } QUANTOR Quantee {',' Quantee} ':' RImplication;
    Base ← Symbol '(' [Expression {',' Expression}] ')';
    Base ← Identifier | VARIABLE;
    Base ← { ANNOT } '(' Expression ')';

        Identifier ← 'true' | 'false' | NAME_I;
        Symbol ← NAME_S;
        Symbol ← CONSTRUCTOR | ACCESSOR | 'is_{CONSTRUCTOR}';

Here, 'is_{CONSTRUCTOR}' represents any string constructed from 'is_' and a CONSTRUCTOR, e.g., is_RGB.

flowchart LR subgraph Expression direction LR start{ } --> QUANTOR; start --> ANNOT([ANNOT]); ANNOT --> QUANTOR; QUANTOR --> Quantee3([Quantee]); Quantee3 --> comma3["','"]; comma3 --> Quantee3; Quantee3 --> colon3["':'"]; colon3 --> Expr6([RImplication]); start --> Expr6; Expr6 --> endB{ }; end;
flowchart LR subgraph Quantee direction LR VARIABLE([VARIABLE]) --> comma["','"]; comma --> VARIABLE2([VARIABLE]); VARIABLE2 --> comma; VARIABLE --> IN[IN]; VARIABLE2 --> IN; IN --> Type([Type]); end;
flowchart LR subgraph RImplication direction LR start{ } --> Equivalence([Equivalence]); Equivalence --> END{ }; Equivalence --> R_IMPLICATION; R_IMPLICATION --> Equivalence2([Equivalence]); Equivalence2 --> END; end;
flowchart LR subgraph Equivalence direction LR start{ } --> Implication([Implication]); Implication --> END{ }; Implication --> EQUIVALENCE; EQUIVALENCE --> Implication2([Implication]); Implication2 --> END; end;
flowchart LR subgraph Implication direction LR start{ } --> Disjunction([Disjunction]); Disjunction --> END{ }; Disjunction --> IMPLICATION; IMPLICATION --> Disjunction2([Disjunction]); Disjunction2 --> END; end;
flowchart LR subgraph Disjunction direction LR start{ } --> Conjunction([Conjunction]); Conjunction --> END{ }; Conjunction --> OR; OR --> Conjunction2([Conjunction]); Conjunction2 --> OR; Conjunction2 --> END; end;
flowchart LR subgraph Conjunction direction LR start{ } --> Unary([Unary]); Unary --> END{ }; Unary --> AND; AND --> Unary2([Unary]); Unary2 --> AND; Unary2 --> END; end;
flowchart LR subgraph Unary direction LR start{ } --> UNARY; UNARY --> UNARY; UNARY --> Base([Base]); start --> Base; end;
flowchart LR subgraph Base direction LR start{ } --> if["'if'"]; if --> Exp3([Expression]); Exp3 --> then["'then'"]; then --> Exp4([Expression]); Exp4 --> else["'else'"]; else --> Exp5([Expression]); Exp5 --> endB{ }; start --> QUANTOR; start --> ANNOT([ANNOT]); ANNOT --> QUANTOR; QUANTOR --> Quantee3([Quantee]); Quantee3 --> comma3["','"]; comma3 --> Quantee3; Quantee3 --> colon3["':'"]; colon3 --> Expr6([Expression]); Expr6 --> endB; start --> symbol([Symbol]); symbol --> lp3["'('"]; lp3 --> rp3; lp3 --> Exp7([Expression]); Exp7 --> comma7["','"]; comma7 --> Exp7; Exp7 --> rp3["')'"]; rp3 --> endB; start --> IDENTIFIER([Identifier]); IDENTIFIER --> endB; start --> VARIABLE([VARIABLE]); VARIABLE --> endB; start --> bl["'('"]; start --> ANNOT2([ANNOT]); ANNOT2 --> bl; bl --> Exp8([Expression]); Exp8 --> br["')'"]; br --> endB; end;

Well-formedness

  1. Each NAME_T, NAME_S strings must have been declared in the vocabulary. Each NAME_I, CONSTRUCTOR and ACCESSOR must have been declared before occurring in a Base.

  2. Each expression has a type based on the declarations in the vocabulary. An axiom must be a boolean expression. The elements of an expression must have the appropriate types, as specified in the symbol declarations or as required by the built-in connectives.

  3. Each variable must occur in the scope of a quantifier that declares it.

Semantics

  1. The expressions above have their usual mathematical / logic meaning. (See also the semantics of FO(Core) below)

  2. The production rules above define the precedence of the operators.

  3. An is_{CONSTRUCTOR} string denotes a unary predicate that says whether the argument was constructed with CONSTRUCTOR.

  4. When ACCESSOR is the name of the n-th argument of CONSTRUCTOR according to its declaration, it denotes a function that takes an object O created by CONSTRUCTOR, and returns the n-th argument that has been applied to the constructor to construct O. The occurrences of ACCESSOR in an expression must be properly guarded to ensure it is applied to appropriate arguments.

Examples

In ∀x,y T: p(x,y) f(f(x))=y., x and y are variables of type T.

Assuming type Color := {RGB{red: Bool, green: Bool, blue: Bool}}, is_RGB(RGB(true, false, false)) is true and red(RGB(true, false, false)) is true.

Symbol Interpretation

This section describes how the interpretation of a function or predicate is added to a theory or structure.

Syntax

Assertion ← Interpretation;
Interpretation ← NAME_T ':=' TypeInterpretation '.';
Interpretation ← NAME_S ':=' Value '.';
Interpretation ← NAME_S ':=' SymbolInterpretation '.';
  Value ← Identifier;
  Value ← CONSTRUCTOR [ '(' Value {',' Value } ')';
  SymbolInterpretation ← '{' TupleValue { ',' TupleValue } '}';
  SymbolInterpretation ← '{' TupleValue TO Value { ',' TupleValue TO Value} '}' [else];
    TupleValue ← Value;
    TupleValue ← '(' Value { ',' Value } ')';
  else ← 'else' Value;
flowchart LR subgraph Interpretation direction LR start{ } --> NAME_T([NAME_T]); NAME_T --> eq["':='"]; eq --> TypeInterpretation([TypeInterpretation]); start --> NAME_S([NAME_S]); NAME_S --> eq2["':='"]; eq2 --> Value([Value]); eq2 --> lp["'{'"]; lp --> Value1 --> comma["','"] --> Value1([Value]) --> rp["'}'"]; lp --> TValue2([TupleValue]) --> TO --> Value3([Value]) --> rp2["'}'"]; Value3 --> comma2["','"] --> TValue2; rp2 --> elseV['else'] --> Value2([Value]); TypeInterpretation --> dot['.']; Value --> dot; rp --> dot; rp2 --> dot; Value2 --> dot; end;
flowchart LR subgraph TupleValue direction LR start{ } --> Value([Value]); Value --> endV{ }; start --> lp["'('"]; lp --> Value1([Value]); Value1 --> rp["')'"]; Value1 --> comma["','"]; comma --> Value1; rp --> endV; end;
flowchart LR subgraph Value direction LR start{ } --> IDENTIFIER([Identifier]); start --> const([CONSTRUCTOR]); IDENTIFIER --> endV{ }; const --> lp["'('"]; lp --> Val([Value]); Val --> rp["')'"]; rp --> endV; Val --> comma["','"]; comma --> Val; end;

Well-formedness

  1. A NAME_T or NAME_S can be interpreted only once.

  2. All types must be interpreted, in the vocabulary or in a theory/structure.

  3. Each NAME_I, CONSTRUCTOR and ACCESSOR must have been declared before occurring in a Value.

  4. The interpretation can be a single value only for nullary predicates or functions (i.e., with an arity of 0).

  5. The number and type of values in an interpretation must match the type signature of the NAME_S being interpreted.

  6. The number and types of values in a compound identifier must match the type signature of the CONSTRUCTOR.

  7. The TO element is mandatory in function interpretations, and prohibited in predicate interpretations (relaxed in FO[Sugar]).

Semantics

  1. These assertions define the interpretation of types, predicates and functions.

  2. For a type, the assertion has the same semantics as in a type declaration

  3. For a predicate, the set of TupleValue is the set of values for which the predicate is true; the predicate is false for any other TupleValue; for nullary predicate, the unique Value can be true or false.

  4. For a function, the assertion maps tuple of arguments to their value. The value after else is the value given to the function for tuples of arguments that are not in the enumeration. For nullary symbols, the interpretation can be a unique value.

Examples

Color := {red, blue, green}.
node := {A, B, C}.
colorOf := {A -> red, B -> blue} else green.
edge := {(A,B), (B,B)}.
convex := true.

FO(Core) abstract language

This section contains the formal theory of the FO(Core) abstract language.

The translation between the abstract language and the concrete language is not provided. However, corresponding concepts in the abstract and the concrete language are denoted by the same words: this should allow the reader to establish the correspondence by himself.

\(T\) is a set of type-symbols. It contains type-symbol \(𝔹\).

A n-signature is a (n+1)-tuple of type-symbols, noted \(T_1 ⨯ \dots ⨯ T_n → T\), where \(0 \leq n\). (A 0-signature is noted \(() → T\))

A vocabulary \(Σ\) is a set of (symbol \(σ\), n-signature) pairs.

A typing function \(γ\) is a function that maps variables to type-symbols. For a given \(γ\), we define \(γ[x : T]\) to be the function \(γ′\) identical to \(γ\) except that \(γ′(x) = T\).

The type of string \(φ\) (over \(Σ\)) given a typing function \(γ\), noted \(τ(φ, γ)\), is a type-symbol partially defined by induction as follows (terminal symbols are underlined for clarity):

\(φ\)

\(τ(φ, γ)\)

if

\(\underline{true}\)

\(𝔹\)

\(\underline{false}\)

\(𝔹\)

\(x\)

\(γ(x)\)

x is a variable

\(σ\underline{(}t_1\underline{,} .. \underline{,}t_n\underline{)}\)

\(T\)

\((σ,T_1 ⨯ \dots ⨯ T_n → T) \in Σ\)
and \(\forall i \in [1,n]: τ(t_i,γ)=T_i\)

\(φ\underline{∨}ψ\)

\(𝔹\)

\(τ(φ,γ)=𝔹\) and \(τ(ψ,γ)=𝔹\)

\(\underline{¬}φ\)

\(𝔹\)

\(τ(φ,γ)=𝔹\)

\(\underline{∃} x \underline{∈} T\underline{:} φ\)

\(𝔹\)

\(x\) is a variable and \(τ(φ,γ[x:T])=𝔹\)

\(t_1\underline{=}t_2\)

\(𝔹\)

\(τ(t_1,γ)=τ(t_2,γ)\)

\(\mathbf{\underline{if}~} φ \mathbf{~\underline{then}~} t_1 \mathbf{~\underline{else}~} t_2\)

\(T\)

\(τ(φ,γ)=𝔹\) and \(τ(t_1,γ)=T=τ(t_2,γ)\)

otherwise

undefined

Let \(∅\) be the typing function with empty domain. We say that \(φ\) is a well-formed formula of type \(T\) over \(Σ\) if \(τ(φ,∅)=T\). A sentence is a well-formed formula of type \(𝔹\).

This table shows how to extend the syntax with convenient notations:

Convenient notation

Equivalent formula

\(φ\underline{∧}ψ\)

\(¬(¬φ∨¬ψ)\)

\(φ\underline{⇒}ψ\)

\(¬φ∨ψ\)

\(φ\underline{⇐}ψ\)

\(φ∨¬ψ\)

\(φ\underline{⇔}ψ\)

\((φ∧ψ)∨(¬φ∧¬ψ)\)

\(\underline{∀}x \underline{∈} T\underline{:}φ\)

\(¬∃x∈T:¬φ\)

A (total) structure \(𝓘\) over \(Σ\) consists of :

  • an object domain \(D\) containing \(𝔹^𝓘\), the set of booleans;

  • a mapping of type-symbols \(T\) to disjoint subsets \(T^𝓘\) of \(D\); \(D\) is the union of all \(T^𝓘\);

  • a (total) mapping from symbols \(σ\) with n-signature \(T_1 ⨯ \dots ⨯ T_n → T\) to (total) functions from \(T_1^𝓘 ⨯ \dots ⨯ T_n^𝓘\) to \(T^𝓘\).

Note: Identifier and CONSTRUCTOR strings are function symbols whose interpretation have the following properties:

  1. All well-formed ground terms of type \(T\) built exclusively with them uniquely identify an element of \(T^𝓘\).

  2. Every element of \(T^𝓘\) is uniquely identified by a well-formed ground term of type \(T\) built exclusively with them.

We define a variable assignment \(ν\) as a mapping of variables to elements in \(D\). A variable assignment extended so that the mapping of \(x\) is \(d\) is denoted \(ν[x : d]\).

The value of formula \(φ\) in \((𝓘,ν)\), denoted \(⟦t⟧^I_ν = v\), is an element of \(D\) partially defined by induction as follows:

\(φ\)

\(⟦φ⟧^I_ν\)

if

\(\underline{true}\)

\(true\)

\(\underline{false}\)

\(false\)

\(x\)

\(ν(x)\)

x is a variable in the domain of \(ν\)

\(σ\underline{(}t_1\underline{,} .. \underline{,}t_n\underline{)}\)

\(σ^𝓘(⟦t_1⟧^I_ν, .. ,⟦t_n⟧^I_ν)\)

\((σ,T_1 ⨯ \dots ⨯ T_n → T) \in Σ\)
and \(\forall i \in [1,n]: ⟦t_i⟧^I_ν\) is defined

\(φ\underline{∨}ψ\)

\(false\)

\(⟦φ⟧^I_ν\) is defined and false

\(φ\underline{∨}ψ\)

\(⟦φ⟧^I_ν ∨ ⟦ψ⟧^I_ν\)

\(⟦φ⟧^I_ν\) and \(⟦ψ⟧^I_ν\) are defined

\(\underline{¬}φ\)

\(¬⟦φ⟧^I_ν\)

\(⟦φ⟧^I_ν\) is defined

\(\underline{∃} x \underline{∈} T\underline{:} φ\)

\(∃d ∈ T^I : ⟦φ⟧^I_ν[x:d]\)

\(⟦φ⟧^I_ν[x:d]\) is defined for every d in \(T^I\)

\(t_1\underline{=}t_2\)

\(⟦t_1⟧^I_ν = ⟦t_2⟧^I_ν\)

\(⟦t_1⟧^I_ν\) and \(⟦t_2⟧^I_ν\) are defined

\(\mathbf{\underline{if}~} φ \mathbf{~\underline{then}~} t_1 \mathbf{~\underline{else}~} t_2\)

\(⟦t_1⟧^I_ν\)

\(⟦φ⟧^I_ν=true\) and \(⟦t_1⟧^I_ν\) is defined

\(\mathbf{\underline{if}~} φ \mathbf{~\underline{then}~} t_1 \mathbf{~\underline{else}~} t_2\)

\(⟦t_2⟧^I_ν\)

\(⟦φ⟧^I_ν=false\) and \(⟦t_2⟧^I_ν\) is defined

otherwise

undefined

Notice that \(φ\underline{∨}ψ\) and \(\mathbf{\underline{if}~} φ \mathbf{~\underline{then}~} t_1 \mathbf{~\underline{else}~} t_2\) have non-strict semantics.

We say a total structure \(𝓘\) satisfies sentence \(φ\) iff \(⟦φ⟧^I_ν=\mathit{true}\) for any \(ν\). This is denoted \(𝓘 ⊧ φ\). Structures \(𝓘\) that satisfy \(φ\) are called models of \(φ\).