We describe recent developments in the theory of real recursive functions, as discovered by the speaker in collaboration with José Félix Costa and Jerzy Mycka. The class of real recursive functions is the smallest class of partial real-valued vector functions containing the functions 1, -1, 0, and the projections, and closed under composition, differential recursion and infinite limits. Restrictions of this inductive scheme have been previously shown, in this seminar, to correspond to the computable functions over R. We will study the most general and unrestricted form of this inductive scheme by: (1) giving a general introduction; (2) describing a few fundamental results, of which some are new; and, ultimately, (3) showing that real recursive functions have an exact correspondence with the analytical hierarchy of (second-order) predicates.
The concept of logical consequence is one of the most central concepts of logic. It naturally involves de idea of truth preservation. Nonetheless, another adequacy criterion could be devised and its development would still remain in the central area of logical matters. We are thinking in the concept of falsity preservation. In our exposition, we want to go through a few logical systems in which falsity preservation is the adequacy criterion adopted. As we pretend to show quickly, there is a huge amount of systems to which this criterion can be applied such that some traditional remarkable logical metatheorems still hold. We will use examples of natural deduction rules to present our ideas in an intuitive fashion. These rules are easily related to axiomatic systems and also sequent calculi.
An algorithm is outlined for deciding the correctness of bounded space and time imperative programs, using linear algebra techniques encoded in the theory of real closed fields. The approach is shown to be feasible for classical, probabilistic and quantum programs. Joint work with P. Mateus, J. Ramos and C. Sernadas.
What is a logic? What are all the possible logics? Why and how can we consider degenerated cases of logics as logics? Under which operations should the class of logics be closed? We will try to give answers to these questions in the spirit of universal logic.
The Logics of Formal Inconsistency are paraconsistent logics which internalize the notions of consistency and inconsistency by meansof connectives of their language. Based on that idea, we propose several deontic systems in which contradictory obligations are allowed, without trivializing the system. Thus, from conflicting obligations $O(A)$ and $O(-A)$ just can be derived that the sentence $A$ is deontically inconsistent. This avoids the logic collapse, and, on the other hand, this allows to "repair" or to refine the given information set. The novel systems introduce new deontic operators of "deontic consistency" and "deontic inconsistency". This approach can be used for analyzing paradoxes based on contrary-to-duty obligations. This is a joint work with Newton Peron.
In this lecture we compare three types of analogies based on generalizations and their instantiations:
Generalizations w.r.t. invariant parts of proofs (e.g. graphs of rule applications etc);
Generalizations w.r.t. to an underlying meaning.(Here proofs and calculations are considered as trees of formal expressions. We analyze the well known calculation of Euler demonstrating that the 5th fermat number is compound.)
3. Generalizations w.r.t. the premises of a proof (This type of analogies is especially important for juridical reasoning.).
Many algorithms have been proposed to date for the problem of finding biologically significant motifs in promoter regions. They can be classified into two large families: combinatorial methods and probabilistic methods. Probabilistic methods have been used more extensively, since their output is easier to interpret. Combinatorial methods have the potential to identify hard to detect motifs, but their output is much harder to interpret, since it may consist of hundreds or thousands of motifs. In this work, we propose a method that processes the output of combinatorial motif finders in order to find groups of motifs that represent variations of the same motif, thus reducing the output to a manageable size. This processing is done by building a graph that represents the co-occurrences of motifs, and finding communities in this graph. We show that this innovative approach leads to a method that is as easy to use as a probabilistic motif finder, and as sensitive to low quorum motifs as a combinatorial motif finder. The method was integrated with two combinatorial motif finders, and made available on the Web.
It is well known that interleaving presentations is at the heart of fibring, as shown by the mechanism of fibring languages and deduction systems. This idea is abstractly introduced at the level of a suitably general notion of graph. Such graphs are used to present languages, interpretation structures and deduction systems in a uniform way. The induced semantics of fibring is very simple and avoids the collapsing problem. Transference results are also easier to establish. Joint work with A. Sernadas, J. Rasga and M. Coniglio.
In this talk I will explain the new perspective given by universal logic, from the mathematical and philosophical point of views and I will also make some comments regarding the historical development of logic and its connection with other sciences.
In general, by fibring two or more fragments of a given logic, the resulting logic is weaker than the original one, because some important meta-properties of the connectives are lost after the combination process. The lack of such meta-properties avoids the creation of some interactions between conectives from its combination (for instance, distributivity between conjuction and disjunction). In this talk, the question of recovering a logic system by combining fragments of it will be addressed. Specifically, categories of multiple-conclusion consequence relations and sequent calculi will be introduced in such a manner that, in several cases, a logic can be recovered by fibring (in these categories) its fragments. This process is called meta-fibring. The key feature of these categories is a notion of morphism stronger than usual, which preserve several meta-properties of the consequence relations. Soundness and completeness preservation by meta-fibring (wrt algebraic semantics) are obtained.
For a logical sentence $\varphi$, $\mu_x(\varphi)$ denotes the probability that a random model of size $n$ in $N$ satisfies $\varphi$. A logic $L$ is said to admit weak almost everywhere quantifier elimination (w.a.e.q.e.) iff for every formula $\varphi(x)$ in $L$, there is a quantifier free formula $\theta(x)$ such that: $\lim_x\mu_x[\forall x(\varphi(x)\leftrightarrow\theta(x))]=1]$. In relational vocabularies, w.a.e.q.e. implies that $L$ has a $0-1$ law, i.e. for each sentence $\varphi$ of the logic, $\lim_x\mu_x[\varphi] = 0$ or $1$.
It is well known that first order logic (as well as the infinitary logic $L^{\infty}_{\infty\omega}$ with finitely many variables) admits AEQE with the uniform probability on the set of models of size $n$. This subsumes many partial results such as the $0-1$ law for the logic with fixed point operator.
An extension of this result sometimes holds for certain logics with generalized quantifiers. A case of interest are the probability quantifiers (introduced by H.J.Keisler), e.g. $(\exists^{\geq 1/2}x)$, which says “ for at least ½ of all tuples $x$”. This logic in general has no $0-1$ law, e.g. $\lim_x\mu_x[(\exists^{\geq 1/2}x E(x,x))] = 1/2$. Also, $\lim_x\mu_x[\exists s((\exists^{\geq 1/2}y) E(x,y)\wedge(\exists^{\geq 1/2}y)\neg E(x,y))] = 1/2$ can be shown not to exist. The problem here stems from the fact that the threshold ½ is critical for the quantified formula.
Thus, we needed to extract a non-critical fragment of the probability logic that guarantees both w.a.e.q.e. and a $0-1$ law. We also allowed the following two set of parameters to vary with $n$ ($=$ the size of the model), and discovered a nice interplay between them:
The measure on the set of models of size $n$ will be generated by independent atomic probabilities $p R$ for each predicate symbol $R$, and $p R$ depends on $n$.
The ratio $r$ in $(\exists^{\geq r}x)$ will also be allowed to depend on $n$, thus dealing with general monotone numerical quantifiers.
Finally, we carried over these results to a natural non-critical fragment of the infinitary probability logic.
(This is a joint work with Prof. H. Jerome Keisler, University of Wisconsin-Madison)
Probabilistic finite automata as acceptors for languages over finite words have been studied by many researchers. In this talk, we discuss probabilistic automata for recognizing languages over infinite words. The idea is to resolve the choices in a nondeterministic omega-automaton by probabilities and to require positive probabilities for the accepting runs. Surprisingly, probabilistic Buechi automata are more expressive than non-deterministic omega-automata. However, a certain subclass of probabilistic Buechi automata can be identified that has exactly the power of omega-regular languages. Concerning the efficiency, probabilistic $\omega$-automata are not comparable with their nondeterministic counterparts. There are examples of omega-regular languages that have probabilistic Buechi automata of polynomial size, while any nondeterministic omega-automata with Streett, Rabin or Buechi acceptance is of exponential size. The talk will introduce the formal notion of probabilistic automata with Buechi and other acceptance conditions and discuss some basic properties, such as expressiveness, efficiency, composition operations and decision problems.
A new technique is presented for proving that a consequence system enjoys Craig interpolation or Maehara interpolation based on the fact that these properties hold in another consequence system. This technique is based on the existence of a back and forth translation satisfying some properties between the consequence systems. Some examples of translations satisfying those properties are described. Namely a translation between the global/local consequence systems induced by fragments of linear logic, and a new translation between the global consequence systems induced by full Lambek calculus and linear logic, mixing features of a Kiriyama-Ono style translation with features of a Kolmogorov-Gentzen-Gödel style translation. These translations establish a strong relationship between the logics involved and are used to obtain new results about whether Craig interpolation and Maehara interpolation hold in that logics. This talk reports on joint work with C. Sernadas and W. A. Carnielli.
In the research of the relationship between the symbolic and the computational view of cryptography, a recent approach uses static equivalence from cryptographic pi calculi as a notion of symbolic indistinguishability. Previous work has shown that this yields the soundness of natural interpretations of some interesting equational theories, such as certain cryptographic operations and a theory of XOR. However, we argue that static equivalence is too coarse to allow sound interpretations of many natural and useful equational theories. We illustrate this with several explicit examples in which static equivalence fails to work. To fix the problem, we propose a notion of symbolic indistinguishability that is more flexible than static equivalence. We provide general results, and then discuss how this new notion works for the explicit examples where static equivalence fails to ensure soundness. Joint work with P. Mohassel and T. Stegers.
The functions of Computable Analysis are defined by enhancing the capacities of normal Turing Machines to deal with real number inputs. We consider characterizations of these functions using function algebras, known as Real Recursive Functions. I will discuss the basic background, then discuss some recent characterizations of Computable Analysis, and then discuss our new characterization using a simpler function algebra. Our proof is quite different from those of others, using our earlier general techniques: Rather than directly showing that the function algebra can simulate a Turing Machine, we relate the two classes of functions using a series of intermediate classes of functions, via our notion of "approximation". (Joint work with Manuel L. Campagnolo)
In this talk we address several properties of the Exogenous Probabilistic Propositional Logic (EPPL) with the purpose of introducing a temporal version - Exogenous Probabilistic Linear Temporal Logic (EPLTL). In detail, we give a small model theorem for EPPL and present a polynomial-space algorithm for the SAT problem of both EPPL and EPLTL. We also show that the model-checking problem of EPLTL is in PSPACE. Finally, we provide a (weakly) complete calculus for EPLTL. We conclude the talk by pointing out future work and open problems that will be pursued with C. Baier at TU. Dresden. Joint work with P. Mateus.