Guarded logic

Guarded logic is a choice set of dynamic logic involved in choices, where outcomes are limited.

A simple example of guarded logic is as follows: if X is true, then Y, else Z can be expressed in dynamic logic as (X?;Y)∪(~X?;Z). This shows a guarded logical choice: if X holds, then X?;Y is equal to Y, and ~X?;Z is blocked, and a ∪block is also equal to Y. Hence, when X is true, the primary performer of the action can only take the Y branch, and when false the Z branch.^[1]

A real-world example is the idea of paradox: something cannot be both true and false. A guarded logical choice is one where any change in true affects all decisions made down the line.^[2]

History

Before the use of guarded logic there were two major terms used to interpret modal logic. Mathematical logic and database theory (Artificial Intelligence) were first-order predicate logic. Both terms found sub-classes of first-class logic and efficiently used in solvable languages which can be used for research. But neither could explain powerful fixed-point extensions to modal style logics.

Later Moshe Y. Vardi^[3] made a conjecture that a tree model would work for many modal style logics. The guarded fragment of first-order logic was first introduced by Hajnal Andréka, István Németi and Johan Van Benthem in their article Modal languages and bounded fragments of predicate logic. They successfully transferred key properties of description, modal, and temporal logic to predicate logic. It was found that the robust decidability of guarded logic could be generalized with a tree model property. The tree model can also be a strong indication that guarded logic extends modal framework which retains the basics of modal logics.

Modal logics are generally characterized by invariances under bisimulation. It also so happens that invariance under bisimulation is the root of tree model property which helps towards defining automata theory.

Types of Guarded Logic

Within Guarded Logic there exists numerous guarded objects. The first being guarded fragment which are first-order logic of modal logic. Guarded fragments generalize modal quantification through finding relative patterns of quantification. The syntax used to denote guarded fragment is GF. Another object is guarded fixed point logic denoted μGF naturally extends guarded fragment from fixed points of least to greatest. Guarded bisimulations are objects which when analyzing guarded logic. All relations in a slightly modified standard relational algebra with guarded bisimulation and first-order definable are known as guarded relational algebra. This is denoted using GRA.

Along with first-order guarded logic objects, there are objects of second-order guarded logic. It is known as Guarded Second-Order Logic and denoted GSO. Similar to second-order logic, guarded second-order logic quantifies whose range over guarded relations restrict it semantically. This is different from second-order logic which the range is restricted over arbitrary relations. ^[4]

Definitions of Guarded Logic

Let B be a relational structure with universe B and vocabulary τ.

i) A set X ⊆ B is guarded in B if there exists a ground atom α(b_1, ..., b_k) in B such that X = {b_1, ..., b_k}.

ii) A τ-structure A, in particular a substructure A ⊆ B, is guarded if its universe is a guarded set in A (in B).

iii) A tuple (b_1, ..., b_n) ∈ B^n is guarded in B if {b_1, ..., b_n} ⊆ X for some guarded set X ⊆ B.

iv) A tuple (b_1, ..., b_k) ∈ B^k is a guarded list in B if its components are pairwise distinct and {b_1, ..., b_k} is a guarded set. The empty list is taken to be a guarded list.

v) A relation X ⊆ B^n is guarded if it only consists of guarded tuples.^[5]

Guarded Bisimulation

A guarded bisimulation between two τ-structures A and B is an non-empty set I of finite partial isomorphic f: X → Y from A to B such that the back and forth conditions are satisfied.

Back: For every f: X → Y in I and for every guarded set Y` ⊆ B, there exists a partial isomorphic g: X` → Y` in I such that f^-1 and g^-1 agree on Y ∩ Y`.

Forth For every f: X → Y in I and for every guarded set X` ⊆ A, there exists a partial isomorphic g: X` → Y` in I such that f and g agree on X ∩ X`.

References

1. "International Conference on Formal Modelling and Analysis of Timed Systems No4". Paris, France. September 25–27, 2006. |contribution= ignored (help)
2. Nieuwenhuis, Robert; Andrei Voronkov (2001). Logic for Programming, Artificial Intelligence, and Reasoning. Springer. pp. 88–89. ISBN 3-540-42957-3.
3. Vardi, Moshe (1998). Reasoning about the Past with Two-Way Automata (PDF).
4. "Guarded Logics: Algorithms and Bisimulation" (PDF). p. 26 - 48. Retrieved 15 May 2014.
5. "Guarded Logics: Algorithms and Bisimulation" (PDF). p. 25. Retrieved 15 May 2014.