Displaying similar documents to “A N. Bourbaki type general theory and the properties of contracting symbols and corresponding contracted forms.”

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.

The Gödel Completeness Theorem for Uncountable Languages

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

Formalized Mathematics

Similarity:

This article is the second in a series of two Mizar articles constituting a formal proof of the Gödel Completeness theorem [15] for uncountably large languages. We follow the proof given in [16]. The present article contains the techniques required to expand a theory such that the expanded theory contains witnesses and is negation faithful. Then the completeness theorem follows immediately.

Symbol Declarations in Mathematical Writing

Wolska, Magdalena, Grigore, Mihai

Similarity:

We present three corpus-based studies on symbol declaration in mathematical writing. We focus on simple object denoting symbols which may be part of larger expressions. We look into whether the symbols are explicitly introduced into the discourse and whether the information on once interpreted symbols can be used to interpret structurally related symbols. Our goal is to support fine-grained semantic interpretation of simple and complex mathematical expressions. The results of our analysis...

Free Interpretation, Quotient Interpretation and Substitution of a Letter with a Term for First Order Languages

Marco Caminati (2011)

Formalized Mathematics

Similarity:

Fourth of a series of articles laying down the bases for classical first order model theory. This paper supplies a toolkit of constructions to work with languages and interpretations, and results relating them. The free interpretation of a language, having as a universe the set of terms of the language itself, is defined.The quotient of an interpreteation with respect to an equivalence relation is built, and shown to remain an interpretation when the relation respects it. Both the concepts...

Normal forms in partial modal logic

Jan Jaspars (1993)

Banach Center Publications

Similarity:

A "partial" generalization of Fine's definition [Fin] of normal forms in normal minimal modal logic is given. This means quick access to complete axiomatizations and decidability proofs for partial modal logic [Thi].

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

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.

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