Displaying similar documents to “Free Interpretation, Quotient Interpretation and Substitution of a Letter with a Term for First Order Languages”

Representation Theorem for Stacks

Grzegorz Bancerek (2011)

Formalized Mathematics

Similarity:

In the paper the concept of stacks is formalized. As the main result the Theorem of Representation for Stacks is given. Formalization is done according to [13].

Sequent Calculus, Derivability, Provability. Gödel's Completeness Theorem

Marco Caminati (2011)

Formalized Mathematics

Similarity:

Fifth of a series of articles laying down the bases for classical first order model theory. This paper presents multiple themes: first it introduces sequents, rules and sets of rules for a first order language L as L-dependent types. Then defines derivability and provability according to a set of rules, and gives several technical lemmas binding all those concepts. Following that, it introduces a fixed set D of derivation rules, and proceeds to convert them to Mizar functorial cluster...

Relational Formal Characterization of Rough Sets

Adam Grabowski (2013)

Formalized Mathematics

Similarity:

The notion of a rough set, developed by Pawlak [10], is an important tool to describe situation of incomplete or partially unknown information. In this article, which is essentially the continuation of [6], we try to give the characterization of approximation operators in terms of ordinary properties of underlying relations (some of them, as serial and mediate relations, were not available in the Mizar Mathematical Library). Here we drop the classical equivalence- and tolerance-based...

Preliminaries to Classical First Order Model Theory

Marco Caminati (2011)

Formalized Mathematics

Similarity:

First of a series of articles laying down the bases for classical first order model theory. These articles introduce a framework for treating arbitrary languages with equality. This framework is kept as generic and modular as possible: both the language and the derivation rule are introduced as a type, rather than a fixed functor; definitions and results regarding syntax, semantics, interpretations and sequent derivation rules, respectively, are confined to separate articles, to mark...

First Order Languages: Further Syntax and Semantics

Marco Caminati (2011)

Formalized Mathematics

Similarity:

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...

The Vector Space of Subsets of a Set Based on Symmetric Difference

Jesse Alama (2008)

Formalized Mathematics

Similarity:

For each set X, the power set of X forms a vector space over the field Z2 (the two-element field {0, 1} with addition and multiplication done modulo 2): vector addition is disjoint union, and scalar multiplication is defined by the two equations (1 · x:= x, 0 · x := ∅ for subsets x of X). See [10], Exercise 2.K, for more information.MML identifier: BSPACE, version: 7.8.05 4.89.993

N-Dimensional Binary Vector Spaces

Kenichi Arai, Hiroyuki Okazaki (2013)

Formalized Mathematics

Similarity:

The binary set {0, 1} together with modulo-2 addition and multiplication is called a binary field, which is denoted by F2. The binary field F2 is defined in [1]. A vector space over F2 is called a binary vector space. The set of all binary vectors of length n forms an n-dimensional vector space Vn over F2. Binary fields and n-dimensional binary vector spaces play an important role in practical computer science, for example, coding theory [15] and cryptology. In cryptology, binary fields...

Pseudo-Canonical Formulae are Classical

Marco B. Caminati, Artur Korniłowicz (2014)

Formalized Mathematics

Similarity:

An original result about Hilbert Positive Propositional Calculus introduced in [11] is proven. That is, it is shown that the pseudo-canonical formulae of that calculus (and hence also the canonical ones, see [17]) are a subset of the classical tautologies.

Definition of First Order Language with Arbitrary Alphabet. Syntax of Terms, Atomic Formulas and their Subterms

Marco Caminati (2011)

Formalized Mathematics

Similarity:

Second of a series of articles laying down the bases for classical first order model theory. A language is defined basically as a tuple made of an integer-valued function (adicity), a symbol of equality and a symbol for the NOR logical connective. The only requests for this tuple to be a language is that the value of the adicity in = is -2 and that its preimage (i.e. the variables set) in 0 is infinite. Existential quantification will be rendered (see [11]) by mere prefixing a formula...

Strong completeness of the Lambek Calculus with respect to Relational Semantics

Szabolcs Mikulás (1993)

Banach Center Publications

Similarity:

In [vB88], Johan van Benthem introduces Relational Semantics (RelSem for short), and states Soundness Theorem for Lambek Calculus (LC) w.r.t. RelSem. After doing this, he writes: "it would be very interesting to have the converse too", i.e., to have Completeness Theorem. The same question is in [vB91, p. 235]. In the following, we state Strong Completeness Theorems for different versions of LC.

Transition of Consistency and Satisfiability under Language Extensions

Julian J. Schlöder, Peter Koepke (2012)

Formalized Mathematics

Similarity:

This article is the first in a series of two Mizar articles constituting a formal proof of the Gödel Completeness theorem [17] for uncountably large languages. We follow the proof given in [18]. The present article contains the techniques required to expand formal languages. We prove that consistent or satisfiable theories retain these properties under changes to the language they are formulated in.