Failure of completeness properties of intuitionistic predicate logic for constructive models
Fatou's Lemma and the Lebesgue's Convergence Theorem
In this article we prove the Fatou's Lemma and Lebesgue's Convergence Theorem [10].MML identifier: MESFUN10, version: 7.9.01 4.101.1015
Fermat’s Little Theorem via Divisibility of Newton’s Binomial
Solving equations in integers is an important part of the number theory [29]. In many cases it can be conducted by the factorization of equation’s elements, such as the Newton’s binomial. The article introduces several simple formulas, which may facilitate this process. Some of them are taken from relevant books [28], [14]. In the second section of the article, Fermat’s Little Theorem is proved in a classical way, on the basis of divisibility of Newton’s binomial. Although slightly redundant in...
Filters of -algebras.
Finite Equations in n Unknowns
Finite Product of Semiring of Sets
We formalize that the image of a semiring of sets [17] by an injective function is a semiring of sets.We offer a non-trivial example of a semiring of sets in a topological space [21]. Finally, we show that the finite product of a semiring of sets is also a semiring of sets [21] and that the finite product of a classical semiring of sets [8] is a classical semiring of sets. In this case, we use here the notation from the book of Aliprantis and Border [1].
Finite sum-product logic.
Finite Symmetric Functions with Non-Trivial Arity Gap
Given an n-ary k-valued function f, gap(f) denotes the essential arity gap of f which is the minimal number of essential variables in f which become fictive when identifying any two distinct essential variables in f. In the present paper we study the properties of the symmetric function with non-trivial arity gap (2 ≤ gap(f)). We prove several results concerning decomposition of the symmetric functions with non-trivial arity gap with its minors or subfunctions. We show that all non-empty sets of...
Finiteness results on rewriting systems
First Order Languages: Further Syntax and Semantics
Third of a series of articles laying down the bases for classical first order model theory. Interpretation of a language in a universe set. Evaluation of a term in a universe. Truth evaluation of an atomic formula. Reassigning the value of a symbol in a given interpretation. Syntax and semantics of a non atomic formula are then defined concurrently (this point is explained in [16], 4.2.1). As a consequence, the evaluation of any w.f.f. string and the relation of logical implication are introduced....
First order topology [Book]
Fixpoints, games and the difference hierarchy
Drawing on an analogy with temporal fixpoint logic, we relate the arithmetic fixpoint definable sets to the winning positions of certain games, namely games whose winning conditions lie in the difference hierarchy over . This both provides a simple characterization of the fixpoint hierarchy, and refines existing results on the power of the game quantifier in descriptive set theory. We raise the problem of transfinite fixpoint hierarchies.
Fixpoints, games and the difference hierarchy
Drawing on an analogy with temporal fixpoint logic, we relate the arithmetic fixpoint definable sets to the winning positions of certain games, namely games whose winning conditions lie in the difference hierarchy over . This both provides a simple characterization of the fixpoint hierarchy, and refines existing results on the power of the game quantifier in descriptive set theory. We raise the problem of transfinite fixpoint hierarchies.
Folding theory applied to BL-algebras
The notion of n-fold grisly deductive systems is introduced. Some conditions for a deductive system to be an n-fold grisly deductive system are provided. Extension property for n-fold grisly deductive system is established.
Fopid Controller Design for Robust Performance Using Particle Swarm Optimization
Mathematics Subject Classification: 26A33; 93C15, 93C55, 93B36, 93B35, 93B51; 03B42; 70Q05; 49N05This paper proposes a novel method to design an H∞ -optimal fractional order PID (FOPID) controller with ability to control the transient, steady-state response and stability margins characteristics. The method uses particle swarm optimization algorithm and operates based on minimizing a general cost function. Minimization of the cost function is carried out subject to the H∞ -norm; this norm is also...
Formal Specifications in Software Development: an Overview
Formalization of Generalized Almost Distributive Lattices
Almost Distributive Lattices (ADL) are structures defined by Swamy and Rao [14] as a common abstraction of some generalizations of the Boolean algebra. In our paper, we deal with a certain further generalization of ADLs, namely the Generalized Almost Distributive Lattices (GADL). Our main aim was to give the formal counterpart of this structure and we succeeded formalizing all items from the Section 3 of Rao et al.’s paper [13]. Essentially among GADLs we can find structures which are neither V-commutative...
Formalization of the Advanced Encryption Standard. Part I
In this article, we formalize the Advanced Encryption Standard (AES). AES, which is the most widely used symmetric cryptosystem in the world, is a block cipher that was selected by the National Institute of Standards and Technology (NIST) as an official Federal Information Processing Standard for the United States in 2001 [12]. AES is the successor to DES [13], which was formerly the most widely used symmetric cryptosystem in the world. We formalize the AES algorithm according to [12]. We then verify...
Formalized models of ontological systems
Formulas of the general solutions of Boolean equations.