Displaying similar documents to “Definition of First Order Language with Arbitrary Alphabet. Syntax of Terms, Atomic Formulas and their Subterms”

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.

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

Equivalence of Deterministic and Nondeterministic Epsilon Automata

Michał Trybulec (2009)

Formalized Mathematics

Similarity:

Based on concepts introduced in [14], semiautomata and leftlanguages, automata and right-languages, and langauges accepted by automata are defined. The powerset construction is defined for transition systems, semiautomata and automata. Finally, the equivalence of deterministic and nondeterministic epsilon automata is shown.

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.

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

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

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

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