BOL -> SFOL semantics: translation for R* insufficient?

Master / Vertiefung Wissensrepräsentation und -Verarbeitung
1

Disclaimer: Dieser Thread wurde aus dem alten Forum importiert. Daher werden eventuell nicht alle Formatierungen richtig angezeigt. Der ursprüngliche Thread beginnt im zweiten Post dieses Threads.

2

BOL → SFOL semantics: translation for R insufficient?*
The BOL → SFOL semantics translates occurrences of R* (for possibly complex R) non-compositionally as described below:

But what prevents a (set-theoretic) model of the generated SFOL theory from setting C_R to the trivial full relation?
Concretely, if M is the model, [m]M[[ι]][/m] its universe for the sort ι, then [m]M[[C_R]] = M[[ι]] x M[[ι]][/m] is perfectly acceptable and does not contradict the generated axioms.

Indeed, Wikipedia says at https://en.wikipedia.org/w/index.php?title=Transitive_closure&oldid=945383137#In_logic_and_computational_complexity: [quote]one cannot write a formula using predicate symbols R and T that will be satisfied in any model if and only if T is the transitive closure of R[/quote]

Does this mean the translation BOL → SFOL is actually “wrong” (i.e., not as intended)?

3

Reformulating your criticism, why does the axiomatization only require that C_R is some transitive relation bigger than R?
To be the transitive closure, shouldn’t there be axioms that make sure it is the smallest such relation?

In some situations, it would indeed be helpful to do that.
It would in particular ensure that C_R is the transitive closure in every model.
But we would need a stronger logic for that, namely one in which we can quantify over all relations P - then we can add axiom like
forall P. (R subset P and transitive(P)) => C_R subset P

But we do not need that because the semantics of an SFOL theory is not determined by what can be true in some model.
It is determined by what is true in every model (or equivalently, by what is derivable in the calculus).

Because the model in which C_R is the transitive closure of R is among all the models in which C_R is a transitive extension of R, the semantics can at most prove properties that hold about the transitive closure.

1 „Gefällt mir“