Guarded logic

Last updated

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

Contents

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 Y∪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 a 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`.

Related Research Articles

First-order logic—also called predicate logic, predicate calculus, quantificational logic—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantified variables over non-logical objects, and allows the use of sentences that contain variables, so that rather than propositions such as "Socrates is a man", one can have expressions in the form "there exists x such that x is Socrates and x is a man", where "there exists" is a quantifier, while x is a variable. This distinguishes it from propositional logic, which does not use quantifiers or relations; in this sense, propositional logic is the foundation of first-order logic.

<span class="mw-page-title-main">Original proof of Gödel's completeness theorem</span>

The proof of Gödel's completeness theorem given by Kurt Gödel in his doctoral dissertation of 1929 is not easy to read today; it uses concepts and formalisms that are no longer used and terminology that is often obscure. The version given below attempts to represent all the steps in the proof and all the important ideas faithfully, while restating the proof in the modern language of mathematical logic. This outline should not be considered a rigorous proof of the theorem.

In mathematics, a finitary relation over a sequence of sets X1, ..., Xn is a subset of the Cartesian product X1 × ... × Xn; that is, it is a set of n-tuples (x1, ..., xn), each being a sequence of elements xi in the corresponding Xi. Typically, the relation describes a possible connection between the elements of an n-tuple. For example, the relation "x is divisible by y and z" consists of the set of 3-tuples such that when substituted to x, y and z, respectively, make the sentence true.

The relational model (RM) is an approach to managing data using a structure and language consistent with first-order predicate logic, first described in 1969 by English computer scientist Edgar F. Codd, where all data is represented in terms of tuples, grouped into relations. A database organized in terms of the relational model is a relational database.

In logic and mathematics, second-order logic is an extension of first-order logic, which itself is an extension of propositional logic. Second-order logic is in turn extended by higher-order logic and type theory.

In the foundations of mathematics, von Neumann–Bernays–Gödel set theory (NBG) is an axiomatic set theory that is a conservative extension of Zermelo–Fraenkel–choice set theory (ZFC). NBG introduces the notion of class, which is a collection of sets defined by a formula whose quantifiers range only over sets. NBG can define classes that are larger than sets, such as the class of all sets and the class of all ordinals. Morse–Kelley set theory (MK) allows classes to be defined by formulas whose quantifiers range over classes. NBG is finitely axiomatizable, while ZFC and MK are not.

Descriptive complexity is a branch of computational complexity theory and of finite model theory that characterizes complexity classes by the type of logic needed to express the languages in them. For example, PH, the union of all complexity classes in the polynomial hierarchy, is precisely the class of languages expressible by statements of second-order logic. This connection between complexity and the logic of finite structures allows results to be transferred easily from one area to the other, facilitating new proof methods and providing additional evidence that the main complexity classes are somehow "natural" and not tied to the specific abstract machines used to define them.

Finite model theory is a subarea of model theory. Model theory is the branch of logic which deals with the relation between a formal language (syntax) and its interpretations (semantics). Finite model theory is a restriction of model theory to interpretations on finite structures, which have a finite universe.

Independence-friendly logic is an extension of classical first-order logic (FOL) by means of slashed quantifiers of the form and , where is a finite set of variables. The intended reading of is "there is a which is functionally independent from the variables in ". IF logic allows one to express more general patterns of dependence between variables than those which are implicit in first-order logic. This greater level of generality leads to an actual increase in expressive power; the set of IF sentences can characterize the same classes of structures as existential second-order logic.

In mathematical logic, an atomic formula is a formula with no deeper propositional structure, that is, a formula that contains no logical connectives or equivalently a formula that has no strict subformulas. Atoms are thus the simplest well-formed formulas of the logic. Compound formulas are formed by combining the atomic formulas using the logical connectives.

An approach to the foundations of mathematics that is of relatively recent origin, Scott–Potter set theory is a collection of nested axiomatic set theories set out by the philosopher Michael Potter, building on earlier work by the mathematician Dana Scott and the philosopher George Boolos.

In logic, a modal companion of a superintuitionistic (intermediate) logic L is a normal modal logic that interprets L by a certain canonical translation, described below. Modal companions share various properties of the original intermediate logic, which enables to study intermediate logics using tools developed for modal logic.

In mathematical logic, a Lindström quantifier is a generalized polyadic quantifier. Lindström quantifiers generalize first-order quantifiers, such as the existential quantifier, the universal quantifier, and the counting quantifiers. They were introduced by Per Lindström in 1966. They were later studied for their applications in logic in computer science and database query languages.

In database theory, a conjunctive query is a restricted form of first-order queries using the logical conjunction operator. Many first-order queries can be written as conjunctive queries. In particular, a large part of queries issued on relational databases can be expressed in this way. Conjunctive queries also have a number of desirable theoretical properties that larger classes of queries do not share.

An interpretation is an assignment of meaning to the symbols of a formal language. Many formal languages used in mathematics, logic, and theoretical computer science are defined in solely syntactic terms, and as such do not have any meaning until they are given some interpretation. The general study of interpretations of formal languages is called formal semantics.

In mathematical logic the theory of pure equality is a first-order theory. It has a signature consisting of only the equality relation symbol, and includes no non-logical axioms at all.

In logic, a quantifier is an operator that specifies how many individuals in the domain of discourse satisfy an open formula. For instance, the universal quantifier in the first order formula expresses that everything in the domain satisfies the property denoted by . On the other hand, the existential quantifier in the formula expresses that there exists something in the domain which satisfies that property. A formula where a quantifier takes widest scope is called a quantified formula. A quantified formula must contain a bound variable and a subformula specifying a property of the referent of that variable.

In mathematical logic, the spectrum of a sentence is the set of natural numbers occurring as the size of a finite model in which a given sentence is true. By a result in descriptive complexity, a set of natural numbers is a spectrum if and only if it can be recognized in non-deterministic exponential time.

In mathematical logic, fixed-point logics are extensions of classical predicate logic that have been introduced to express recursion. Their development has been motivated by descriptive complexity theory and their relationship to database query languages, in particular to Datalog.

In mathematics, S2S is the monadic second order theory with two successors. It is one of the most expressive natural decidable theories known, with many decidable theories interpretable in S2S. Its decidability was proved by Rabin in 1969.

References

  1. ↑ "Formal modeling and analysis of timed system". International Conference on Formal Modelling and Analysis of Timed Systems No4. Paris, France. September 25–27, 2006.
  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). pp. 26–48. Retrieved 15 May 2014.
  5. ↑ "Guarded Logics: Algorithms and Bisimulation" (PDF). p. 25. Retrieved 15 May 2014.
This page is based on this Wikipedia article
Text is available under the CC BY-SA 4.0 license; additional terms may apply.
Images, videos and audio are available under their respective licenses.