# FO[PF]¶

FO[PF] extends FO[Sugar] to allow the use of partial functions (including partial predicates),
i.e., n-ary functions that are not totally defined over the cross-product of their argument types, `T1 ⨯ ... ⨯ Tn`

.

It introduces “unary predicates in type signature” and partial `Interpretation`

s.

## Unary predicates in type signature¶

This section describes how unary predicates can be used to specify the domain and range of partial functions.

**Syntax**

FO[PF] adds this production rule:

```
Type ← NAME_S;
```

**Well-formedness condition**

A

`NAME_S`

cannot be used as a`Type`

before it has been declared as a**unary predicate**symbol. This prevents loops in the subtype-of relation.A

`NAME_S`

cannot be used as a`Type`

in a`ConstructorDeclaration`

.(Well-guardedness) Logic formulas in a theory must be

*well-guarded*to ensure that the value of functions outside of their domain has no influence on the truth value of the theory. This can be achieved by using binary quantification and the non-strict (aka asymmetric) interpretation of the logic connectives in FO[Core] (including`if.. then..else`

).

**Semantics**

A unary predicate `P`

with signature `T → Bool`

denotes a subset \(P^I\) of \(T^I\) in structure \(I\).
A unary predicate `Q`

with signature `P → Bool`

denotes a subset \(Q^I\) of \(P^I\).
A n-ary predicate `R`

with signature `T1 ⨯ ... ⨯ Tn → Bool`

(where any `Ti`

can be a unary predicate)
denotes a subset \(R^I\) of \(T_1^I ⨯ ... ⨯ T_n^I\).

Thanks to the acyclicity of the subtype-of relation, a predicate `P`

always denotes a subset of a cross-product of type(s).
This cross-product is determined by (recursively) looking up the signature of `P`

.

A function `f`

with signature `P → Q`

denotes a *total* function from the set \(P^I\) to the set \(Q^I\).
The function has no value outside of \(P^I\).
A function `f`

with signature `T1 ⨯ ... ⨯ Tn → T`

(where `T`

and any `Ti`

can be a unary predicate)
denotes a *total* function from the set \(T_1^I ⨯ ... ⨯ T_n^I\) to the set \(T^I\).

(For FO[ID]) A definition of `f`

must define a value in the range of `f`

for all tuples of arguments in the domain of `f`

.

**Example**

```
vocabulary {
type LivingBeing:= { Bob, Alice, Tom, Garfield, Kermit }
person : LivingBeing → Bool
married : person → Bool
spouse: married → married
}
```

## Interpretations¶

This section discusses the (possibly partial) interpretation of partial functions.

**Syntax**

(no change)

**Well-formedness condition**

(Partial predicate) Unlike in FO[Core], the

`Interpretation`

of a predicate`p`

may use the`→`

element, followed by`true`

or`false`

. When it uses the`→`

element, it must use it for every`TupleValue`

, and it may also use the`else`

clause.The

`Value`

in the`Interpretation`

of a symbol`σ`

must be in the domain and range of`σ`

. The`Interpretation`

of`σ`

must be total over its domain. These conditions are checked at the syntax level when the`Interpretation`

of the domain and/or range of`σ`

is explicitly and totally given.

**Semantics**

If the `Interpretation`

of `σ`

is total and has no `else`

part, it also specifies the interpretation of the domain of `σ`

.

**Example**

```
vocabulary {
type LivingBeing:= { Bob, Alice, Tom, Garfield, Kermit }
person : LivingBeing → Bool
married : person → Bool
spouse: married → married
}
theory {
person := { Alice, Bob, Tom }
spouse := { Alice → Bob; Bob → Alice }
}
```

This theory implies that `Alice`

and `Bob`

are the only `married`

persons.